Đàn tác tử AI Claude hình thức hóa chứng minh Định lý lớn Fermat trong 11 ngày

Lean là ngôn ngữ lập trình và hệ thống chứng minh định lý tương tác, được phát triển ban đầu tại Microsoft Research. Lean được thiết kế để biểu diễn các định nghĩa, mệnh đề và chứng minh toán học theo dạng mà máy tính có thể kiểm tra một cách chặt chẽ.

Định lý lớn Fermat được Pierre de Fermat nêu từ thế kỉ 17, khẳng định không tồn tại các số nguyên dương a, b, c thỏa mãn aⁿ + bⁿ = cⁿ với n > 2.

Sau hơn 350 năm chưa có lời giải, nhà toán học Andrew Wiles (Anh) công bố chứng minh hoàn chỉnh vào năm 1995, dựa trên những công cụ sâu của lý thuyết số hiện đại. Bản chứng minh của Andrew Wiles dài khoảng 129 trang và từng trải qua quá trình kiểm tra kéo dài, sau khi các nhà toán học phát hiện một lỗ hổng trong phiên bản ban đầu.

Mới đây, Anthropic - công ty AI hàng đầu thế giới - cho biết Claude đã hoàn thành nhiệm vụ hình thức hóa toàn bộ chứng minh để máy tính có thể kiểm chứng.

Không phải Claude tìm ra lời giải mới

Theo Anthropic, Claude không tự xây dựng một chứng minh mới cho Định lý lớn Fermat mà dựa trên phiên bản giản lược của con đường chứng minh do Andrew Wiles phát triển. Cách trình bày này được lấy từ công trình của Henri Darmon, Fred Diamond và Richard Taylor - ba nhà toán học chuyên về lý thuyết số và những lĩnh vực toán học liên quan đến chứng minh của Andrew Wiles.

Chuỗi lập luận này kế thừa các kết quả quan trọng của 5 nhà toán học Gerhard Frey, Jean-Pierre Serre, Ken Ribet, Andrew Wiles và Richard Taylor.

Điểm mới là Claude đã chuyển toàn bộ các bước trong chứng minh thành mã Lean, để máy tính có thể kiểm tra xem từng bước suy luận có đúng theo các quy tắc toán học và logic hay không.

Trong một chứng minh dành cho con người, nhà toán học có thể bỏ qua những bước được cho là hiển nhiên. Với Lean, các bước đó phải được thể hiện đủ rõ để hệ thống có thể kiểm tra. Đây chính là phần công việc thường rất tốn thời gian khi hình thức hóa các chứng minh toán học lớn.

Anthropic cho biết Claude đã làm phần lớn công việc một cách tự động trong 11 ngày, tạo ra khoảng 30.300 định lý, trong đó 29.511 định lý được sử dụng trong chứng minh cuối cùng. Toàn bộ dự án tạo ra khoảng 13 triệu dòng mã Lean, lớn hơn 5 lần quy mô thư viện Mathlib mà chứng minh dựa vào.

Hàng chục tác tử Claude cùng thực hiện

Thành quả này cũng không đến từ một phiên Claude đơn lẻ.

Anthropic sử dụng một hệ thống đa tác tử AI dựa trên Claude Code. Trong đó, hàng chục tác tử Claude cùng tham gia định nghĩa khái niệm, chứng minh các định lý trung gian và kết nối chúng thành chuỗi lập luận hoàn chỉnh.

Những nỗ lực ban đầu không thành công. Các tác tử AI có thể chứng minh từng phần nhưng nhanh chóng mất dấu trạng thái chung của dự án, dẫn tới việc phối hợp kém hiệu quả và làm lại công việc của nhau. Khoảng 7% số dòng mã không phải mã mẫu trong bản chứng minh cuối cùng đến từ những nỗ lực thất bại này.

Bước ngoặt đến khi nhóm chuyển sang Prove2Me, nền tảng hình thức hóa toán học cộng tác do Tianyi Peng - nhà nghiên cứu Anthropic - cùng các cộng sự tại Đại học Columbia (Mỹ) phát triển.

Prove2Me tổ chức dự án dưới dạng một đồ thị có hướng không chu trình gồm các định lý và quan hệ phụ thuộc giữa chúng. Nhờ đó, các tác tử AI có thể biết định lý nào đã hoàn thành, định lý nào cần chứng minh và kết quả nào có thể tái sử dụng. Cách tổ chức này cũng cho phép nhiều tác tử AI làm việc song song mà ít bị mất trạng thái của dự án.

Nền tảng còn tách phần phát biểu định lý khỏi phần chứng minh để giảm chi phí biên dịch Lean, đồng thời gắn mỗi định lý với mô tả bằng ngôn ngữ tự nhiên để các tác tử AI dễ tìm kiếm và tái sử dụng kết quả đã có.

Tianyi Peng đứng sau hệ thống điều phối

Tianyi Peng là người khởi xướng thử nghiệm dùng Claude để hình thức hóa Định lý lớn Fermat. Anthropic cho biết Tianyi Peng và nhóm nghiên cứu của ông tại Đại học Columbia phát triển các công cụ phục vụ việc hình thức hóa toán học bằng AI.

