Claude chứng minh Định lý cuối cùng Fermat bằng Lean như thế nào?

Ngày 4/9/2026, Anthropic công bố một cột mốc đáng chú ý của AI trong toán học: Claude đã làm việc phần lớn tự động trong 11 ngày để tạo một bản formalization của Định lý cuối cùng Fermat bằng Lean. Theo Anthropic, kết quả là proof đầu tiên của định lý này có thể được máy tính kiểm tra từ đầu đến cuối. Đây là một bước tiến lớn về formal verification, nhưng cần hiểu đúng Claude đã làm gì và chưa làm gì.

Claude không tìm ra một định lý mới và cũng không thay thế công trình của Andrew Wiles. Công việc mới nằm ở việc biến một chuỗi lập luận toán học cực kỳ phức tạp thành mã Lean đủ chi tiết để proof assistant kiểm tra từng bước. Sự khác biệt này rất quan trọng nếu muốn đánh giá đúng ý nghĩa của kết quả.

Anthropic vừa công bố gì về Claude và Định lý Fermat?

Trong bài nghiên cứu Formalizing Fermat’s Last Theorem đăng ngày 4/9/2026, Anthropic cho biết Claude đã tạo một proof end-to-end được Lean kiểm tra. Công ty gọi đây là bản computer-checked proof hoàn chỉnh đầu tiên của Fermat’s Last Theorem.

Theo số liệu Anthropic công bố, Claude mất 11 ngày, viết khoảng 13 triệu dòng Lean và tạo proof cho 30.300 theorem trong quá trình làm việc. Trong proof cuối cùng có khoảng 29.500 theorem được sử dụng. Quy mô này lớn bất thường: Anthropic nói artifact dài hơn 5 lần Mathlib, thư viện toán học cộng đồng chính mà dự án dựa vào.

Một điểm đáng chú ý khác là mức độ tự chủ. Anthropic mô tả Claude làm việc largely autonomously; con người chỉ đưa một số chỉ dẫn cấp cao theo từng thời điểm, chẳng hạn ưu tiên một nhánh toán học hoặc thúc đẩy một theorem quan trọng. Phần lớn việc phân rã, tìm lemma, viết Lean và kết nối các proof do hệ thống agent thực hiện.

Claude có thực sự “giải lại” Định lý cuối cùng Fermat từ đầu?

Không. Cách nói chính xác hơn là Claude đã formalize một proof của Định lý cuối cùng Fermat để máy tính có thể kiểm tra. Định lý đã được Andrew Wiles chứng minh trong thập niên 1990, với phần sửa chữa quan trọng cùng Richard Taylor; proof hoàn chỉnh được công bố năm 1995.

Anthropic cho biết artifact của Claude đi theo một phiên bản đơn giản hóa của hướng chứng minh Wiles được trình bày bởi Henri Darmon, Fred Diamond và Richard Taylor. Dự án cũng tận dụng một số phần từ dự án FLT tại Imperial College London và các formalization có sẵn. Vì vậy, novelty nằm ở quy mô và tốc độ autoformalization, không phải ở việc khám phá ra chân lý toán học mới.

Formalization khác mathematical discovery ở đâu?

Mathematical discovery tìm ra định lý, cấu trúc hoặc proof mới mà trước đó chưa biết. Formalization lấy một phát biểu hoặc proof đã có rồi diễn đạt lại bằng ngôn ngữ hình thức sao cho một kernel kiểm chứng có thể xác nhận mọi bước suy luận tuân theo các tiên đề và quy tắc logic.

Hai công việc có liên quan nhưng không đồng nhất. Một AI có thể rất giỏi formalization mà chưa chắc tìm được proof mới; ngược lại, một proof tự nhiên rất sáng tạo vẫn có thể khó formalize. Kết quả Fermat của Claude chủ yếu là bằng chứng cho năng lực thứ nhất.

Định lý cuối cùng Fermat là gì và vì sao proof này nổi tiếng?

Fermat’s Last Theorem 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^n + b^n = c^n với số nguyên n lớn hơn 2. Pierre de Fermat ghi lại khẳng định này khoảng năm 1637 và nói rằng ông có một proof “kỳ diệu”, nhưng phần lề quá hẹp để viết ra.

Bài toán tồn tại hơn 350 năm trước khi Wiles công bố hướng giải năm 1993. Sau khi một lỗ hổng được phát hiện trong quá trình kiểm tra, Wiles và Taylor mất thêm thời gian để sửa. Bản proof đúng được công bố năm 1995 và dựa vào hàng loạt công cụ hiện đại của số học và hình học đại số.

Chính sự chênh lệch giữa một phát biểu rất ngắn và một proof cực kỳ sâu khiến FLT trở thành benchmark hấp dẫn cho formal mathematics. Máy tính không chỉ cần hiểu câu kết luận; nó phải được cung cấp toàn bộ cây phụ thuộc của hàng nghìn kết quả trung gian.

