In 1637, Pierre de Fermat scribbled a claim in the margin of a book: no three positive integers a, b, c can satisfy aⁿ + bⁿ = cⁿ for any whole number n greater than 2. He added that he had a “truly marvelous proof” the margin was too narrow to contain, then died without ever writing it down. It took 358 years, and Andrew Wiles’s landmark 1995 proof, to finally settle the question.
This September, Anthropic’s Claude did something different, but arguably just as remarkable. Over 11 days of largely autonomous work, Claude converted Wiles’s proof into 13 million lines of Lean, a formal programming language in which every logical step can be checked automatically by a computer, with no step requiring a human to simply trust that it’s correct.
Proving vs. Verifying: a Crucial Distinction
It’s worth being precise about what happened here, because it’s easy to overstate. Claude did not discover new mathematics. Fermat’s Last Theorem was already proven, and mathematicians have been confident in Wiles’s argument for three decades. What Claude did was formalize that proof by translating dense, prose-based mathematical reasoning, spread across multiple papers and built on decades of number theory, into a fully machine-checkable form.
That distinction matters more than it might sound. A traditional proof is checked by human reviewers reading it line by line, a process that can take years for something as intricate as Fermat’s Last Theorem, and one broken logical link anywhere in the chain can undermine the whole argument. A formalized proof removes that uncertainty entirely: if the code compiles under Lean’s proof-checker, every step is guaranteed valid by the rules of mathematical logic itself, no human trust required.
The Scale Is the Real Story
To get there, Claude constructed roughly 30,300 supporting theorems, about 29,500 of which made it into the final proof: a body of formalized mathematics more than five times larger than Mathlib, the largest existing library of formalized math, built over years by a global community of contributors. Kevin Buzzard, the Imperial College London mathematician who has led a community effort to formalize the same theorem since 2024, reviewed and ran Claude’s code himself. His verdict was split: mathematically, nothing new was proven. But as a demonstration of what AI-assisted formalization can now do at scale and speed, he called it extraordinary.
Why This Matters Beyond Fermat
Mathematics has a quietly growing verification problem: proofs, including AI-generated ones, are being produced faster than the community can check them by hand. Formal, computer-checked proofs sidestep that bottleneck entirely. If this approach scales beyond a single famous theorem, it could reshape how mathematicians validate new results, not by replacing human insight, but by giving it an incorruptible, automated safety net.
Fermat thought his proof was too big for a margin. Claude’s version needed 13 million lines instead, and unlike Fermat’s, every single one of them can be checked.
Source:
Castelvecchi, D. (2026, September 8). Anthropic AI “formalizes” proof of Fermat’s last theorem — a milestone for mathematics. Nature. https://doi.org/10.1038/d41586-026-02822-9
Anthropic. (2026, September 5). Formalizing Fermat’s Last Theorem. https://www.anthropic.com/research/formalizing-fermats-last-theorem
