13 Million Lines of Lean in 11 Days, to Prove Something We Knew

TL;DR

On September 4, 2026, Anthropic published the first end-to-end, computer-checked proof of Fermat's Last Theorem. Dozens of Claude agents wrote roughly 13 million lines of Lean over 11 days, proved 29,511 theorems along the way, and burned about six billion output tokens doing it. The artifact is public and Apache 2.0, it compiles, and it leans on nothing but Lean's three standard axioms. Then Kevin Buzzard, who runs the multi-year human project to formalize the same theorem, built it himself, confirmed it, and wrote that mathematically the whole thing "tells us essentially nothing." He is right. It is still the most interesting AI result of the week, for a completely different reason.

What is actually in the repository

Not a paper. A buildable Lean project, and the top-level statement is the real one:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
  (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

The repo ships 60,475 modules, 29,511 theorems and 1,450 definitions against Lean 4.33.1 and Mathlib v4.33.0. It contains no axiom, no sorry, no native_decide, no unsafe, no partial def, and no #eval. The only things it assumes are Lean's three standard axioms: propext, Classical.choice and Quot.sound.

That list of what is absent is the whole story. Lean's kernel works like a customs officer who opens every single crate: each inference gets stamped or the shipment is refused. A sorry is the paperwork equivalent of a sticky note reading "trust me, it's fine." There are none in here.

It was checked twice, and not only by the tool that wrote it. A comparator run validated the proof against the challenge statement, and nanoda 0.4.13, an independent Lean kernel written in Rust, chewed through 1,052,234 declarations without an error. Buzzard compiled it too. Three separate checkers is a higher standard than most published mathematics gets.

How a swarm proves a theorem

The interesting engineering is not the model, it is the scheduler. The run went through Prove2Me, a formalization platform from Tianyi Peng, an Anthropic researcher whose group at Columbia builds tooling for exactly this. Prove2Me holds a directed acyclic graph of theorem statements and lets agents pick which node to attack next.

If that sounds familiar it is because it is a build system. Every theorem is a target, its prerequisites are its dependencies, and an agent can grab any node whose dependencies are already green. Hundreds of workers never block on each other, and nobody needs to hold the 129-page argument in context at once. The rest of the design follows from that: statements and proofs live in separate files so Lean recompiles less, and every statement carries a natural-language description so an agent can search for a lemma instead of re-proving it.

One number from the run deserves to be stolen by anyone building agent pipelines: failed attempts contributed about 7% of the non-boilerplate lines in the final proof. Dead branches were not waste, they were inventory.

The mathematician it beat says it proves nothing

Buzzard leads the Imperial College London FLT project, funded by EPSRC grant EP/Y022904/1 through September 2029, with mathematical strategy set by Richard Taylor. He posted the same day under the headline "Anthropic has beaten me to it," and then declined to be impressed for the obvious reason:

Note that mathematically this work of anthropic tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK.

Anthropic says the same thing about itself, which is the honest move. Its post draws the line explicitly: unlike recent AI work on the Riemann hypothesis that produced new mathematics, "what's novel here is the verification." Nobody discovered anything. A thing everybody already believed is now checkable by a computer.

Buzzard's second paragraph is the one that matters:

What this work does tell us, however, is what is possible in the field of autoformalization. If thousands of pages of the literature can be formalized end-to-end by some kind of AI swarm in an 11 day period now, then in the future we will start to see formalization of modern research being done on the fly.

He also measured it. Over 13.4 million lines by his count, taking nearly 20 times as long to compile as Mathlib on a 96-core machine, and one dry line on the economics: "I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money." Six billion output tokens is not a rounding error on anyone's invoice.

The caveats, stated plainly

This is not the proof Buzzard is building. His project formalizes the modern argument following Khare, Taylor and others. Claude followed the 1995 Darmon, Diamond and Taylor exposition of the Wiles and Taylor-Wiles argument, which is an older and more direct route.

That route has a gap. As Buzzard notes, the DDT proof only works for primes 17 and above. The remaining cases were already covered by the flt-regular formalization of Fermat's Last Theorem for regular primes, and since the smallest irregular prime is 37, the two halves meet. The repo carries 106 files traceable to Imperial and flt-regular, so the human work is in there, load-bearing.

Two more things a reader should know. Anthropic concedes the proof "is likely much longer than it needs to be," and every identifier is machine-generated, which makes the largest Lean proof ever written also, by some distance, the least browsable one. It is published as a research artifact, unmaintained, with contributions closed.

Reproducing it is not a laptop exercise either.

Why this lands outside mathematics

Strip the theorem away and look at the shape of the run. A hard problem was decomposed into a dependency graph of subproblems, each one small enough for a single agent context. A verifier that cannot be argued with graded every submission. Failures were recycled. Nothing merged unless the checker said yes.

That shape is not specific to number theory. It is what you get any time you have a cheap, total, adversary-proof oracle: a type checker, a compiler, a proof assistant, a property-based test suite, a hardware equivalence checker. Where such an oracle exists, agent count scales and correctness does not degrade, because the oracle is the thing holding the line, not the model. Where it does not exist, none of this transfers, which is why the same technique does not make your product roadmap self-executing.

The accessibility proof point is the sleeper here. Anthropic reports that agents running on consumer Claude Max subscriptions, through Prove2Me, jointly formalized Vinogradov's Three Primes Theorem in three days. That is a serious analytic number theory result, done on a plan a hobbyist can buy. The 13-million-line stunt needed a lab. The three-day one did not.

Key Takeaways

• Anthropic published the first complete machine-checked proof of Fermat's Last Theorem on September 4, 2026: roughly 13 million lines of Lean, 29,511 theorems, 11 days, about six billion output tokens, Apache 2.0.
• It uses only Lean's three standard axioms and contains no sorry, no native_decide and no unsafe. An independent Rust kernel, nanoda, re-checked 1,052,234 declarations cleanly.
• Kevin Buzzard verified it and says it tells us nothing new mathematically, because nobody doubted the theorem. What it demonstrates is autoformalization at swarm scale.
• The proof follows the 1995 Darmon, Diamond and Taylor exposition, not the modern argument, and it covers primes 17 and up. The lower cases come from the earlier flt-regular work, and 106 files trace back to human projects.
• The transferable design is Prove2Me: a DAG of subproblems, parallel agents, a machine oracle that grades every submission, and failed attempts recycled into about 7% of the final code.
• Agents on consumer Claude Max subscriptions formalized Vinogradov's Three Primes Theorem in three days through the same platform. This scale of formalization is no longer lab-only.

Sources: Anthropic research post, anthropics/fermats-last-theorem on GitHub, Kevin Buzzard, Xena Project blog, Imperial College London FLT project, Prove2Me paper (arXiv 2608.28433), FLT for regular primes (arXiv 2410.01466), Crypto Briefing