Thirteen Million Lines of Lean: Claude Writes the First Machine-Checked Proof of Fermat's Last Theorem

Around 1637, Pierre de Fermat scribbled a claim in the margin of his copy of Diophantus’s Arithmetica: no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n > 2. He added, unhelpfully, that he had discovered a “truly marvelous proof” that the margin was too narrow to contain. It took humanity until 1995 — and Andrew Wiles’s 129-page tour de force — to settle the question. Today, Anthropic announced that its AI model Claude has done something no human or machine had done before: produced a complete, end-to-end, computer-checked formal proof of Fermat’s Last Theorem, written largely autonomously over 11 days in the Lean proof language.

What was announced

In a research post titled “Formalizing Fermat’s Last Theorem,” Anthropic describes what it calls the first complete machine-checked proof of the theorem. Claude wrote roughly 13 million lines of Lean and proved 29,500 intermediate theorems on the way to the final result, consuming about six billion output tokens from a general-purpose internal research model Anthropic says is roughly comparable to Claude Fable 5.1.

The distinction here matters and is easy to miss. Claude did not discover a new proof of Fermat’s Last Theorem — the mathematical content follows Wiles’s proof, adapted from the streamlined exposition by Darmon, Diamond, and Taylor, and it reuses pieces of the ongoing Imperial College London FLT project. What Claude did is arguably harder in a different way: it translated an enormous body of abstract mathematics into a formal language rigorous enough that a computer can verify every single logical step. The Lean proof checker did exactly that, and the final artifact relies on just Lean’s three standard axioms. A separate comparator confirmed that the theorem statement matches Mathlib’s own statement of FLT, closing the loophole of proving a subtly different claim.

For scale: formalizing FLT was expected to be a multi-year effort. The blueprint the mathematical community had been using just to describe the initial phase of the project runs to 86 pages.

Inside the 11-day run

The project was driven by Tianyi Peng, an Anthropic researcher whose group at Columbia University builds tools for AI formalization, working with a multi-agent harness built on Claude Code. The pivotal ingredient was Prove2Me, an open collaborative platform for formalizing mathematics designed by Peng and his collaborators. Prove2Me maintains a directed acyclic graph (DAG) of theorem statements that agents consult to decide what to attempt next, separates theorem statements from proofs into different files to speed up Lean compilation, and keeps natural-language descriptions of each statement to simplify the proof path.

The first attempts failed instructively. Early agents had some success but quickly lost track of the project’s state and stopped collaborating effectively; their discarded work still accounts for roughly 7% of the non-boilerplate lines in the final proof. Human input was deliberately thin — Peng limited himself to occasional high-level nudges like “Jacobian as a scheme sounds high priority” and “push the Mazur theorem to be done soon.”

Anthropic’s excerpts of Claude’s own thinking during the campaign are strikingly human in texture. As the final pieces cascaded into place, the agent logged: ”🏁🏁🏁 The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign.”

Why formalization is the story

Checking a mathematical proof is not like checking a calculation. Proofs are long chains of inference, and one broken link can silently invalidate everything downstream. Wiles’s original 1995 paper took months of painstaking review; the 1908 Wolfskehl Prize (100,000 German gold marks, roughly 1–2 million dollars today) drew 621 claimed proofs in its first year alone, nearly all wrong. Formalization promises to compress that verification burden from months of expert labor to machine time — but until now, the cost of formalization itself was prohibitive, which is why Jan Bergstra’s proposal to formalize Wiles’s proof sat mostly dormant for a decade, and why Kevin Buzzard’s community effort, kicked off in 2024, was planned as a multi-year campaign.

Kevin Buzzard, the Imperial College mathematician who led that community effort, reviewed Claude’s proof and framed the result plainly: “If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature. Such autoformalization techniques will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees.”

The other half of his quote points at the AI-era stakes: formalization is how humans can gain confidence in AI-generated mathematics, which is currently verified by extremely costly human-led review. As models produce more purported proofs than ever, a machine-checkable certificate of correctness becomes the difference between an interesting claim and a settled one.

From frontier lab to consumer subscription

Perhaps the most provocative detail in the announcement is a small follow-up experiment. Anthropic researchers used three personal Claude Max subscriptions — consumer plans, not a frontier-lab compute cluster — to formalize applications of the Hardy–Littlewood circle method. Collaborating entirely through Prove2Me, the agents completed a formalization of Vinogradov’s Three Primes Theorem in three days. Anthropic’s conclusion: with the right scaffolding, collaborative formalization of major results may be achievable on ordinary consumer subscriptions. The company also says it has expanded free and discounted subscriptions and research credits for mathematicians working on pure math and formalization.

There are honest caveats. The run consumed six billion tokens — token-intensive even by frontier-research standards, even if the finished artifact is the largest Lean proof ever constructed. The model was an internal research model “roughly comparable” to a shipping product, not a generally available capability. And formalizing a 1995 proof, however monumental, is a different task from producing novel mathematics.

But the direction is unambiguous. A milestone that the formal-mathematics community budgeted in years fell in eleven days, and the same stack reproduced a classic analytic-number-theory result in three days on consumer plans. As Anthropic puts it, formalization is “a place where we feel unambiguously good about the role of AI” — a tool that catches errors in the human mathematical corpus while making machine-generated mathematics checkable at last. Fermat’s margin was too narrow for his proof. Claude’s proof would not have fit in his library.