Claude Formalizes Fermat’s Last Theorem in Lean, Anthropic Says

What Lean checked

Fermat's Last Theorem says that no positive integers a, b and c satisfy a^n + b^n = c^n when n is greater than two. Andrew Wiles and Richard Taylor established the accepted human proof in the 1990s. Anthropic's result translates that known argument into definitions and proof terms that Lean can check step by step, including details a paper written for mathematicians leaves implicit. [1]

The public repository declares the theorem over Lean's natural numbers and makes its default build fail unless the proof uses exactly Lean's three standard axioms, with no added axiom, unfinished proof marker or native-code shortcut. A comparator checks that this statement matches Mathlib's own statement of Fermat's Last Theorem. The repository also reports that nanoda, a separate Lean kernel written in Rust, accepted an export containing more than one million declarations. [4]

Those checks establish that the encoded conclusion follows from the stated axioms, assuming the checking kernels are sound. They do not make thirteen million lines readable, or prove that every intermediate theorem's name captures the mathematical idea a human associates with it. The repository says that semantic reading remains a job for people. [4]

The eleven-day campaign needed a map

Anthropic says dozens of agents running a general-purpose internal research model, roughly comparable to Claude Fable 5.1, completed the formalization in eleven days. The run consumed about six billion output tokens, wrote thirteen million lines of Lean and proved 30,300 intermediate theorems, of which 29,500 appear in the final proof. Tianyi Peng supplied occasional high-level priorities rather than filling in the individual proofs. [1]

Early attempts stalled because the agents lost track of the project's state and stopped coordinating. The successful run used Prove2Me, which represented outstanding theorem statements as a directed graph, separated statements from proofs to reduce compilation work, and attached natural-language descriptions so agents could find and reuse results. A multi-agent harness built on Claude Code executed the work. Anthropic reports that failed attempts still contributed about seven percent of the final non-boilerplate code. [1]

The result therefore measures a model-plus-scaffold system, not an unaided chatbot presented with Wiles's paper. The campaign's early attempts failed on project memory and division of labor; giving the agents a shared dependency map turned a mass of local proof attempts into an end-to-end artifact. [1][3]

An independent mathematician compiled it

Kevin Buzzard, who leads a separate effort to formalize Fermat's Last Theorem at Imperial College London, compiled Anthropic's repository and ran the comparator himself. He reported that it checked, measured more than 13.4 million lines, and took nearly twenty times as long to compile as Mathlib on a 96-core machine. In a follow-up comment, he said he manually inspected the small set of lines Claude classified as neither definitions nor proofs and found no malicious shortcut, while acknowledging that this was not a perfect audit. [5]

A result about verification, not Fermat

The proof follows the 1995 Darmon, Diamond and Taylor exposition of the Wiles and Taylor-Wiles argument rather than the modern route Buzzard's team is developing. Buzzard's assessment is blunt: the formalization adds essentially nothing to the mathematics of Fermat's theorem, whose proof number theorists already accepted. It shows that an agent system can turn thousands of pages of existing literature into a checked artifact at a speed the field had not planned around. [5][3]

The next bottleneck is curation. Buzzard's project also aims to put reusable number theory into Mathlib and produce a human-explorable account of a modern proof. Anthropic's repository is a standalone research artifact that does not accept contributions, and Mathlib still expects painstaking human review. Generating checked code at this scale can make formal verification practical while leaving the work of deciding what belongs in the shared mathematical library very much unfinished. [4][5]