Image: generated by METAL AI
Summary
- Anthropic announced on September 4 that it used Claude to fully formalize Fermat's Last Theorem into a form a computer can verify
- Claude worked almost autonomously for 11 days, writing 13 million lines of Lean code and using 29,500 of the 30,300 intermediate lemmas it proved in the final proof
- Kevin Buzzard of Imperial College London said the work holds up without relying on any assumptions beyond the axioms of mathematics
Anthropic announced on September 4 that it used its AI model Claude to fully formalize Fermat's Last Theorem for the first time into a form a computer can check line by line. Working almost autonomously for 11 days with minimal human intervention, Claude produced 13 million lines of code in the proof language Lean, proving 29,500 intermediate lemmas along the way to complete the final proof. Mathematicians had originally expected the task to take years, which is why the result is making waves.
What is Fermat's Last Theorem
In 1637, Pierre de Fermat scribbled a note in the margin of a copy of Diophantus's Arithmetica. He claimed that for any exponent n greater than 2, there are no positive integers a, b, c satisfying a^n + b^n = c^n. He added that he had a proof but no room to write it down — and no one else managed to produce one for more than 350 years. Countless attempts followed until Andrew Wiles finally delivered a 129-page proof in 1995. Along the way, in 1908, a prize worth $1–2 million in today's money was offered for a correct solution, and in just the first year 621 incorrect submissions poured in. Even Wiles's own proof, once published, was found to have a serious gap during verification, and he needed another year to fix it.
A decade later, Dutch computer scientist Jan Bergstra proposed formalizing that proof — converting human-readable logic into something a computer could verify. Since 2024, Kevin Buzzard of Imperial College London has led a multi-year community effort using the Lean proof assistant, and the blueprint document covering just the early stages of that work already ran to 86 pages.
To put it plainly: Andrew Wiles's 129-page proof, completed by hand in 1995, took human reviewers months just to check. Formalization means rewriting that same proof in Lean, a language a computer can verify line by line. Anthropic handed this formalization task to Claude, and it was done in 11 days — a result that echoes a warning Terence Tao raised last month, that AI could end up serving as the gatekeeper verifying mathematical achievements.
What Claude did over 11 days
Tianyi Peng, an Anthropic researcher who studies AI formalization tools at Columbia University, decided to test whether Claude could make progress on formalizing FLT. The result far exceeded his expectations. In 11 days, Claude completed a fully computer-verified proof from start to finish, proving 30,300 lemmas in the process and using 29,500 of them in the final proof. Dozens of Claude agents worked together, defining concepts, proving intermediate lemmas, and progressively tackling harder propositions.
Claude's proof followed the simplified version of Wiles's proof laid out by Darmon, Diamond, and Taylor. Human involvement was limited to occasional high-level guidance from Tianyi Peng — suggestions like "it seems like a priority to treat the Jacobian as a scheme."
| Comparison | Wiles's proof (1995) | Claude's formalization (2026) |
|---|---|---|
| Length | 129 pages | 13 million lines of Lean code |
| Verification time | Months (human review) | 11 days (autonomous AI work) |
| Intermediate lemmas | Not separately tallied | 29,500 used (30,300 produced) |
A rough start, then Prove2Me
The process wasn't smooth from the beginning. In early attempts, the agents made some progress but soon lost track of their work state and failed to collaborate effectively. Those failed attempts ended up accounting for about 7% of the non-boilerplate code in the final proof.
The turning point came when the project moved to a platform called Prove2Me. Built by Tianyi Peng and his Columbia University colleagues as an open collaboration platform, it helped in three ways: it maintained a directed acyclic graph (DAG) of theorem statements so agents could figure out what to prove next; it separated theorem statements from their proofs into different files to speed up Lean compilation; and it attached natural-language descriptions to each theorem to make them easier to search and reuse.
Anthropic shared the completed proof with Kevin Buzzard, who offered this assessment:
"This remarkable feat of automated formalization proves Fermat's Last Theorem, with no assumptions beyond the axioms of mathematics." — Kevin Buzzard (Imperial College London)
The proof code is public
The full Lean code and proof graph are available in the github.com/anthropics/fermats-last-theorem repository. Mathematicians and developers alike can browse the actual sequence in which Claude built up its theorems, line by line.
The Riemann Hypothesis, and the questions that follow
This isn't the first time Anthropic has set Claude loose on a major math problem. Last month, using a research version of Claude not available to the public, the company reported raising the known lower bound on the proportion of zeros of the zeta function — progress on the Riemann Hypothesis. Building on that momentum, Fields Medalist Terence Tao warned in an essay for the International Congress of Mathematicians that AI could trigger disruption in the math community on the scale of the foundational crisis of the early 1900s. His point wasn't about mathematical truth itself being at risk, but about the implicit value system that decides what counts as an achievement and who gets credit for it — a system he says is now being tested.
Editor's take
What's genuinely new in this announcement isn't the proof — it's the verification. The recent Riemann Hypothesis work was aimed at producing new mathematical discovery, but this FLT formalization was about taking a result already proven 30 years ago and having a computer confirm it beyond any shadow of doubt. Anthropic itself emphasizes this distinction: believing something is logically correct and actually checking it the way you'd verify a calculation are two very different things.
The generational comparison makes the point vivid. Two months after Wiles published his proof, a reviewer's single question exposed a fatal gap, and patching it took a full year. That's a reminder of how fundamentally limited human verification is when it comes to following 129 pages of logic by eye. Claude broke the same logic down into 13 million lines of machine-verified code, with Lean automatically confirming every single link in the chain. In effect, a machine filled in the gaps a human might have missed.
Practically speaking, this event sends two kinds of signals — one to mathematics researchers, and another to everyone in knowledge-work fields watching this trend. For mathematicians, there's now a tool that could cut down the years it typically takes to verify new results. For other fields, it's a precedent showing that AI can formally reconstruct complex logical structures that are too unwieldy for humans to verify on their own. It's worth remembering, though, that even here, the early attempts saw agents lose track of state and fail to collaborate — evidence that without solid infrastructure (like Prove2Me's state-management tools), autonomous AI agents can quickly go off the rails.
In the coming weeks, we're likely to see more cases of this same approach applied to other hard problems. OpenAI has also recently claimed to have solved a long-unsolved math problem, suggesting the two companies may be heading toward a competition over mathematical formalization and proof verification as well.
Comments