Anthropic công bố bằng chứng hoàn chỉnh cho Định lý cuối cùng của Fermat trong Lean 4

Anthropic vừa phát hành một bằng chứng toán học hoàn chỉnh, được máy kiểm tra, cho Định lý cuối cùng của Fermat trong Lean 4 — một cột mốc quan trọng cho việc ứng dụng AI trong toán học và xác minh chính thức. Dự án mã nguồn mở này được xây dựng trên Mathlib, bộ thư viện chuẩn của Lean, và triển khai đầy đủ chuỗi lập luận kinh điển của Frey, Serre, Ribet, Wiles và Taylor-Wiles.

Bằng chứng không chỉ dừng lại ở việc khai báo định lý mà còn cung cấp các công cụ xác minh độc lập — bao gồm một bộ so sánh và một trình kiểm tra nanoda — để đảm bảo rằng mã Lean thực thi đúng như những gì đã tuyên bố. Đây là một research artifact (sản phẩm nghiên cứu), được thiết kế để kiểm tra, không phải để đọc, với mã nguồn có thể được sinh ra bởi các tác nhân AI dưới sự giám sát chặt chẽ của chính Lean.

Nội dung chính của dự án

Kho lưu trữ trên GitHub bao gồm nhiều thành phần được tổ chức rõ ràng:

• Theorems/: chứa tệp khai báo định lý chính Thm_fermat_last_theorem.lean, nói rằng với mọi số tự nhiên n ≥ 3 và các số a, b, c nguyên dương, phương trình a^n + b^n = c^n không có nghiệm.
• P2M/Sol/: chứa toàn bộ phần chứng minh, mỗi module nhập các khai báo mà nó trích dẫn.
• Definitions/: định nghĩa các khái niệm được sử dụng xuyên suốt.
• verification/: gồm hai tập lệnh xác minh độc lập — một bộ so sánh (comparator) và một trình kiểm tra nanoda.
• html/: toàn bộ bằng chứng được trình bày dưới dạng trang web có thể duyệt ngoại tuyến.
• tools/docs-site/: chương trình đã tạo ra các trang web đó.

Xác minh độc lập và bảo mật

Điểm đáng chú ý của dự án là cơ chế xác minh hai lớp. Người dùng có thể tự xây dựng dự án bằng lệnh lake build với mức bộ nhớ khoảng 5 GB mỗi tiến trình. Sau đó, hai tập lệnh kiểm tra sẽ được chạy:

• verification/comparator/run.sh — so sánh đầu ra.
• verification/nanoda/run.sh — dùng trình kiểm tra nanoda (một trình kiểm tra khác của Lean) để xác nhận lại.

Kết quả cuối cùng được coi là thành công khi đầu ra kết thúc bằng dòng thông báo rằng flt_mathlib chỉ phụ thuộc vào ba tiên đề cơ bản: propext, Classical.choice, Quot.sound. Điều này đồng nghĩa với việc bằng chứng không sử dụng bất kỳ tiên đề bổ sung không chính đáng nào.

Nguồn gốc và giấy phép

Dự án được phát hành bởi Anthropic, PBC với giấy phép Apache License 2.0 và đã ghi nhận công lao của các dự án nguồn mở liên quan:

• Dự án FLT của Imperial College London do Kevin Buzzard dẫn dắt — cung cấp các gói Frey, biểu diễn Galois, lý thuyết biến dạng.
• Dự án flt-regular (định lý Kummer).
• Mathlib — bộ thư viện chuẩn của Lean.

Tệp ATTRIBUTION.md liệt kê chi tiết 106 tệp chứa tài liệu từ hai dự án đầu, cùng 23 tệp tái hiện nội dung từ Mathlib. Các tài nguyên như KaTeX và Graphviz (được biên dịch sang WebAssembly) đi kèm cũng có giấy phép riêng.

Ý nghĩa đối với cộng đồng toán học và AI

Đối với độc giả Việt Nam quan tâm đến toán học và công nghệ, dự án này minh chứng một xu hướng quan trọng: AI đang trở thành trợ thủ đắc lực trong việc tạo ra các chứng minh toán học phức tạp, không chỉ ở mức hỗ trợ con người mà còn ở mức tự động hóa một phần hoặc toàn bộ quá trình suy luận, với sự đảm bảo chặt chẽ từ hệ thống máy tính.

Việc có một bằng chứng máy kiểm tra cho một định lý huyền thoại như FLT — vốn từng được coi là bất khả thi trong nhiều thế kỷ — mở ra tiềm năng to lớn cho việc xác minh chính thức trong các lĩnh vực khác như phát triển phần mềm an toàn, giao thức blockchain hay hệ thống trí tuệ nhân tạo đáng tin cậy.

Cách tiếp cận

Dù mã nguồn được sinh ra từ AI, tác giả nhấn mạnh rằng Lean chính là trọng tài cuối cùng — mọi bước suy luận phải được máy xác nhận trước khi được chấp nhận. Các tên định danh trong mã có thể được sinh tự động và không mang ý nghĩa toán học, và khi tên mâu thuẫn với nội dung khai báo thì chính khai báo (statement) mới là điều được chứng minh.

Dự án hiện không được bảo trì và không nhận đóng góp — một tuyên bố rõ ràng về bản chất nghiên cứu của nó. Tuy nhiên, với mã nguồn mở, bất kỳ ai cũng có thể tải về, tự kiểm tra, và học hỏi từ cách bố trí của một chứng minh quy mô lớn trong Lean.