Formalized mathematics và computer-checked proof là gì?

Formalized mathematics là cách biểu diễn định nghĩa, theorem và proof trong một hệ thống logic hình thức. Thay vì chỉ đọc câu chữ như một nhà toán học, phần mềm có thể kiểm tra chính xác proof có tuân thủ các quy tắc suy luận hay không.

Trong dự án này, hệ thống kiểm chứng là Lean. Lean vừa là programming language vừa là interactive theorem prover. Các theorem được viết thành những phát biểu formal, còn proof phải đủ chi tiết để Lean kernel xác minh.

Một proof dành cho con người thường bỏ qua nhiều bước được xem là hiển nhiên. Lean không được phép “tin” vào trực giác đó. Mỗi định nghĩa, chuyển đổi, điều kiện biên và theorem phụ đều phải nối thành chuỗi logic hợp lệ. Đây là lý do formalization của toán học hiện đại thường tốn khối lượng công việc khổng lồ.

“Computer-checked” có nghĩa là máy tính đã tự hiểu proof như con người?

Không hẳn. Computer-checked nghĩa là sau khi proof được biểu diễn trong Lean, kernel của Lean kiểm tra rằng các bước formal suy ra đúng kết luận theo hệ tiên đề đã chọn. Máy không cần có trực giác toán học giống con người để làm bước kiểm tra này.

Anthropic cho biết artifact cuối dùng ba tiên đề chuẩn của Lean và một bộ so sánh xác nhận phát biểu theorem ở đỉnh proof khớp với phát biểu Fermat’s Last Theorem trong Mathlib. Điều đó giúp giảm rủi ro kiểu “chứng minh đúng một phát biểu khác với thứ mọi người tưởng đang chứng minh”.

Claude đã formalize Định lý Fermat bằng kiến trúc nào?

Điểm đáng chú ý nhất không chỉ là model, mà là scaffolding bao quanh model. Anthropic dùng Prove2Me cùng một multi-agent harness dựa trên Claude Code. Nhiều agent cùng xử lý các theorem nhỏ hơn, tìm dependency và xây dần lên mục tiêu cuối.

Prove2Me biến proof lớn thành một DAG theorem

Prove2Me tổ chức dự án thành directed acyclic graph (DAG): theorem lớn phụ thuộc vào các theorem nhỏ hơn, các theorem nhỏ lại có dependency riêng. Agent có thể nhìn vào graph để biết phần nào đang mở, phần nào đã được chứng minh và phần nào nên xử lý tiếp.

Theo Anthropic, cấu trúc này giải quyết ba bài toán thực tế: duy trì trạng thái để agent không quên toàn bộ chiến dịch, giảm chi phí biên dịch bằng cách tách statement và proof, và hỗ trợ tìm kiếm/tái sử dụng theorem thông qua mô tả ngôn ngữ tự nhiên.

Nhiều agent phối hợp thay vì một Claude chạy đơn lẻ

Hàng chục agent cùng định nghĩa khái niệm, chứng minh theorem trung gian và tái sử dụng kết quả của nhau. Đây là một ví dụ rõ về việc năng lực hệ thống có thể tăng mạnh khi một model được đặt trong workflow có phân rã nhiệm vụ, memory/state và verification loop tốt.

Anthropic cũng thừa nhận các thử nghiệm ban đầu thất bại: agent mất dấu trạng thái dự án và phối hợp kém. Những nỗ lực không thành công vẫn đóng góp khoảng 7% số dòng non-boilerplate trong artifact cuối. Điều này cho thấy orchestration không phải phần phụ; nó là điều kiện để workload dài ngày hoạt động.

Model nào đã được dùng và tốn bao nhiêu compute?

Anthropic nói chiến dịch tiêu thụ khoảng 6 tỷ output tokens từ một internal general-purpose research model có năng lực roughly comparable to Claude Fable 5.1. Cách diễn đạt này không nên được hiểu là toàn bộ proof được tạo trực tiếp bằng đúng model thương mại Claude Fable 5.1 đang bán cho người dùng.

Nếu muốn tìm hiểu model Fable 5.1 mà Anthropic dùng làm mốc so sánh, Bot.io.vn đã có bài Claude Fable 5.1 là gì?. Bài Fermat này tập trung vào workflow formal mathematics, không phải review model.

Vì sao con số 11 ngày đáng chú ý?

Formalizing FLT lâu nay được xem là một dự án nhiều năm. Dự án cộng đồng do Kevin Buzzard dẫn dắt tại Imperial College London bắt đầu một nỗ lực quy mô lớn từ năm 2024, và blueprint chỉ cho giai đoạn đầu đã dài hàng chục trang.

