Claude Hình thức hóa Định lý Cuối cùng của Fermat trong Lean trong 11 ngày

Anthropic thông báo vào ngày 4 tháng 9 rằng Claude đã tạo ra chứng minh hoàn chỉnh đầu tiên của Định lý Cuối cùng của Fermat được máy tính kiểm tra. Theo công ty, hàng chục tác nhân Claude đã làm việc phần lớn một cách tự chủ trong 11 ngày, tạo ra khoảng 13 triệu dòng mã Lean và chứng minh 30.300 định lý, trong đó khoảng 29.500 định lý xuất hiện trong chứng minh cuối cùng.

Đây không phải là một chứng minh mới của Định lý Cuối cùng của Fermat theo nghĩa toán học thông thường. Andrew Wiles và Richard Taylor đã hoàn thành chứng minh được giới toán học chấp nhận vào thập niên 1990. Thay vào đó, Claude chuyển một hướng chứng minh đã được thiết lập trong tài liệu nghiên cứu sang ngôn ngữ hình thức, nơi các bước logic có thể được máy tính kiểm tra.

Sự phân biệt này quan trọng. Kết quả hầu như không bổ sung tri thức mới về việc Định lý Cuối cùng của Fermat có đúng hay không, nhưng cho thấy một hệ thống AI có thể hình thức hóa một khối toán học nâng cao vốn trước đây được kỳ vọng cần nhiều năm công sức của chuyên gia. Kevin Buzzard, nhà toán học tại Imperial College London đang dẫn dắt một dự án hình thức hóa riêng, đã biên dịch mã của Anthropic và tự chạy các kiểm tra comparator. Ông cho biết chứng minh đã được kiểm tra thành công.

1. Claude đã chứng minh hình thức điều gì

Định lý Cuối cùng của Fermat phát biểu rằng không có các số nguyên dương \(a\), \(b\) và \(c\) thỏa mãn \(a^n+b^n=c^n\) khi số mũ nguyên \(n\) ít nhất là ba. Mệnh đề này có vẻ sơ cấp, nhưng các chứng minh đã biết của nó phụ thuộc vào những kết quả tinh vi liên quan đến đường cong elliptic, dạng mô-đun, biểu diễn Galois, lý thuyết biến dạng, hình học đại số và lý thuyết số.

Kho mã của Anthropic biểu diễn định lý cuối cùng trực tiếp trên các số tự nhiên của Lean. Mệnh đề của nó nhận các số tự nhiên dương \(a\), \(b\) và \(c\), cùng với \(n \geq 3\), rồi chứng minh rằng phương trình không thể đúng. Một kiểm tra cuối cùng riêng biệt suy ra phát biểu hiện có của Mathlib về Định lý Cuối cùng của Fermat từ định lý này.

Lập luận đi theo công trình của Frey, Serre, Ribet, Wiles và Taylor–Wiles, đặc biệt là phần trình bày năm 1995 của Henri Darmon, Fred Diamond và Richard Taylor. Nó sử dụng mối liên hệ giữa một nghiệm giả định của phương trình Fermat với một đường cong elliptic Frey, sau đó áp dụng các kết quả về tính mô-đun và hạ mức để đi đến mâu thuẫn.

Buzzard chỉ ra một chi tiết quan trọng trong cách xây dựng. Hướng đi dựa trên Wiles của Anthropic xử lý các số mũ nguyên tố \(p \geq 17\). Kết quả hoàn chỉnh kết hợp công trình đã được hình thức hóa trước đó về các số nguyên tố chính quy để khép lại những trường hợp còn lại. Tuy vậy, định lý Lean thu được vẫn bao quát mọi số mũ là số tự nhiên ít nhất bằng ba.

Hiện vật này cũng phụ thuộc vào khối lượng đáng kể công việc trước đó của con người. Anthropic cho biết họ đã điều chỉnh tài liệu từ dự án FLT của Imperial College, dự án flt-regular và Mathlib. Tệp ghi công của họ xác định 106 tệp chứa nội dung từ hai dự án đầu và 23 tệp tái tạo văn bản của Mathlib. Do đó, thành tựu này là sự tích hợp và mở rộng do AI dẫn dắt của một hệ sinh thái hình thức hiện có, chứ không phải 13 triệu dòng được tạo ra độc lập với toán học hình thức trước đó.

2. Cách một hệ thống đa tác nhân quản lý chứng minh

Ban đầu, Anthropic nhận thấy các tác nhân Claude có thể chứng minh từng kết quả riêng lẻ nhưng mất dấu dự án rộng lớn hơn. Các tác nhân trùng lặp công việc, không tái sử dụng hiệu quả các định lý đã hoàn thành và ngừng phối hợp khi chứng minh phát triển. Những nỗ lực thất bại vẫn chiếm khoảng 7% mã không phải boilerplate trong kết quả cuối cùng.

Lần chạy thành công sử dụng Prove2Me, một nền tảng hình thức hóa cộng tác mở do Tianyi Peng và các cộng sự tại Đại học Columbia phát triển. Prove2Me biểu diễn một dự án dưới dạng đồ thị có hướng không chu trình gồm các phát biểu định lý. Các tác nhân có thể chọn những nút chưa hoàn thành, chứng minh các điều kiện tiên quyết và tái sử dụng các kết quả được tạo ra ở nơi khác trong đồ thị.

