Anthropic chạm đích trước: Trí tuệ nhân tạo chính thức hóa thành công Định lý cuối cùng của Fermat

Trong một thông báo gây chấn động giới toán học, Anthropic đã xác nhận rằng một trong các mô hình nội bộ của họ, sử dụng nền tảng prove2.me, đã hoàn tất việc hình thức hóa toàn bộ chứng minh Định lý cuối cùng của Fermat (FLT) trong Lean. Đây là định lý cuối cùng được hình thức hóa trong danh sách 100 bài toán hình thức hóa nổi tiếng của Freek Wiedijk, khép lại một cột mốc kéo dài suốt 20 năm. Tuy nhiên, ý nghĩa thực sự không nằm ở định lý—điều đã được chứng minh từ lâu—mà ở sức mạnh của công nghệ autoformalization (tự động hình thức hóa) trong việc biến hàng ngàn trang giấy tờ toán học thành mã máy có thể kiểm chứng chỉ trong… 11 ngày.

Chi tiết toán học của chứng minh

Điều đáng chú ý là Anthropic không sử dụng chứng minh hiện đại (mà tác giả bài viết, nhà toán học Kevin Buzzard, đang theo đuổi dựa trên công trình của Khare, Taylor...). Thay vào đó, họ chọn cách tiếp cận theo trình bày Darmon–Diamond–Taylor từ năm 1995 về lập luận Wiles–Taylor–Wiles, thông qua định lý Langlands–Tunnell và định lý hạ mức của Ribet.

Repository của Anthropic phát triển lý thuyết Fontaine (để nghiên cứu sự biến dạng phẳng của biểu diễn Galois) và đủ lý thuyết về iđêan Eisenstein của Mazur để đưa ra kết luận rằng không đường cong Frey nào có thể có điểm bậc 17. Điều này hạn chế phạm vi chứng minh với điều kiện p ≥ 17. Tuy nhiên, điều này không thành vấn đề vì FLT đã được hình thức hóa cho các số nguyên tố chính quy lẻ bởi Best-Birkbeck-Brasca-Rodriguez; số nguyên tố bất quy tắc nhỏ nhất là 37, và do đó mọi trường hợp đều được bao phủ.

Công thức điều kiện p ≥ 17

Quy mô mã nguồn ấn tượng

Buzzard, người được Anthropic trao quyền truy cập để kiểm chứng, đã biên dịch và chạy bộ kiểm tra comparator trên mã nguồn. Kết quả cho thấy đây là một "cỗ máy" chứng minh khổng lồ lên tới hơn 13,4 triệu dòng mã, cần thời gian biên dịch gần gấp 20 lần thư viện toán học của Lean, ngay cả trên máy chủ 96 nhân với 500GB RAM. Mặc dù Lean có thể hoạt động chậm khi duyệt nhiều tệp trong kho mã kích thước lớn, Anthropic cũng cung cấp các tài liệu HTML dễ khám phá hơn thay vì phải lục lọi trong mã lệnh.

Việc này mang ý nghĩa gì (và không là gì)

Một phản ứng ngây thơ sẽ là: Buzzard giờ không còn việc để làm nữa vì ông đang được EPSRC tài trợ 1 triệu bảng Anh để hình thức hóa FLT trong 5 năm. Nhưng tác giả bài viết thẳng thắn khẳng định điều ngược lại:

• Về mặt toán học thuần túy, công trình này không mang lại tri thức mới. Buzzard từng tuyên bố ông 99,9% chắc chắn rằng chứng minh FLT là đúng, và giới lý thuyết số hầu như chắc chắn 100%. Ông cho rằng quá trình hình thức hóa này chỉ bám sát các tài liệu cũ và "không thêm gì mới".
• Mục tiêu ban đầu của Buzzard với EPSRC là giảm FLT về toán học của thập niên 1980, chứ không phải chứng minh trọn vẹn. Vì vậy công trình của Anthropic đi xa hơn, nhưng đồng thời họ không hướng tới việc tạo tài liệu động cho con người khám phá—điều mà ông cam kết thực hiện.
• Điều quan trọng nhất đến từ khía cạnh autoformalization: nếu AI có thể tự động hóa hàng ngàn trang văn bản trong 11 ngày thì tương lai sẽ chứng kiến việc hình thức hóa các nghiên cứu hiện đại một cách "trực tuyến".

"Khả năng tự động hình thức hóa các tài liệu khó cuối cùng sẽ làm cho quá trình bình duyệt các bài báo toán học bớt đau đớn hơn nhiều. Nó cũng giữ cho chúng ta trung thực—có những bài báo với giả định 'những người trong ngành đều biết' và sẽ rất thú vị khi xem chính xác điều gì đang được giả định trong các chứng minh quan trọng thuộc lĩnh vực của tôi." — Kevin Buzzard

Câu chuyện cá nhân

Buzzard kết thúc bài viết bằng một giai thoại thú vị. Năm 1993, Wiles công bố chứng minh của mình tại Viện Newton trong ba bài giảng. Buzzard lúc đó là nghiên cứu sinh năm thứ hai, dự buổi đầu tiên, thấy "hoàn toàn khó hiểu", bèn bỏ hai buổi sau để đi nghỉ ở Ireland cùng bạn gái mới. Mãi khi quay lại Cambridge một tuần sau, ông mới nghe tin định lý đã được chứng minh.

Điều tương tự gần như lặp lại vào năm 2026. Trong kỳ festival Green Man tại xứ Wales với người bạn gái đó—giờ là vợ—ông nhận được email từ một người lạ với tiêu đề "End-to-end Lean formalization of Fermat's Last Theorem"… nhưng vì sóng điện thoại kém, ông gạt đi và tưởng là "thư rác". Một tuần sau, khi dọn dẹp gần 1.000 email tồn đọng, ông mới giật mình nhận ra sự thật. "Anthropic mất chỉ 11 ngày; tôi nhận được 1 triệu bảng để chạy dự án trong 5 năm. Nhưng tôi tự hỏi liệu họ có chi nhiều tiền hơn thế không?" — ông đùa.

Kết luận

Công trình này là một cột mốc quan trọng, không phải vì nó chứng minh FLT (điều đã được công nhận từ năm 1995), mà vì nó chứng minh khả năng của AI trong việc xử lý, kiểm tra và mô hình hóa các khối kiến thức toán học khổng lồ. Với tốc độ này, giấc mơ về những cỗ máy "kiểm toán toán học" tự động sẽ không còn xa.