Anthropic công bố mã nguồn chứng minh Định lý lớn Fermat bằng Lean 4

Định lý lớn Fermat trong Lean 4

Một chứng minh hoàn chỉnh, được máy tính kiểm chứng về Định lý lớn Fermat trong Lean 4, được xây dựng dựa trên Mathlib (Lean 4.33.1; Mathlib v4.33.0, được ghim theo commit trong lakefile.lean). Lập luận này dựa trên công trình của Frey, Serre, Ribet, Wiles và Taylor-Wiles. Tệp PROOF-PATH.md nêu tên từng bước và định lý Lean tương ứng, còn thư mục html/ trình bày toàn bộ chứng minh dưới dạng các trang web mà bạn có thể duyệt ngoại tuyến (xem phần "Đọc chứng minh trên trình duyệt" bên dưới).

Sản phẩm nghiên cứu. Không được duy trì và không nhận đóng góp.

Phát biểu

Theorems/Thm_fermat_last_theorem.lean khai báo

và mục tiêu xây dựng mặc định FinalCheck.lean chứa

vì vậy quá trình xây dựng sẽ thất bại trừ khi chứng minh dựa trên đúng ba tiên đề tiêu chuẩn của Lean (không có sorry, không có tiên đề bổ sung, không có native_decide). FinalCheck.lean cũng suy ra phát biểu của riêng Mathlib, FermatLastTheorem, từ định lý này.

Cách thức xác minh

Không có module nào chứa axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def hoặc #eval (Challenge.lean sử dụng sorry theo thiết kế và không phải là một phần của gói này).

Tổng hợp lại, các kiểm tra này xác lập rằng phát biểu trên tuân theo ba tiên đề, với giả định tin tưởng vào nhân (kernel) của Lean (hoặc nanoda) và các công cụ kiểm tra. Phát biểu được viết bằng các số tự nhiên tích hợp sẵn của Lean, các toán tử +, ≤, < và ≠; thành phần duy nhất từ Mathlib là ^ trên ℕ, được Mathlib định nghĩa là phép lũy thừa tích hợp của Lean, và các trình kiểm tra so sánh đảm bảo rằng mọi định nghĩa được nêu trong phát biểu đều đồng nhất với Mathlib gốc. Không cần phải tin tưởng bất kỳ thành phần nào khác trong Mathlib, vì nhân của Lean kiểm tra mọi thứ bên dưới phát biểu. Điều mà không công cụ nào có thể kiểm tra là liệu mỗi định lý trung gian có mang ý nghĩa như tên gọi của nó hay không; đó là việc của người đọc, và PROOF-PATH.md đã nêu tên định lý Lean đằng sau mỗi bước và xác định chính xác mức độ mạnh của từng kết quả cổ điển được chứng minh tại đây.

Đọc chứng minh trên trình duyệt

Thư mục html/ (khoảng 390 MB) trình bày kho lưu trữ này dưới dạng các trang web tĩnh: lộ trình chứng minh từng bước; một trang cho mỗi định lý trong tổng số 29.511 định lý (phát biểu Lean chính xác, các tài liệu trích dẫn và được trích dẫn, cùng đồ thị phụ thuộc có thể mở rộng) và cho mỗi module trong 1.450 module định nghĩa (mã nguồn đầy đủ và các phát biểu sử dụng nó); một ô tìm kiếm trên tất cả tên định lý và định nghĩa; các định lý cột mốc dưới dạng đồ thị; cùng các tệp README.md, PROOF-PATH.md và ATTRIBUTION.md được hiển thị với các liên kết chéo. Thư mục này là một phần của kho lưu trữ, vì vậy khi clone hoặc tải xuống tệp ZIP, bạn đã có sẵn nó (nếu bạn nhận được html/ dưới dạng tệp lưu trữ riêng, hãy giải nén nó tại thư mục gốc của kho lưu trữ). Mở html/index.html trong trình duyệt web; mọi thứ đều hoạt động ngoại tuyến mà không cần máy chủ web. Các trang này chỉ được kiểm tra bằng máy trên trình duyệt dựa trên Chromium, và tệp html/README-DOCS.md giải thích những gì được trích dẫn từ các tệp Lean và những gì được tạo tự động (các tóm tắt tiếng Anh và tài liệu tham khảo gợi ý được tạo tự động; phát biểu Lean là căn cứ xác thực).

Tự kiểm tra

Lean in ra một số lượng lớn các cảnh báo về deprecation (ngừng hỗ trợ) và style-linter trong quá trình xây dựng. Chúng không ảnh hưởng đến kết quả. Quá trình xây dựng thành công khi đầu ra kết thúc bằng 'flt_mathlib' depends on axioms: [propext, Classical.choice, Quot.sound] và Build completed successfully. Mỗi tập lệnh sẽ tìm nạp và xây dựng trình kiểm tra của nó ở phiên bản đã ghim và thoát với mã 0 khi thành công.

Về các nguồn tài liệu

FinalCheck.lean là mục tiêu mặc định; Theorems/ chứa các phát biểu, P2M/Sol/ chứa các chứng minh (mỗi tệp nhập các phát biểu mà nó trích dẫn), Definitions/ chứa các định nghĩa, verification/ chứa hai bài kiểm tra, html/ chứa các trang web đã mô tả ở trên và tools/docs-site/ chứa chương trình tạo ra chúng. Các nguồn Lean được tạo ra bởi các tác nhân AI dựa trên mã nguồn mở Lean do con người viết, với Lean đóng vai trò trọng tài, và được viết để máy kiểm tra thay vì để đọc: tên gọi được tạo tự động, các nhãn như P2M hoặc hậu tố thập lục phân là nhãn của quy trình thay vì toán học, và khi tên gọi và phát biểu không khớp nhau, phát biểu mới là thứ đã được chứng minh. Các bình luận đã bị loại bỏ, ngoại trừ các thông báo từ nguồn gốc, doc strings và các trích dẫn (được liệt kê trong ATTRIBUTION.md) cùng bình luận expected-output mà #guard_msgs kiểm tra.

Giấy phép và ghi nhận tác giả

Bản quyền 2026 Anthropic, PBC; phát hành theo Giấy phép Apache 2.0 (LICENSE). Một phần nội dung bắt nguồn từ ba dự án Apache-2.0 được ghi nhận trong NOTICE: dự án FLT của Imperial College London do Kevin Buzzard dẫn đầu (gói Frey, biểu diễn Galois, lý thuyết biến dạng, patching và nhiều nội dung khác), flt-regular (định lý Kummer) và Mathlib. ATTRIBUTION.md liệt kê 106 tệp chứa tài liệu từ hai dự án đầu tiên, cùng với tệp nguồn, chủ sở hữu bản quyền và tác giả, và 23 tệp tái tạo văn bản của Mathlib (các đoạn trích trong Definitions/Def_Compat_Mathlib430.lean và hai mươi hai module chứng minh lại một bổ đề của Mathlib tại chỗ). Các trang web tích hợp KaTeX và Graphviz (được biên dịch sang WebAssembly) theo giấy phép riêng của chúng, được liệt kê trong html/assets/vendor/LICENSES.txt. Lean và các gói trong lake-manifest.json được tìm nạp tại thời điểm xây dựng, không được phân phối tại đây. Nếu bạn nhận ra tài liệu chưa được ghi nhận, sự thiếu sót đó là không cố ý.