Nền tảng này cũng tách các phát biểu định lý khỏi chứng minh của chúng. Thiết kế đó giảm chi phí biên dịch lại và cho phép hệ thống thay đổi hoặc thay thế một chứng minh mà không làm gián đoạn mọi phát biểu phụ thuộc. Các mô tả ngôn ngữ tự nhiên gắn với các nút định lý cung cấp cho tác nhân thêm một cách để tìm kiếm thư viện đang phát triển và nhận diện các phụ thuộc hữu ích.

Một harness đa tác nhân dựa trên Claude Code đã điều phối hàng chục tác nhân trong lần chạy kéo dài 11 ngày. Đầu vào toán học từ con người được cho là chỉ giới hạn ở các ưu tiên cấp cao không thường xuyên, chẳng hạn hướng các tác nhân tới các Jacobian hoặc yêu cầu họ hoàn thành một định lý liên quan đến công trình của Mazur. Một nhật ký nội bộ ghi nhận định lý gốc đã được chứng minh vào ngày 18 tháng 8.

Anthropic báo cáo rằng lần chạy đã tiêu thụ xấp xỉ sáu tỷ token đầu ra. Nó sử dụng một mô hình nghiên cứu nội bộ đa dụng chỉ được mô tả là gần tương đương Claude Fable 5.1, vì vậy mô hình và cấu hình chính xác không được công khai. Công ty chưa tiết lộ chi phí tiền tệ hoặc chi phí tính toán của dự án.

Bản phát triển hoàn chỉnh chứa 29.511 trang định lý và 1.450 mô-đun định nghĩa trong tài liệu có thể duyệt. Anthropic tính 30.300 định lý có thể được máy tính xác minh trên toàn bộ lần chạy, bao gồm các kết quả rốt cuộc không cần đến cho đường phụ thuộc cuối cùng.

3. Chứng minh đã được kiểm tra như thế nào

Một chứng minh hình thức chỉ có giá trị nếu phát biểu định lý, các giả định được phép và quy trình xác minh được kiểm soát. Kho mã của Anthropic ghim dự án vào Lean 4.33.1 và Mathlib 4.33.0, đồng thời bao gồm nhiều lớp kiểm tra.

Trước hết, dự án được xây dựng từ đầu. 60.475 mô-đun của nó được kernel Lean kiểm tra. Định lý cuối cùng phụ thuộc chính xác vào ba tiên đề Lean chuẩn: tính mở rộng mệnh đề, lựa chọn cổ điển và tính đúng đắn của thương. Các mô-đun chứng minh được phân phối không chứa placeholder sorry chưa hoàn thành, tiên đề mới khai báo, mã không an toàn, lối tắt quyết định native hoặc hiện thực bên ngoài.

Thứ hai, dự án sử dụng Lean Comparator để so sánh định lý đã chứng minh với một phát biểu thách thức được cung cấp riêng, chỉ dựa trên Mathlib. Kiểm tra này được thiết kế để xác lập rằng lời giải chứng minh cùng một mệnh đề, không dùng tiên đề chưa được phê duyệt và được kernel chấp nhận. Comparator đã trả về phán quyết chấp nhận.

Thứ ba, một hiện thực kernel Lean độc lập mang tên nanoda đã kiểm tra một phiên bản môi trường được xuất ra và chấp nhận 1.052.234 khai báo không có lỗi. Anthropic áp dụng bốn bản vá cho nanoda: một bản cho đầu ra tiến trình và ba bản để tăng tốc các truy vấn tìm kiếm đẳng thức định nghĩa. Kho mã cho biết không bản vá nào thay đổi hoặc làm suy yếu một quy tắc kiểu.

Buzzard đưa ra xác nhận bên ngoài phù hợp nhất. Ông biên dịch mã trên một máy 96 lõi và tự chạy comparator. Ông mô tả kho mã có hơn 13,4 triệu dòng và cho biết việc biên dịch mất thời gian gần gấp 20 lần so với thư viện toán học của Lean.

Có thể tái tạo mọi kiểm tra, nhưng việc đó đòi hỏi phần cứng lớn. Bản dựng được Anthropic ghi lại mất 5 giờ 32 phút với 96 tác vụ song song, đạt đỉnh 153 GB bộ nhớ và sử dụng xấp xỉ 67 GB cho bản dựng Lean cùng tối đa 220 GB tệp C được tạo ra có thể xóa. Lần chạy comparator mất 14 giờ 46 phút và đạt đỉnh 230 GB. Việc xuất môi trường cho kernel thứ hai tạo ra một tệp 37,8 GB.

Các kiểm tra này xác lập rằng phát biểu hình thức chính xác tuân theo từ các tiên đề đã liệt kê, với giả định tính đúng đắn của ít nhất một kernel kiểm tra và các công cụ xác minh xung quanh. Chúng không tự động xác lập rằng tên do máy tạo ra của mọi định lý trung gian mô tả chính xác ý nghĩa toán học của nó. Anthropic xử lý hạn chế đó bằng một tài liệu đường dẫn chứng minh, ánh xạ các bước toán học chính tới các phát biểu Lean chính xác của chúng.

