Lean Accepts Claude’s 10.5-Million-Line Fermat Proof

Lean, the proof-checking software used by mathematicians worldwide, has accepted a complete formal version of Fermat's Last Theorem. The formalization, produced by Anthropic's Claude system and published as an open repository, contains no unresolved placeholder steps, no extra axioms and no computational shortcuts beyond Lean's standard foundations (repository). Kevin Buzzard, the Imperial College London mathematician who had been leading his own formalization effort, independently compiled the project and confirmed it checks out, calling it "an extraordinary autoformalization achievement" (Buzzard).

The mathematics itself was settled long ago. Andrew Wiles proved the theorem in 1995, and no serious mathematician doubted the result. What remained unfinished was rewriting that proof as instructions for a literal checker, supplying every definition and intermediate step the original author could leave implicit. Anthropic says dozens of AI agents completed this translation in eleven days during August, working in parallel through a platform called Prove2Me (Anthropic).

That timeline, though, describes a process outsiders cannot reproduce. The internal model, orchestration infrastructure, operator decisions and compute expenditure are not part of the public release. What is reproducible is the finished artifact: anyone with sufficient hardware can recompile the Lean project and confirm the proof checks. A separate checker written in Rust by Anthropic verified the same formal artifact, confirming all 1,052,234 declarations are consistent (technical report). This is a second reading of the same text, not an independent reconstruction of the eleven-day campaign.

How the agents worked

Formalizing a proof means rewriting a mathematician's argument so that a program with no mathematical intuition can confirm every logical step. The theorem itself is deceptively simple: for any whole-number exponent of three or above, no three positive whole numbers satisfy aⁿ + bⁿ = cⁿ. The proof, though, passes through deep layers of number theory across hundreds of pages.

Claude did not discover new mathematics. It formalized the established chain of results leading to Wiles's proof, following an exposition by mathematicians Henri Darmon, Fred Diamond and Richard Taylor (Anthropic, technical report). The creative insight belonged to Wiles and his predecessors. Claude's contribution was translating that insight into roughly 10.5 million lines of machine-checkable code (technical report).

The Prove2Me platform, designed by Anthropic researcher Tianyi Peng and Columbia University collaborators, split the proof into a dependency graph of some 29,511 self-contained claims (technical report). Agents selected ready claims, wrote Lean proofs for them and checked one another's proposed statements, working in parallel. The campaign consumed roughly six billion output tokens from an internal research model (technical report).

Human operators wrote no Lean code during the run, according to Anthropic, though they selected the theorem, supplied the known proof route, designed the agent infrastructure and occasionally adjusted priorities (Anthropic). The full operator transcript and compute costs were not disclosed.

Built on years of human groundwork

The result depended on Mathlib, the large community-maintained library of formalized mathematics, and drew directly on two prior projects. Buzzard's team at Imperial had been building a Lean formalization of FLT since late 2023, funded by a £1 million EPSRC grant planned through 2029 (EPSRC award). A separate community project had already formalized the theorem for a subset of cases. Anthropic's attribution file identifies 106 files containing material taken or adapted from these efforts (attribution).

Parallel execution makes the eleven-day calendar time incomparable with the human person-hours invested by Buzzard's team, which had run for about 22 funded months when Claude's campaign began (EPSRC award). Anthropic disclosed neither GPU-hours nor energy costs.

Before this release, FLT was the last remaining item on Freek Wiedijk's list of 100 important theorems awaiting formalization, a benchmark that has tracked progress for two decades (Buzzard).

The strongest test of whether this generalizes will be formalization of recent, less documented mathematics where no blueprint, mature libraries or prior formal work exists. This run tested a famous theorem with substantial infrastructure already in place. It demonstrates that AI agents, given a known proof route and prior formal work, can produce a complete formalization that Lean accepts and outsiders can recheck. The generation campaign itself remains unreproducible from the published material.