Claude formal hóa Định lý Fermat trong 11 ngày: bài học cho đội AI Agent

Ngày 4/9/2026, Anthropic công bố Claude đã làm việc gần như tự chủ trong 11 ngày để tạo ra bản formal hóa đầu tiên từ đầu đến cuối của Định lý cuối Fermat có thể được máy tính kiểm tra.

Kết quả gồm 13 triệu dòng mã Lean và 30.300 định lý trung gian được chứng minh, trong đó 29.500 định lý được dùng trong bản cuối. Nhưng đây không phải câu chuyện “AI tự tìm ra lời giải mới” cho bài toán tồn tại hàng trăm năm. Claude đã chuyển một hướng chứng minh đã biết sang ngôn ngữ hình thức để trình kiểm chứng Lean có thể xác nhận từng mắt xích logic.

Điều đáng chú ý với doanh nghiệp nằm ở cách đội AI Agent được tổ chức: nhiều lần thử đầu thất bại khi các Agent mất dấu trạng thái chung. Hệ thống chỉ hoàn thành nhiệm vụ sau khi có một cấu trúc điều phối và kiểm chứng phù hợp.

Claude đã làm gì trong 11 ngày?

Định lý cuối Fermat phát biểu rằng 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 lớn hơn 2. Andrew Wiles công bố chứng minh nổi tiếng vào năm 1995; bản đầu dài 129 trang và từng cần một năm để sửa lỗ hổng được phát hiện trong quá trình thẩm định.

Claude không thay thế thành tựu đó. Nhóm Anthropic sử dụng một phiên bản đơn giản hóa của chứng minh Wiles, rồi giao cho hàng chục Agent chuyển toàn bộ chuỗi lập luận sang Lean—một proof assistant có thể kiểm tra logic bằng máy.

Theo Anthropic:

• Công việc hoàn tất trong 11 ngày.
• Bản formal hóa dài khoảng 13 triệu dòng Lean, hơn 5 lần kích thước Mathlib—thư viện toán học cộng đồng mà dự án dựa vào.
• Các Agent chứng minh 30.300 định lý trung gian và dùng 29.500 định lý trong bản cuối.
• Hệ thống tiêu thụ khoảng 6 tỷ output token.
• Đầu vào toán học của con người chủ yếu là các chỉ dẫn cấp cao không thường xuyên.

Vì sao các lần thử đầu thất bại?

Anthropic cho biết những lần thử ban đầu nhanh chóng mất đà: các Agent không còn theo dõi đúng trạng thái dự án và phối hợp kém hiệu quả. Những nhánh thất bại vẫn chiếm khoảng 7% số dòng không phải mã khuôn mẫu trong bản cuối.

Bước ngoặt đến khi nhóm chuyển sang Prove2Me, một nền tảng cộng tác mở cho toán học hình thức. Nền tảng này tạo ba lớp hạ tầng:

1. Một đồ thị có hướng không chu trình (DAG) để chia định lý lớn thành các định lý con và giúp Agent biết nên xử lý nhiệm vụ nào tiếp theo.
2. Cách tách phát biểu và chứng minh thành các tệp riêng, giúp biên dịch Lean nhanh hơn và giảm tiêu hao tài nguyên.
3. Mô tả bằng ngôn ngữ tự nhiên cho từng phát biểu để Agent tìm kiếm, tái sử dụng và nối các kết quả dễ hơn.

Cuối cùng, Lean kiểm tra bản chứng minh; một bộ so sánh độc lập trong quy trình cũng xác nhận phát biểu của định lý khớp với phiên bản trong Mathlib. Nhà toán học Kevin Buzzard đã xem xét kết quả và nhận định các tạo tác formal hóa đủ vững để các công trình khác xây tiếp.

Nhận định của Học viện AI: năng lực Agent phụ thuộc vào “hệ điều hành công việc”

Case này cho thấy thêm Agent hoặc dùng model mạnh hơn chưa đủ. Một đội AI chỉ tạo ra đầu ra phức tạp khi có bốn thành phần:

• Bản đồ nhiệm vụ: chia mục tiêu thành các phần phụ thuộc rõ ràng.
• Trạng thái dùng chung: mọi Agent biết việc nào đã xong, việc nào đang làm và kết quả nào được phép tái sử dụng.
• Bộ kiểm chứng xác định: đầu ra được máy hoặc quy tắc cứng kiểm tra thay vì chỉ để một model khác “cảm nhận” là đúng.
• Con người ở tầng phán quyết: chuyên gia đặt hướng, tháo nút thắt và quyết định khi nào kết quả đủ tin cậy.

Đây là cùng mô hình xuất hiện trong dữ liệu vận hành mới của OpenAI: một nhà nghiên cứu điều phối nhiều Agent chạy song song, trong khi con người vẫn giữ quyền đặt ưu tiên và phê duyệt.

Doanh nghiệp có thể áp dụng ngay như thế nào?

Không phải doanh nghiệp nào cũng cần chứng minh định lý. Nhưng quy trình xử lý hồ sơ, kiểm toán, nghiên cứu thị trường, viết phần mềm hay soạn tài liệu pháp lý đều có cấu trúc tương tự: nhiệm vụ lớn, nhiều phần phụ thuộc và yêu cầu kiểm tra nghiêm ngặt.

Trước khi triển khai nhiều Agent, doanh nghiệp nên trả lời năm câu hỏi:

1. Công việc đã được tách thành các đơn vị đủ nhỏ và có thứ tự phụ thuộc chưa?
2. Agent đọc và cập nhật trạng thái chung ở đâu?
3. Đầu ra nào có thể được kiểm tra bằng quy tắc, test, schema hoặc đối chiếu nguồn?
4. Khi nào Agent phải dừng và chuyển cho chuyên gia?
5. Doanh nghiệp đo tỷ lệ đầu ra được duyệt, chi phí và công sửa lại như thế nào?

Nếu thiếu các câu trả lời này, multi-agent có thể chỉ tạo ra nhiều hoạt động hơn, không tạo ra nhiều giá trị hơn. Khung AgentOps 7 giai đoạn là một điểm bắt đầu phù hợp để đưa thử nghiệm sang production có kiểm soát.

Doanh nghiệp của bạn đã sẵn sàng giao việc cho một đội AI Agent chưa? Làm khảo sát AI Readiness của Học viện AI để xác định điểm xuất phát và lớp vận hành còn thiếu.

Nguồn và lưu ý

Nguồn chính: Anthropic, “Formalizing Fermat’s Last Theorem”, công bố ngày 4/9/2026. Số liệu về thời gian, token và quy mô mã do Anthropic báo cáo; bản proof được công khai và kiểm tra bằng Lean. Phần diễn giải cho vận hành doanh nghiệp là nhận định của Học viện AI.