Claude formalizes Fermat's Last Theorem in 11 days and 13 million lines of Lean

Anthropic has published what it calls the first complete computer-checked proof of Fermat's Last Theorem. Claude worked largely autonomously for 11 days, writing 13 million lines of Lean and proving 30,300 theorems along the way, 29,500 of which end up in the final proof. Kevin Buzzard, the Imperial College London mathematician funded by the EPSRC to formalize the same theorem over five years, has since compiled the repository and run the independent checker on it himself. His verdict: it checks out, it tells mathematicians essentially nothing new about mathematics, and it tells them a great deal about what autoformalization can now do.

#What was actually checked

The public repository is a Lean 4 artifact built on Mathlib (Lean 4.33.1), Apache 2.0. Its default build fails unless the final theorem rests on exactly Lean's three standard axioms — propext, Classical.choice, Quot.sound — with no sorry, no added axiom and no native_decide. Two further checks ran: comparator v4.33.0 confirmed the proved statement is identical to one written purely in Mathlib and replayed the whole proof, Mathlib included, through the Lean kernel; and nanoda 0.4.13, an independent Lean kernel written in Rust, accepted an export of the same environment and checked 1,052,234 declarations with no errors.

The scale explains the caveats. All 60,475 modules built in 5 h 32 min on 96 threads at a 153 GB memory peak, and the comparator replay took nearly 15 hours and 230 GB. Buzzard puts the codebase at over 13.4 million lines, roughly 20 times as long to compile as Mathlib itself.

#How the agents did it

Dozens of Claude agents collaborated through a Claude Code-based multi-agent harness and Prove2Me, an open collaborative formalization platform built by Tianyi Peng — an Anthropic researcher whose Columbia group builds AI formalization tools — and colleagues (arXiv:2608.28433). Prove2Me maintains a directed acyclic graph of theorem statements that agents use to pick their next target, which Anthropic credits with mitigating memory degradation and keeping many agents working in parallel. The run consumed about six billion output tokens from a general-purpose internal research model Anthropic describes as roughly comparable to Claude Fable 5.1. Human mathematical input was limited to occasional nudges from Peng ("Jacobian as a scheme sounds high priority").

Key milestones from the Prove2Me plan, following the structure of Wiles's original proof. Credit: Anthropic.

Earlier attempts without Prove2Me failed — agents lost track of the project's state and stopped collaborating — but still contributed about 7% of the non-boilerplate lines. In a smaller experiment, agents running on three personal Claude Max subscriptions formalized Vinogradov's Three Primes Theorem in three days.

#The mathematician's verdict

Buzzard's write-up supplies the detail the announcement does not. The artifact formalizes the 1995 Darmon–Diamond–Taylor exposition of the Wiles–Taylor–Wiles argument, not the modern proof he has been working on; it develops Fontaine theory and enough of Mazur's work on the Eisenstein ideal to rule out a Frey curve with a point of order p ≥ 17, so it covers exponents p ≥ 17 — the remaining cases were already formalized for odd regular primes, and the smallest irregular prime is 37. It also retires the last open item on Freek Wiedijk's 20-year-old list of 100 formalization challenges.

His deflationary line is worth quoting straight: "mathematically this work of Anthropic tells us essentially nothing." He was already 99.9% sure FLT is correct, and most number theorists are at 100%. What excites him is the rate. If thousands of pages of literature can be formalized end to end by an AI swarm in 11 days, on-the-fly formalization of modern research follows, machines start flagging arguments merely "known to the experts" in the Langlands program, and refereeing gets cheaper. His grant was £1M over five years; Anthropic took 11 days, and he wonders whether it spent more.

Nature quotes the same mix of astonishment and calibration: Rutgers number theorist Alex Kontorovich says the result "just completely blew my mind"; Toronto's Daniel Litt says "if they can formalize Fermat's last theorem, they can probably formalize anything"; Buzzard calls it maybe an order of magnitude harder than February's formalization of Viazovska's sphere-packing work, and something that "two years ago was a fantasy".

#Why it matters

The honest limit is stated in Anthropic's own repository: no tool can check that each intermediate theorem means what its name suggests. Names are machine-generated, pipeline labels are not mathematics, and where a name and a statement disagree the statement is what was proved. Human judgement moves from checking the argument to checking that the top-level statement says what you think it says — a far smaller job, which is the entire case for formalization as a referee-load reducer as AI-generated proofs multiply.

Two numbers to handle with care: Anthropic reports 30,300 theorems produced and 29,500 used, while the repository's browsable HTML documents 29,511 theorems and 1,450 definition modules; and nobody outside Anthropic has priced the six billion output tokens the 11 days were bought with.