Anthropic's Claude Formalizes Fermat's Last Theorem: The First Machine-Checked Proof in 11 Days
Posted on 6th Sep 2026 07:38:59 in Artificial Intelligence, Machine Learning
Tagged as: AI, Anthropic, Claude, Fermat, Lean, mathematics, formal verification
On September 4, 2026, Anthropic announced a result that combines one of the oldest stories in mathematics with one of the newest tools in artificial intelligence: the company's Claude model produced the first complete, computer-checked proof of Fermat's Last Theorem (FLT), written in the Lean programming language. Working largely autonomously for 11 days, a swarm of AI agents generated more than 13 million lines of Lean code, proved 30,300 intermediate theorems — 29,500 of them used in the final proof — and consumed roughly six billion output tokens in the process. The result was verified by Lean's kernel using only the three standard axioms of the system, and independently re-checked by nanoda, a separate Rust implementation of the Lean kernel.
The announcement matters not because AI "discovered" anything new — it did not — but because it demonstrates that AI can now automate formal verification, the painstaking process of converting human mathematics into a form that computers can check step by step. As Kevin Buzzard, the Imperial College London mathematician who reviewed the proof, put it: "This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics."
A 350-Year Hunt, and the Price of Certainty
Fermat's Last Theorem begins with a margin note. Around 1637, the French mathematician Pierre de Fermat scribbled in his copy of Diophantus's Arithmetica that no positive integers a, b, and c satisfy the equation a? + b? = c? for any power n greater than 2, adding the famous remark: "I have discovered a truly marvelous proof of this, which this margin is too narrow to contain." For more than 350 years, that proof proved elusive. In 1908, a prize of 100,000 German gold marks was offered to anyone who could produce a correct proof; 621 incorrect attempts arrived in the first year alone.
The theorem finally fell to Andrew Wiles, who announced a proof in a three-day lecture series at Cambridge's Newton Institute in June 1993. Two months into verification, a reviewer's question exposed a critical gap. Wiles spent a year trying to repair it, first alone and then with his former student Richard Taylor, before publishing the completed 129-page proof in May 1995.
Even then, certainty came slowly — a pattern that repeats across modern mathematics. Thomas Hales's 1998 proof of the Kepler conjecture spent four years in review before a 12-referee panel settled for "99 percent certain." Grigori Perelman's 2002 proof of the Poincaré conjecture took the community roughly four years and three 300-page expositions to accept. Harald Helfgott's 2013 proof of the weak Goldbach conjecture is still under review. Against that backdrop, Dutch computer scientist Jan Bergstra proposed in 2005 that Wiles's proof should be "formalized" — translated into a form computers can check automatically. In 2024, Kevin Buzzard launched a multi-year, publicly funded project at Imperial College London to do exactly that in the Lean proof assistant. The community's blueprint for the initial phase alone ran to 86 pages, and mathematicians expected the full formalization to take years. Claude finished it in 11 days.
How a Swarm of AI Agents Wrote 13 Million Lines of Lean
Lean is a proof assistant: a programming environment in which mathematical theorems are stated as code and verified by a small, trusted kernel. Unlike a proof written for human readers, which skips "obvious" steps and leans on centuries of published work, a Lean proof must make every step explicit. A single broken link in the chain invalidates everything built on it — and the kernel accepts or rejects each statement with no middle ground.
The Anthropic run was led by Tianyi Peng, an Anthropic researcher whose group at Columbia University builds tools for AI formalization. The system combined a Claude Code-based multi-agent harness with Prove2Me, an open collaborative platform designed by Peng and his collaborators. Prove2Me maintains a directed acyclic graph of theorem statements, separates theorem statements from their proofs so files compile faster, and attaches natural-language descriptions to each statement so agents can search for and reuse existing results. Dozens of Claude agents worked against this dependency graph in parallel, defining concepts, proving intermediate theorems, and assembling ever harder results.
The first attempts failed. Agents accumulated too much context, lost track of what had already been proved, and duplicated work; roughly 7 percent of the non-boilerplate lines in the final repository come from those abandoned efforts. The run succeeded only after Prove2Me was added mid-project, giving the agents a shared map of the proof's dependency graph. The final proof follows a simplified version of Wiles's argument from the 1995 exposition by Henri Darmon, Fred Diamond, and Richard Taylor, running through Frey curves, Ribet's level-lowering theorem, and the Taylor-Wiles patching method. Human input was limited to occasional high-level instructions from Peng. Even the review process was multi-agent: on Day 11, a false lemma that had passed one agent's review was caught by another before it corrupted the final result. The root statement of the theorem was marked proved on August 18, 2026 at 02:00:57 UTC.
The verification story is unusually strong. Lean's kernel accepted the proof using only its three standard axioms, with no added axioms, no "sorry" placeholders, and no shortcuts. A comparator confirmed that the statement proved matches Mathlib's own statement of Fermat's Last Theorem, and nanoda — an independently written Rust kernel — checked the artifact as well. The formalization covers primes p greater than or equal to 17; the smaller cases were already formalized in earlier work on odd regular primes, and the smallest irregular prime is 37, so the coverage is complete. At more than 13 million lines, the artifact is over five times the size of Mathlib, the community mathematics library it builds on. A clean build takes about five and a half hours on 96 processor cores and peaks at 153 gigabytes of memory. By one estimate, six billion output tokens at API prices would cost roughly $300,000. A companion experiment formalized Vinogradov's Three Primes Theorem in just three days using consumer Claude Max plans.
What the Proof Is — and What It Is Not
The achievement is best understood by what it does not do. Claude did not find a new proof of Fermat's Last Theorem; it transcribed an established version of Wiles's argument into machine-checkable form. Buzzard, who compiled the repository and ran the comparator himself, is direct on this point: the work "adds essentially no new mathematical content," and most number theorists were already certain the theorem is correct. The remaining gap is semantic: the Lean kernel proves that the encoded statements follow logically from one another, but it cannot verify that every lemma's name and natural-language description actually express the mathematics it claims to. Turning checked code into mathematics that humans genuinely understand remains a separate task — one Buzzard's own EPSRC-funded project is still pursuing, along with contributions to Mathlib itself.
What is genuinely new is the capability. Buzzard's verdict points to the significance: "If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature. Such autoformalization techniques will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees." Fermat's Last Theorem was the final entry on Freek Wiedijk's famous list of 100 formalization challenges, a 20-year-old benchmark that is now complete. Anthropic frames the result as a step toward a future where every AI-generated proof ships alongside a machine-checked formalization, giving human reviewers a reliable way to evaluate the flood of purported results that LLMs are already producing.
Why It Matters Beyond Mathematics
For the software and AI industries, the FLT run is a systems story as much as a mathematics story. The model mattered — Anthropic describes it as an internal research model roughly comparable to Claude Fable 5.1 — but the run only succeeded after the coordination layer was fixed. The Prove2Me dependency graph, the separation of statements from proofs, and the natural-language indexing of results turned a failing multi-agent effort into an 11-day success. The same pattern is visible across long-horizon AI engineering work: as tasks stretch beyond a single context window, the orchestration infrastructure becomes as consequential as the underlying model.
The result also sharpens the debate about trust in AI output. A Lean proof is one of the few AI artifacts that cannot be faked or inflated — the compiler either verifies the logic or rejects it. As AI systems produce more purported mathematics, code, and research, formal verification offers a scalable way to separate demonstrably correct work from plausible-sounding output. The cost remains substantial: 13 million lines of code is a heavy artifact to store, rebuild, and audit. But 11 days of agent time replacing a process that was expected to take a human team years is the kind of productivity jump that gets noticed far beyond number theory.
Sources
- Anthropic — Formalizing Fermat's Last Theorem
- AI Weekly — Anthropic's Claude Formalizes Fermat's Last Theorem in Lean
- Xena Project (Kevin Buzzard, Imperial College London) — FLT: Anthropic Has Beaten Me To It
- Superpower Daily — Anthropic's Claude Built a 13-Million-Line Fermat Proof, Leaving a Semantic Review Gap