# Anthropic’s Fermat Proof Is 13 Million Lines. > Source: > Published: 2026-09-08 04:36:03+00:00 Anthropic published the first formalized proof of Fermat’s Last Theorem on 4 September, and the number everyone repeated was 13 million lines of Lean. Its own write-up says the proof is “likely much longer than it needs to be” — and gives no figure for how much longer, or where the length sits. So we cloned it. **The 13 million lines are real: 13,499,380 across 60,478 files.** But they are not bloated proofs. Measured per declaration with the same counter on both sides, the median machine-written proof step is **8 lines** against **4 lines** for human-written Mathlib. Two times, not fifty. The size does not come from verbose proofs. It comes from **562,341 declarations** — the number of steps Claude generated to close one theorem. That reframes the question about machine-generated proof length. The interesting cost is not how wordy each step is. It is how many steps a machine needs where a human would take one. The proof is enormous, and the enormity is structural rather than stylistic. Individual steps are close to human density. There are simply an extraordinary number of them, and they are almost entirely new statements rather than reuses of what Mathlib already had. 13,499,380 lines of Lean in 60,478 .lean files, cloned at commit aa2d8b3 on 7 September 2026. The working tree is 1.9 GB. It divides into three unequal parts: The one-to-one match between Theorems/ and P2M/Sol is the architecture: every theorem is stated in one place and proved in another, and 99.7% of the solution files carry a top-level declaration literally named theorem solution. Yes, and by less than the raw file sizes suggest. We scanned both corpora with the same counter — lines from a declaration to the next top-level construct — against Mathlib at the exact commit the proof pins, db584cd (Lean 4.33.1, Mathlib v4.33.0): That is **2.0x on the median and 2.8x on the mean.** For machine-generated code closing a proof that took human mathematicians decades, twice the verbosity per step is a narrow gap, not a pathological one. The tail is where the two diverge properly. Mathlib’s longest proof is 256 lines. The Fermat proof has steps of 3,123. Its 99th percentile, 166 lines, is longer than anything in Mathlib at all. From decomposition, not from padding. 562,341 declarations closed one theorem. Mathlib — the accumulated formalization of a very large part of undergraduate and graduate mathematics — shows 185,411 by the same count. One theorem, on that measure, took roughly three times the declarations of the whole library. Read that as a ceiling rather than a fact, for a reason we hit ourselves and explain below. But the shape survives the caveat: the machine’s route to the theorem is decomposed into far more, and far smaller, pieces than a human would write, and it is almost entirely new ground. Only 0.6% of the proof’s theorem names share even a final name component with anything in Mathlib. Because this is the cleanest example anyone has published of a working evidence layer for agent output. Dozens of agents worked for 11 days and produced 13.5 million lines that no human will ever read. The reason anyone believes the result is not that the process was trustworthy. It is that Lean’s kernel checked every declaration, #print axioms confirms the proof rests on exactly three standard axioms, an independent Rust kernel accepted an export of the same environment, and a comparator confirmed the proved statement matches Mathlib's own. That is an unusually complete audit trail, and it exists because formal mathematics had already built one. Everywhere else agents act, the record is far thinner. We counted the tool-call record in six open-source agent frameworks and the median captures 5 of the 12 fields an audit record needs, with none recording why a run stopped — which is the mechanism behind [the silent agent failures no dashboard catches](https://medium.com/p/b690d82b00bd). The same gap shows up on the input side: [the 38,900 tokens of tool definitions an agent is handed before it does anything](https://medium.com/p/bd6187ca140d) are invisible in every trace we looked at. The contrast is the point. Verification made 13 million unreadable lines trustworthy. Almost no other domain has the equivalent. **Does the proof actually verify?** Anthropic reports a from-scratch lake build on Lean 4.33.1 with Mathlib compiled from source, checked further by the comparator tool and by nanoda, an independent Lean kernel in Rust. We did not reproduce the build; we counted source. **Is there a** **sorry hiding in it?** One file contains sorry, and its own header explains why: verification/comparator/Challenge.lean states the theorem using only Mathlib as the comparator's challenge, and its proofs are deliberately left open. The proof proper is checked under #print axioms against the three standard axioms. **Is 13 million lines a lot for a formal proof?** Yes, by a wide margin, and the size is dominated by step count rather than step length. Mathlib in total carries about 1.15 million lines of proof body by our count. **Why is only 0.6% of it recognisable from Mathlib?** The proof follows the Frey–Serre–Ribet–Wiles–Taylor route through modular curves, Galois representations and Cerednik–Drinfeld theory. Most of that machinery had never been formalized, so the repository is largely new statements rather than reuses. **Can I check these numbers?** Yes. git clone --depth 1 the repository, then count .lean lines per directory. The commit is aa2d8b3. **One question, if you work with agent output.** This proof is trustworthy because a kernel checked all 13.5 million lines, and formal mathematics is nearly alone in having that. In your own work, what is the largest volume of machine-generated output you have shipped that had *no* independent verifier — and what stood in for one? [Anthropic’s Fermat Proof Is 13 Million Lines.](https://pub.towardsai.net/anthropics-fermat-proof-is-13-million-lines-7df36801f4a5) was originally published in [Towards AI](https://pub.towardsai.net) on Medium, where people are continuing the conversation by highlighting and responding to this story.