Key Takeaways
Anthropic said Claude produced the first end-to-end, computer-checked proof of Fermat's Last Theorem, written in the Lean proof assistant over 11 days of largely autonomous work.
The formalization runs to 13 million lines of Lean code and proves 29,500 intermediate theorems, making it the largest formal math proof ever constructed.
Kevin Buzzard, the mathematician who reviewed it, said AI autoformalization is now robust enough for the field to build on, which points toward faster checking of AI-generated math.
Anthropic said on September 4 that its Claude model produced the first complete, computer-checked proof of Fermat's Last Theorem, one of the most famous problems in the history of mathematics. Claude worked largely autonomously over 11 days, writing the proof in Lean, a language that lets a computer verify every logical step.
Fermat scribbled the claim in a book margin around 1637, that no positive whole numbers satisfy a to the n plus b to the n equals c to the n when n is greater than two. It stayed unproven for more than 350 years. Andrew Wiles published the first correct proof in 1995, running to 129 pages that took other mathematicians months to check.
The new work does not find fresh mathematics. It formalizes Wiles's argument so a machine can confirm it beyond doubt. Anthropic said dozens of Claude agents worked in parallel through Prove2Me, an open platform built by researcher Tianyi Peng and collaborators at Columbia University, consuming about 6 billion tokens. The result, posted to GitHub, is 13 million lines of Lean code, more than five times the size of Mathlib, the community proof library it builds on, and the largest formal proof ever constructed.
Claude proved 30,300 theorems along the way and used 29,500 in the final proof, which relies only on Lean's three standard axioms. Kevin Buzzard, the Imperial College London mathematician who has led a multi-year effort to formalize the theorem, reviewed the work.
"AI autoformalization artefacts are now robust enough to be built upon," said Kevin Buzzard, Imperial College London.
The bigger point is about trust. As AI systems generate more proofs than people can review, machine-checkable formalization offers a way to confirm the work is right, the same verification question that runs through how the FDA plans to test generative AI medical devices and why OpenAI has kept its largest frontier training run on hold over a safety threshold. The pattern here is hard to ignore.
People Also Ask
Did AI really prove Fermat's Last Theorem?
Not from scratch. Andrew Wiles proved it in 1995. Anthropic said Claude formalized that proof in Lean so a computer could verify every step, the first time this has been done end to end.
What is a Lean proof and why does formalization matter?
Lean is a proof assistant that checks mathematical logic automatically. Formalization rewrites a human proof into code Lean can verify, which removes doubt about hidden errors.
How long did Claude take to formalize Fermat's Last Theorem?
Anthropic said Claude completed the proof in 11 days of largely autonomous work, a task human experts had expected to take years.
Why does an AI-checked math proof matter for the rest of AI?
As AI produces more results than people can review by hand, automatic formalization gives a way to confirm they are correct, which could speed up trustworthy math and science.
Sources: Anthropic (research post, September 4, 2026), the anthropics/fermats-last-theorem repository on GitHub, and the Lean proof assistant and Imperial College London FLT project.