Trong bối cảnh đó, việc một hệ thống agent đi từ dependency graph đến end-to-end Lean proof trong chưa đầy hai tuần là khác biệt về tốc độ. Anthropic báo cáo 30.300 theorem được formalize/prove trong quá trình, 29.500 theorem đi vào artifact cuối và tổng mã Lean đạt khoảng 13 triệu dòng.

Tuy nhiên, nhiều dòng code không đồng nghĩa proof đẹp hơn. Anthropic tự lưu ý artifact có thể dài hơn mức cần thiết, trong khi Mathlib được con người biên tập rất chặt. Vì vậy, 13 triệu dòng nên được đọc như một chỉ báo về khả năng hoàn thành workload khổng lồ, không phải thước đo tối ưu về chất lượng mã.

Kevin Buzzard đã đánh giá proof của Claude như thế nào?

Anthropic đã gửi artifact cho Kevin Buzzard, người dẫn dự án formalization FLT tại Imperial. Buzzard nhận xét rằng kết quả chứng minh Fermat’s Last Theorem mà không cần giả định ngoài các tiên đề toán học chuẩn và cho thấy các artifact autoformalization đã đủ vững để xây tiếp lên trên.

Đây là sự xác nhận quan trọng từ một chuyên gia trực tiếp làm FLT formalization. Dù vậy, nên phân biệt giữa ba lớp: Anthropic là bên tạo và công bố artifact; Lean kernel là cơ chế machine verification; còn review của Buzzard là đánh giá chuyên môn từ bên ngoài nhóm triển khai.

Dự án công khai của Imperial tại GitHub là một nỗ lực riêng, xây dựng formalization theo lộ trình cộng đồng. Artifact của Anthropic không đơn giản là “Imperial project chạy nhanh hơn”; nó sử dụng proof path và scaffolding riêng, dù có tái sử dụng một số thành phần.

Kết quả này có ý nghĩa gì với AI for Science?

Giá trị lớn nhất của formalization là tạo ra một lớp kiểm tra cứng cho tri thức do con người hoặc AI tạo ra. Khi số lượng proof tăng nhanh, việc các chuyên gia phải đọc thủ công từng dòng có thể trở thành nút thắt. Proof assistant giúp chuyển một phần burden từ “tin vào người viết” sang “kiểm tra artifact formal”.

Điều này đặc biệt quan trọng với AI-generated mathematics. LLM có thể viết lập luận nghe thuyết phục nhưng chứa bước nhảy sai. Nếu lập luận được formalize và kernel chấp nhận, người đọc có một tín hiệu mạnh hơn nhiều so với prose tự nhiên.

Anthropic kỳ vọng formal proof sẽ ngày càng đi kèm bản trình bày cho con người thay vì thay thế nó. Một bản paper vẫn cần giải thích trực giác, động cơ và ý nghĩa; Lean đảm nhiệm lớp logic có thể audit.

Đây cũng là một hướng khác của AI for Science so với mô hình dự báo. Chẳng hạn, WeatherNext 3 dùng AI để mô hình hóa hệ thống Trái Đất, còn Claude trong bài này được dùng để biến tri thức toán học thành artifact có thể kiểm chứng.

Bài toán Fermat cho thấy điều gì về AI Agent chạy dài hạn?

Một model mạnh chưa đủ để xử lý project 11 ngày với hàng chục nghìn theorem. Hệ thống cần biết project đang ở đâu, dependency nào đã hoàn thành, proof nào có thể tái sử dụng và công việc nào có thể chạy song song.

DAG trong Prove2Me đóng vai trò giống một project graph cho toán học. Nó giảm memory degradation và giúp agent chọn frontier theorem phù hợp thay vì mỗi lần lại đọc toàn bộ project. Đây là pattern rất gần với các persistent/long-running agent workflow đang xuất hiện trong coding và research.

Bot.io.vn từng phân tích một hướng liên quan trong bài Automated Alignment Researchers: khi AI được trao workflow thử nghiệm, đánh giá và lặp lại, khả năng của cả hệ thống có thể vượt xa một câu trả lời đơn lẻ của chatbot.

Những giới hạn cần nhớ trước khi gọi đây là “AI chứng minh Fermat”

• Không phải proof toán học mới: Claude formalize một proof path dựa trên công trình toán học đã biết.
• “Đầu tiên” là claim của Anthropic: nên gắn phát biểu này với nguồn công bố, dù artifact đã được Lean kiểm tra và Buzzard review.
• Chi phí rất lớn: khoảng 6 tỷ output tokens cho chiến dịch, nên chưa thể coi đây là workload rẻ hay phổ thông.
• 13 triệu dòng không đồng nghĩa code tối ưu: formalization do agent sinh có thể cần refactor, rút gọn và tổ chức lại để cộng đồng dễ bảo trì.
• Formal verification không thay thế exposition: proof formal xác nhận logic, nhưng nhà toán học vẫn cần bản giải thích dễ hiểu để học, đánh giá ý tưởng và tái sử dụng.