Tianyi Peng hiện là trợ lý giáo sư tại Trường Kinh doanh Columbia, thuộc bộ phận Ra quyết định, Rủi ro và Vận hành.

Đáng chú ý, Tianyi Peng có bằng tiến sĩ từ Viện Công nghệ Massachusetts (Mỹ) và bằng cử nhân khoa học máy tính tại Đại học Thanh Hoa (Trung Quốc), nơi ông được tuyển vào Lớp Yao, chương trình đào tạo khoa học máy tính tinh hoa do giáo sư Andrew Yao khởi xướng.

Tianyi Peng cùng Shuze Chen, Kunal Marwaha, Xiaoyang Lu và Henry Yuen là các tác giả của nghiên cứu Prove2Me: An Open Collaborative Platform for Scaling Math Formalization, được công bố trên trang arXiv cuối tháng 8/2026. Nghiên cứu đề xuất mô hình trong đó con người và các tác tử AI có thể cùng tham gia hình thức hóa toán học quy mô lớn, với tính đúng đắn cuối cùng được máy tính kiểm tra.

Trong chiến dịch hình thức hóa toàn bộ chứng minh Định lý lớn Fermat, vai trò của Tianyi Peng không phải trực tiếp viết hàng triệu dòng mã Lean. Anthropic cho biết đóng góp của ông chủ yếu là những chỉ dẫn cấp cao, chẳng hạn ưu tiên xây dựng một khái niệm hoặc đẩy nhanh việc hoàn thành định lý quan trọng.

Máy tính kiểm tra đến đâu?

Mã nguồn của dự án hiện đã được Anthropic công khai trên GitHub. Kho mã cho biết chứng minh được xây dựng bằng phiên bản Lean 4.33.1 và Mathlib 4.33.0. Lean là phần mềm giúp kiểm tra các chứng minh toán học bằng máy tính. Mathlib là thư viện mã nguồn mở chứa một lượng lớn định nghĩa, định lý và công cụ toán học được hình thức hóa cho Lean.

Bản dựng hoàn chỉnh gồm 60.475 mô-đun, tức các phần mã được chia nhỏ để tổ chức và kiểm tra. Lean đã kiểm tra mọi khai báo trong các mô-đun đó.

Dự án còn được kiểm tra bằng comparator. Công cụ này đối chiếu phát biểu Định lý lớn Fermat của dự án với phiên bản tương ứng trong Mathlib, đồng thời kiểm tra rằng các hằng số được sử dụng và toàn bộ chứng minh đều vượt qua quá trình kiểm tra của Lean kernel.

Lean kernel là bộ phận kiểm tra cốt lõi của Lean, có nhiệm vụ xác nhận rằng chứng minh do con người hoặc AI tạo ra thực sự tuân thủ các quy tắc logic của hệ thống không.

Một bộ kiểm tra độc lập khác có tên nanoda, được viết bằng Rust, cũng kiểm tra bản xuất của môi trường Lean. Bộ kiểm tra này đã chấp nhận 1.052.234 khai báo mà không phát hiện lỗi.

Điều này cho thấy sự khác biệt quan trọng giữa câu trả lời toán học do AI tạo ra và một chứng minh hình thức. Với câu trả lời thông thường, chuyên gia phải đọc và đánh giá xem lập luận có hợp lí hay không. Với chứng minh hình thức, từng bước được viết theo một ngôn ngữ mà máy tính có thể hiểu, rồi được hệ thống kiểm tra dựa trên các quy tắc logic rõ ràng.

Từ Fermat đến tương lai AI làm toán

Anthropic cho biết toàn bộ chiến dịch đã sử dụng khoảng 6 tỉ token đầu ra từ một mô hình nghiên cứu đa dụng nội bộ, có năng lực tương đương Claude Fable 5.1. 11 ngày là khoảng thời gian một hệ thống gồm nhiều tác tử AI được phối hợp để hoàn thành nhiệm vụ.

Kevin Buzzard, giáo sư tại Đại học Imperial College London (Anh) và là người dẫn dắt dự án cộng đồng kéo dài nhiều năm nhằm hình thức hóa Định lý lớn Fermat bằng Lean, đã xem xét bản chứng minh Lean của Anthropic. Ông đánh giá đây là thành tựu đáng chú ý trong lĩnh vực tự động hình thức hóa, đồng thời cho rằng các kết quả do AI tạo ra đã đủ đáng tin cậy để những người khác có thể tiếp tục phát triển dựa trên đó.

Theo Anthropic, trong một thí nghiệm nhỏ sau đó, ba tài khoản Claude Max cá nhân đã phối hợp hoàn toàn thông qua Prove2Me để hình thức hóa Định lý ba số nguyên tố của Vinogradov trong ba ngày. Kết quả này cho thấy thành công với Fermat có thể không chỉ là một trường hợp cá biệt.

Ý nghĩa lớn hơn của câu chuyện là AI có thể trở thành một lớp kiểm chứng cho toán học. Khi các mô hình AI ngày càng tạo ra nhiều chứng minh hơn, con người sẽ khó tự kiểm tra tất cả từng bước. Một chứng minh hình thức đi kèm có thể giúp máy tính xác nhận các bước suy luận có tuân thủ quy tắc logic hay không, trong khi con người vẫn có thể đọc phần giải thích toán học theo cách thông thường.