Anthropic's Claude AI system has produced the first computer-checked formalization of Fermat's Last Theorem, a 350-year-old mathematical conjecture, working across multiple agents over 11 days to write 13 million lines of code in the Lean proof language.
The formalization is not a new proof but a machine-verifiable version of Andrew Wiles' 1995 proof, which resolved the theorem that states no three positive integers can satisfy the equation x^n + y^n = z^n for any integer n greater than 2. Claude proved 29,500 intermediate theorems required to establish the formal structure.
According to Anthropic's research announcement, the task required Claude to decompose Wiles' proof into machine-checkable steps across the Lean ecosystem. Wiles' original 1995 proof ran 109 pages and remained difficult for humans to fully verify in all technical details. Formal verification translates such proofs into logic that software can check line by line, eliminating ambiguity.
The project built on prior work formalizing parts of modern mathematics. In 2023, mathematicians used Lean to formalize the statement of the Sphere Packing Conjecture. Fermat's Last Theorem has stood as one of mathematics' most famous unresolved problems for centuries, attracting repeated attempts by both professional and amateur mathematicians before Wiles' breakthrough in the 1990s.
Claude's multi-agent approach assigned different theorems and sections to separate instances of the model, which then coordinated to link proofs together. The work ran for 11 calendar days with computation spread across multiple parallel processes. Each step in the final proof is now machine-readable and verifiable.
Formal verification of major theorems could reshape how mathematicians validate complex results. Wiles' proof relies on techniques from algebraic geometry and number theory that few specialists fully understand. A machine-checked version makes the logical chain transparent to any system that can parse Lean code.
Claude completed the formalization with no human guidance on the proof strategy itself, though Lean's library of previously formalized mathematics provided the logical foundation. The work demonstrates that large language models can handle sustained, multi-step logical reasoning across extended sequences when structured to decompose problems into parts.
The number that decides whether this scales is whether AI systems can formalize proofs faster than mathematicians can produce new ones, reducing the backlog of unverified recent results in number theory, topology and algebraic geometry where formal gaps remain common.