Một giới hạn sâu hơn là proof assistant chỉ kiểm tra những gì đã được formalize. Nếu statement được đặt sai hoặc mô hình hóa không đúng ý định, kernel có thể xác nhận một theorem hoàn toàn chính xác nhưng không phải theorem mà con người muốn. Vì vậy Anthropic nhấn mạnh việc đối chiếu statement cuối với Mathlib là một bước quan trọng.

Ai nên quan tâm tới cột mốc này?

Nhà toán học và researcher

Formalization quy mô lớn có thể giảm thời gian kiểm tra proof, tạo thư viện theorem tái sử dụng và phát hiện lỗi trong literature cũ. Nó cũng mở ra khả năng kiểm tra nhanh hơn các kết quả do AI hỗ trợ sinh ra.

Developer xây AI Agent

Case study này cho thấy state management, decomposition và verifier quan trọng ngang model. Prove2Me là ví dụ của một môi trường mà agent không chỉ “suy nghĩ”, mà còn phải tạo artifact có validator cứng xác nhận.

Doanh nghiệp và đội R&D

Thông điệp rộng hơn là workflow chuyên môn có thể được tự động hóa sâu hơn khi nhiệm vụ có ngôn ngữ hình thức và bộ kiểm tra đáng tin. Coding đã có compiler/test suite; formal mathematics có Lean; những lĩnh vực khác sẽ cần verifier tương tự nếu muốn giao việc dài ngày cho agent.

Câu hỏi thường gặp về Claude và Định lý Fermat

Claude có phát minh ra proof mới của Định lý Fermat không?

Không. Anthropic mô tả công việc là autoformalization: Claude chuyển một proof path dựa trên toán học đã biết sang Lean để máy tính kiểm tra. Proof toán học của FLT đã có từ công trình Wiles và Taylor.

Lean là gì?

Lean là một theorem prover và programming language cho phép viết các phát biểu toán học cùng proof ở dạng formal. Lean kernel kiểm tra liệu proof có thực sự suy ra theorem theo các tiên đề và quy tắc logic hay không.

Vì sao proof của Claude dài tới 13 triệu dòng?

Formal proof phải khai báo rất nhiều chi tiết mà paper cho con người thường lược bỏ. Ngoài ra artifact do agent sinh chưa được tối ưu cô đọng như thư viện do cộng đồng biên tập. Anthropic lưu ý đây là proof lớn nhất mà họ xây dựng và có thể dài hơn mức cần thiết.

Proof có được công khai không?

Anthropic cho biết full proof và written walkthrough được công khai từ bài nghiên cứu của họ. Prove2Me cũng có mission Fermat’s Last Theorem để theo dõi graph theorem và cách formalization được tổ chức.

Kết quả này có nghĩa AI đã có thể tự giải mọi bài toán khó?

Không. FLT trong trường hợp này là bài toán đã có proof, nên nhiệm vụ chủ yếu là formalization và verification. Tìm ra proof mới cho open conjecture vẫn là một loại năng lực khác và chưa thể suy ra trực tiếp từ kết quả này.

Claude model nào đã làm dự án Fermat?

Anthropic chỉ nói họ dùng một internal general-purpose research model có năng lực xấp xỉ Claude Fable 5.1. Vì vậy không nên khẳng định chính xác rằng bản Claude Fable 5.1 thương mại đã tự mình tạo toàn bộ proof.

Điều cần theo dõi tiếp theo

Cột mốc tiếp theo không chỉ là thêm những proof khổng lồ. Điều đáng theo dõi là cộng đồng có thể tái kiểm tra, rút gọn và tích hợp artifact vào các thư viện chuẩn đến đâu; các agent có giảm được chi phí token không; và workflow kiểu Prove2Me có giúp formalize literature toán học thường ngày chứ không chỉ landmark theorem hay không.

Anthropic cũng nêu một thử nghiệm nhỏ hơn: ba gói Claude Max cá nhân phối hợp qua Prove2Me đã formalize Vinogradov’s Three Primes Theorem trong ba ngày. Nếu các kết quả dạng này lặp lại với chi phí thấp hơn, autoformalization có thể trở thành công cụ thực dụng cho researcher chứ không chỉ là demo phòng lab.

Với Bot.io.vn, điểm đáng chú ý nhất không phải câu giật tít “AI giải Fermat”, mà là sự xuất hiện của một workflow nơi AI tạo ra tri thức ở dạng có thể kiểm chứng bằng máy. Đó có thể là một trong những cơ chế quan trọng để duy trì độ tin cậy khi lượng nội dung khoa học do AI tạo ra tăng nhanh.