4. Điều gì đã thay đổi đối với toán học có AI hỗ trợ

Trước kết quả này, Định lý Cuối cùng của Fermat là mục còn lại trong danh sách lâu năm gồm 100 thách thức đáng chú ý về hình thức hóa định lý của Freek Wiedijk. Dự án Imperial College bắt đầu vào năm 2024 với nguồn tài trợ năm năm và ban đầu hướng đến việc quy định lý về các kết quả đã biết vào cuối thập niên 1980. Tài liệu dự án ghi nhận rằng một hình thức hóa hoàn chỉnh sẽ cần chuyển dịch hàng nghìn trang toán học không hình thức.

Thay vào đó, chứng minh của Anthropic đi đến định lý cuối cùng từ đầu đến cuối. Buzzard nhấn mạnh rằng điều này không khiến dự án của ông trở nên dư thừa: nỗ lực của Imperial đang phát triển các phần bổ sung có thể tái sử dụng, dễ đọc với con người cho Mathlib và đi theo một chứng minh hiện đại hơn. Anthropic gắn nhãn kho mã của mình là một hiện vật nghiên cứu sẽ không được duy trì và không nhận đóng góp.

Do đó, tiến bộ thực tiễn nằm ở thông lượng. Các tác nhân Claude đã tập hợp các định nghĩa và chứng minh hình thức trải rộng trên đại số, giải tích điều hòa, hình học và lý thuyết số ở quy mô vượt số dòng của Mathlib hơn năm lần. Kết quả cho thấy một hệ thống tác nhân dựa trên đồ thị có thể duy trì các phụ thuộc và điều phối công việc trên một quá trình hình thức hóa quá lớn đối với ngữ cảnh của một mô hình đơn lẻ.

Chứng minh cũng cho thấy một lộ trình xác minh cho toán học do AI tạo ra. Một mô hình ngôn ngữ có thể tạo ra lập luận ngôn ngữ tự nhiên không chính xác với văn phong thuyết phục, nhưng Lean từ chối một hạng tử chứng minh không kiểm tra kiểu. Một phát biểu định lý được kiểm soát riêng và comparator tiếp tục giảm rủi ro tác nhân thành công bằng cách âm thầm làm yếu hoặc thay đổi bài toán.

Cơ chế đó không loại bỏ nhu cầu về các nhà toán học. Con người vẫn phải quyết định liệu một phát biểu hình thức có nắm bắt khái niệm dự định hay không, đánh giá tầm quan trọng và cách trình bày của một kết quả, cũng như duy trì các thư viện có thể tái sử dụng. Tuy nhiên, nó có thể chuyển việc kiểm tra toàn diện các bước logic từ các phản biện viên con người sang các kernel trợ lý chứng minh—với điều kiện các định nghĩa, phát biểu định lý và ranh giới xác minh đáng tin cậy được kiểm tra độc lập.

Câu hỏi thường gặp

Claude có phát hiện một chứng minh mới của Định lý Cuối cùng của Fermat không?

Không. Claude đã hình thức hóa một hướng đã được thiết lập trong tài liệu Frey–Serre–Ribet–Wiles–Taylor–Wiles để Lean có thể kiểm tra mọi bước logic.

Kết quả có được xác minh độc lập không?

Kevin Buzzard đã biên dịch mã công khai và chạy Lean Comparator, cho biết kết quả kiểm tra thành công. Kho mã cũng ghi nhận các kiểm tra thành công bởi Lean và kernel độc lập nanoda.

Mô hình Claude nào đã tạo ra chứng minh?

Anthropic chưa nêu tên một mô hình công khai chính xác. Công ty mô tả mô hình nghiên cứu nội bộ đa dụng này là gần tương đương Claude Fable 5.1.

Các nhà nghiên cứu có thể tái tạo việc xác minh không?

Có, mã và hướng dẫn được công khai theo giấy phép Apache 2.0. Việc tái tạo đầy đủ đòi hỏi phần cứng đáng kể, bao gồm hàng trăm gigabyte bộ nhớ cho một số giai đoạn xác minh.

Kho mã 13 triệu dòng có hoàn toàn là toán học mới do AI viết không?

Không. Các tác nhân AI đã tạo ra và tích hợp phần lớn bản phát triển trong khi xây dựng trên Mathlib và công trình hình thức hóa mã nguồn mở trước đó từ các dự án Imperial College FLT và flt-regular.

Tham khảo nguồn

• Thông báo gốc của Anthropic trên X
• Anthropic: Hình thức hóa Định lý Cuối cùng của Fermat
• Kho mã Định lý Cuối cùng của Fermat của Anthropic
• Kevin Buzzard: FLT—Anthropic đã vượt qua tôi
• Bài báo nghiên cứu Prove2Me
• Dự án hình thức hóa Lean của Imperial College London
• Kho mã Lean Comparator và mô hình xác minh