AI System Completes Machine-Checked Proof of Fermat's Last Theorem in 11 Days
Anthropic published on Sept. 4, 2026, what the company says is the first complete, computer-verified proof of Fermat's Last Theorem, written by its Claude AI system in 11 days. The full code is available on GitHub.
The proof is intended to show what AI systems can now do in mathematical formalization, converting human-readable proofs into machine-checkable form, rather than to add new mathematics. Kevin Buzzard of Imperial College London, who leads the community effort to formalize Fermat's Last Theorem by hand, compiled the repository and ran the verification tool on it. "It checks out," he wrote on his blog. He also noted that "mathematically this work of Anthropic tells us essentially nothing" — the proof follows the established 1990s argument by Darmon, Diamond and Taylor and adds no new results.
According to Anthropic, Claude produced 13 million lines of Lean code and proved 30,300 intermediate theorems, of which 29,500 appear in the final proof. Buzzard measured the repository at over 13.4 million lines and said it takes nearly 20 times as long as Lean's main mathematics library to compile on a 96-core machine. The proof uses Lean's three standard axioms, and a comparator confirmed the theorem statement matches the one already in Mathlib, the community library. Anthropic says the project consumed about six billion output tokens from an internal research model.
Fermat's Last Theorem was the final unformalized entry on Freek Wiedijk's list of 100 theorems that mathematicians set as a 20-year benchmark for automated proof systems. Buzzard said the achievement demonstrates what is now possible: "If thousands of pages of the literature can be formalized end-to-end by some kind of AI swarm in an 11 day period now, then in the future we will start to see formalization of modern research being done on the fly."
Anthropic also reports that three personal Claude Max subscriptions, collaborating through the same Prove2Me platform the project used, completed a separate formalization of Vinogradov's Three Primes Theorem in three days.
