Claude Viết 13 Triệu Dòng Lean Trong 11 Ngày Để Máy Kiểm Chứng Định Lý Lớn Fermat
Ngày 4/9/2026, Anthropic công bố Claude đã hoàn tất bản chứng minh Định lý lớn Fermat đầu tiên được máy kiểm chứng trọn vẹn từ đầu đến cuối: 13 triệu dòng mã Lean, 30.300 định lý trung gian, khoảng 6 tỷ token đầu ra, trong 11 ngày. Nhưng Claude không khám phá ra chứng minh nào — nó dịch chứng minh n
Ngày 4/9/2026, Anthropic công bố một con số dễ gây choáng: Claude đã viết 13 triệu dòng mã Lean trong 11 ngày để tạo ra bản chứng minh Định lý lớn Fermat đầu tiên được máy kiểm chứng trọn vẹn. Con số là thật và đã được một nhà toán học độc lập rà soát. Điều nó chứng minh, và điều nó không chứng minh, lại là hai chuyện rất khác nhau.
Điều Anthropic đã công bố
Định lý lớn Fermat — không tồn tại ba số nguyên dương a, b, c thoả an + bn = cn với n lớn hơn 2 — được Pierre de Fermat nêu năm 1637 và chỉ được chứng minh năm 1995 bởi Andrew Wiles, với phần bổ khuyết làm cùng Richard Taylor. Bản chứng minh đó dài hàng trăm trang và dựa trên một tầng dày các kết quả khác của toán học thế kỷ 20.
"Hình thức hoá" là việc dịch một lập luận như thế sang ngôn ngữ mà trợ lý chứng minh như Lean kiểm tra được từng bước. Khi nhân Lean chấp nhận, không còn chỗ nào phải tin vào lời tác giả hay vào việc người phản biện có đọc kỹ hay không. Theo Anthropic, đây là những gì Claude đã làm:
| Hạng mục | Con số | Ghi chú |
|---|---|---|
| Thời gian | 11 ngày | Chạy phần lớn tự động, không có người can thiệp từng bước |
| Mã Lean sinh ra | 13 triệu dòng | Anthropic gọi đây là bản chứng minh Lean lớn nhất từng được viết |
| Định lý đã chứng minh | 30.300 | Trong đó 29.500 định lý được dùng trong bản chứng minh cuối |
| Token đầu ra tiêu thụ | khoảng 6 tỷ | Anthropic không công bố chi phí tiền mặt tương ứng |
| Mô hình sử dụng | Nội bộ | Một mô hình nghiên cứu chưa phát hành, năng lực đại khái tương đương Claude Fable 5.1 |
Nguồn: Anthropic, "Formalizing Fermat's Last Theorem", đăng 4/9/2026, Locaith đọc trực tiếp ngày 8/9/2026. Toàn bộ là số do hãng tự công bố, chưa có bên thứ ba đo lại.
Cách tổ chức công việc đáng chú ý không kém con số. Anthropic cho biết hàng chục tác tử Claude làm việc song song thông qua Prove2Me, một nền tảng do Tianyi Peng và các cộng sự ở Đại học Columbia thiết kế, điều phối các tác tử theo một đồ thị có hướng không chu trình các mệnh đề cần chứng minh. Nói cách khác: bài toán lớn được bẻ thành một mạng lưới các bổ đề phụ thuộc lẫn nhau, rồi phát cho các tác tử làm dần từ dưới lên.
Hình thức hoá không phải là khám phá
Đây là chỗ nhiều bản tin trượt, và cũng là chỗ Anthropic nói khá thẳng. Claude không tìm ra một chứng minh nào cả. Nó đi theo bản trình bày chứng minh Wiles năm 1995 trong phiên bản của Darmon, Diamond và Taylor — một lối đi đã có sẵn, đã được cộng đồng toán học kiểm tra suốt ba thập kỷ. Việc của Claude là dịch lối đi đó sang một ngôn ngữ mà máy kiểm được, và lấp đầy hàng chục nghìn bước trung gian mà bài báo toán học vốn để ngầm cho người đọc tự hiểu.
Sự phân biệt này không phải bắt bẻ chữ nghĩa. Nó quyết định câu trả lời cho câu hỏi mà ai cũng muốn hỏi tiếp: vậy AI đã tự làm được toán chưa? Kết quả này không trả lời câu đó. Nó trả lời một câu khác, hẹp hơn nhưng vẫn đáng giá: một hệ tác tử có thể duy trì tính nhất quán qua hàng chục nghìn bước suy luận hình thức, trong nhiều ngày, mà không trôi khỏi mục tiêu. Với bất kỳ ai từng xem một mô hình ngôn ngữ lạc đề sau ba mươi bước, đó là một dữ kiện đáng chú ý.
Vì sao "máy kiểm được" lại quan trọng hơn "AI nói rằng đúng".
Khi Claude viết một đoạn văn giải thích toán, bạn phải tin nó. Khi Claude viết mã Lean và nhân Lean chấp nhận, bạn không cần tin nó — bạn chỉ cần tin nhân Lean, một chương trình nhỏ, ổn định, đã được soi kỹ trong nhiều năm. Đây là mô hình hiếm hoi trong đó đầu ra của AI có thể được kiểm chứng độc lập bằng máy, không cần chuyên gia đọc lại. Nếu bạn đang tìm chỗ để giao việc cho AI mà vẫn ngủ ngon, hãy tìm những chỗ có tính chất này.
Cái giá, và những vết sẹo còn nằm trong mã
Anthropic tự nêu hai hạn chế, và cả hai đều đáng đọc kỹ.
- Bản chứng minh dài gấp khoảng năm lần Mathlib — thư viện toán học chuẩn của cộng đồng Lean, thành quả tích luỹ nhiều năm của hàng trăm người. Anthropic nói thẳng rằng điều này gợi ý bản chứng minh có thể dài hơn mức cần thiết. Nhân Lean không chấm điểm văn phong; nó chỉ trả lời đúng hoặc sai.
- Khoảng 7% số dòng không phải mã khuôn mẫu đến từ những hướng thử thất bại. Nghĩa là trong 13 triệu dòng có một phần là ngõ cụt còn sót lại — dấu vết của quá trình mò mẫm, chưa được dọn.
- Mô hình dùng ở đây không bán. Anthropic mô tả đó là một mô hình nghiên cứu nội bộ, năng lực đại khái tương đương Claude Fable 5.1. Bạn không thể mở API và làm lại thí nghiệm này.
Điểm phê bình có sức nặng nhất không nằm ở tính đúng đắn mà ở khả năng dùng lại. Một bản phân tích đăng ngày 6/9/2026 nêu đúng chỗ này: được nhân Lean chấp nhận khác với việc tạo ra thứ toán học mà cộng đồng còn đọc được, bảo trì được và ghép vào thư viện chung được. Mathlib có giá trị vì người khác dùng lại được từng mảnh của nó. Một khối 13 triệu dòng chứng minh đúng một định lý thì đóng được định lý đó, nhưng chưa chắc để lại hạ tầng gì cho người sau.
Dự án của con người vẫn chạy tới 2029 — và không làm cùng một việc
Một câu hỏi tự nhiên: vậy dự án hình thức hoá Định lý lớn Fermat do con người làm còn ý nghĩa gì? Câu trả lời là hai bên không đi cùng một đường và không nhắm cùng một đích.
| Anthropic / Claude | Dự án FLT (Imperial College London) | |
|---|---|---|
| Người dẫn | Hệ tác tử Claude, có người giám sát | Kevin Buzzard, dự án mở nhiều tác giả |
| Đi theo bản nào | Bản trình bày 1995 của Darmon, Diamond và Taylor | Biến thể hiện đại của Wiles/Taylor-Wiles, dựa nhiều vào ý tưởng của Khare và Wintenberger |
| Thời gian | 11 ngày | Được EPSRC tài trợ theo đề tài EP/Y022904/1 đến tháng 9/2029 |
| Mục tiêu | Đóng định lý, đầu-đến-cuối, máy kiểm được | Xây thư viện dùng lại được cho toán học hiện đại |
Nguồn: Anthropic (4/9/2026) và kho mã dự án FLT của Imperial College London trên GitHub, Locaith đọc ngày 8/9/2026.
Nói cho công bằng với cả hai bên: Claude đóng được một cánh cửa mà giới toán học tưởng còn mất nhiều năm mới đóng, và Kevin Buzzard — người đang được tài trợ để làm việc đó bằng tay — chính là người đã rà soát kết quả và gọi nó là "thành tựu tự động hình thức hoá phi thường", nói rằng nó "chứng minh Định lý lớn Fermat mà không cần giả thiết nào ngoài các tiên đề của toán học". Nhưng dự án của ông đi lối hiện đại hơn và nhắm tới một thứ khác: một nền móng mà các nhà toán học sau còn xây tiếp lên được.
Điều doanh nghiệp nên rút ra
Không doanh nghiệp Việt Nam nào sắp phải hình thức hoá một định lý. Nhưng cấu trúc của thí nghiệm này thì áp dụng được, và nó nói điều gì đó cụ thể hơn nhiều so với một tiêu đề về toán học.
- Việc hợp với AI nhất là việc có máy chấm. Điều làm 11 ngày này khả thi không phải mô hình thông minh hơn, mà là mỗi bước đều có một trọng tài không thiên vị trả lời đúng/sai ngay lập tức. Trong doanh nghiệp, những chỗ có tính chất đó là: mã có bộ kiểm thử, dữ liệu có ràng buộc lược đồ, văn bản có mẫu bắt buộc, sổ sách có phép đối chiếu. Hãy giao AI vào đó trước, thay vì vào những việc chỉ con người mới nói được là đúng hay sai.
- Chia nhỏ theo đồ thị phụ thuộc, đừng giao một khối lớn. Prove2Me không thắng vì có mô hình tốt hơn; nó thắng vì bẻ bài toán thành mạng lưới mệnh đề nhỏ có thể kiểm riêng và ghép lại. Cùng một mô hình, cùng một ngân sách token, cách chia việc quyết định kết quả.
- Đọc kỹ mô hình nào đã làm ra kết quả. Kết quả này dùng mô hình nội bộ chưa phát hành và khoảng 6 tỷ token đầu ra. Khi một hãng công bố năng lực gây choáng, câu hỏi đầu tiên nên là: bản này có bán không, và chạy hết bao nhiêu? Nếu câu trả lời là "chưa" và "không công bố", thì đó là mốc nghiên cứu, chưa phải thứ đưa vào kế hoạch năm sau được.
Nguồn:
- Anthropic — Formalizing Fermat's Last Theorem, đăng 4/9/2026 — nguồn sơ cấp cho toàn bộ con số, cho Prove2Me, cho việc dùng mô hình nội bộ, cho các hạn chế tự nêu và cho trích dẫn của Kevin Buzzard; Locaith đọc trực tiếp 8/9/2026
- Anthropic — Formalizing Fermat's Last Theorem in Lean (bản PDF kỹ thuật) — tài liệu đi kèm bài công bố
- Imperial College London — Kho mã dự án FLT — nguồn cho việc dự án do Kevin Buzzard dẫn dắt, cho mã đề tài EPSRC EP/Y022904/1 và mốc tháng 9/2029, và cho việc dự án đi theo biến thể hiện đại dựa trên ý tưởng của Khare và Wintenberger; Locaith đọc 8/9/2026
- Remio — Anthropic Claude Formalized Fermat's Last Theorem. It Did Not Discover the Proof, đăng 6/9/2026 — nguồn cho lập luận phê bình về khả năng dùng lại và cho phân biệt giữa hình thức hoá và khám phá
Mọi con số trong bài đều do Anthropic tự công bố và chưa có bên thứ ba độc lập đo lại — riêng tính đúng đắn của bản chứng minh thì được nhân Lean kiểm chứng bằng máy, đó là một dạng bảo đảm khác và mạnh hơn ý kiến chuyên gia. Kevin Buzzard rà soát kết quả với tư cách nhà toán học độc lập, đồng thời ông cũng là người dẫn dắt dự án hình thức hoá cạnh tranh — Locaith nêu cả hai vai trò để bạn đọc tự cân nhắc. Câu trích của Kevin Buzzard được lấy từ chính bài công bố của Anthropic, không phải từ phỏng vấn riêng. Chi phí tiền mặt của thí nghiệm chưa công bố; bài này không ước tính thay. Ba khuyến nghị cuối bài là quan điểm riêng của Locaith. Ảnh bìa và sơ đồ cấu trúc chứng minh: Anthropic, lấy từ chính bài công bố. Biên soạn và phân tích bởi Ban Biên Tập Locaith, 8/9/2026.