Claude Formalizes Fermat’s Last Theorem in 11 Days, Producing 13 Million Lines of Lean Code

Quick Facts

• Claude produced the first complete computer-checked proof of Fermat’s Last Theorem in 11 days, working largely autonomously using a multi-agent system.
• The formalization runs to 13 million lines of Lean code, proves 29,500 intermediate theorems, and consumed roughly six billion output tokens.
• An independent Lean kernel, nanoda, verified the proof by checking more than one million declarations without errors.

Anthropic has produced the first complete computer-checked proof of Fermat’s Last Theorem, with Claude completing the work in 11 days. Mathematicians had expected the formalization process to take several years.

The result, published September 4, 2026, is the largest formal proof ever written in the Lean programming language. The codebase spans 13 million lines, proves 30,300 theorems, and is more than five times the size of Mathlib, the primary Lean mathematics library.

Fermat’s Last Theorem states that no positive integers a, b, c satisfy the equation aⁿ + bⁿ = cⁿ for any integer n greater than 2. Pierre de Fermat first wrote the conjecture around 1637. Sir Andrew Wiles published the first proof in 1995 after years of work, producing a 129-page paper.

Formalizing a proof means converting mathematical reasoning into a language a computer can verify line by line. Lean accepts or rejects code with no middle ground, requiring every logical step, algebraic dependency, and imported theorem to be made explicit. Human mathematical writing routinely skips steps experts consider obvious. Lean does not.

Anthropic researcher Tianyi Peng, whose group at Columbia University builds tools for AI formalization, led the effort. The team gave Claude access to an open-source tool called Prove2Me, which maintains a directed acyclic graph of theorem statements and coordinates multiple agents against it. The first attempt failed. Adding Prove2Me mid-run made completion possible.

The 11-day figure is wall-clock time across several dozen parallel agents, not the output of a single continuous session. The model used was described as a general-purpose internal research model roughly comparable to Claude Fable 5.1. The proof follows a simplified version of Wiles’s 1995 argument, in the formulation by Darmon, Diamond, and Taylor.

Lean verified the result using only its three standard axioms. An independent kernel, nanoda, also accepted an exported version of the environment and checked more than one million declarations without finding errors.

Kevin Buzzard of Imperial College London, who had been leading a multi-year community effort to formalize Fermat’s Last Theorem, called the result significant. “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,” Buzzard said. He added: “If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature.”

Buzzard also noted that the proof is multi-layered, spanning algebra, harmonic analysis, geometry, and number theory, and that AI formalization outputs are now reliable enough to be built upon by others.

Anthropic said in a statement that the work represents “a major step in the long process of firming up the core of mathematical knowledge.” The company added that it expects producing a formalized proof alongside any paper intended for human readers will become standard practice.

For software and technology companies, the result signals that AI-assisted formal verification is moving from research curiosity to practical tool. The same architecture — multi-agent coordination, graph-based task management, and compiler-verified output — could apply to verifying software correctness, checking regulatory compliance logic, or auditing financial models where human review is slow and error-prone.

Formal verification also functions as a benchmark that cannot be gamed. The Lean compiler returns a binary result. That property makes the Fermat formalization one of the cleaner demonstrations of what current AI systems can accomplish at scale on hard, well-defined problems.

Read more: Anthropic uses Claude to formalize proof of Fermat’s Last Theorem