Claude wrote 13 million Lean lines to check Fermat's Last Theorem

Anthropic published what it calls the first complete computer-checked formalization of Fermat's Last Theorem. Claude agents worked for 11 days to translate an existing mathematical proof into Lean code. The project produced 13 million lines and proved 30,300 intermediate theorems, with 29,500 used in the final proof. Anthropic says the run consumed about six billion output tokens.

The agents did not discover a new proof of the theorem. They followed a simplified version of the work behind Andrew Wiles's proof. Dozens of agents used a collaboration system called Prove2Me. A human researcher gave occasional high-level directions. Anthropic says early attempts lost track of the project, and their failed work still accounts for about 7 percent of the non-boilerplate lines.

The code is public. Its default build checks that the final theorem depends on Lean's three standard axioms and contains no unfinished proof markers. The repository says Lean built 60,475 modules. It also says nanoda, a second Lean kernel written in Rust, accepted an export containing 1,052,234 declarations with no errors.

Anthropic produced the result and owns the public repository, so the speed, token count and autonomy figures remain company claims. The formalization checks an existing proof; it does not replace Wiles's mathematical discovery or provide a short human explanation. Public code makes outside review possible, but publication is not the same as completed independent review.

Formal proof systems can check each logical step, but people usually spend years putting a large proof into that form. Claude changed how much formal detail a project can produce quickly.

The output is more than five times the size of Mathlib, the main library it builds on. That makes the result useful and awkward at the same time. A machine can check the chain. Mathematicians still need to understand the structure, review dependencies and decide whether the formal statement matches the theorem they care about.

Independent teams can now clone the repository, rebuild it from scratch and inspect the proof path. The first test is whether Lean and formal-math contributors reproduce Anthropic's checks and accept the dependency chain.

The next test is cost and reuse. Watch whether the same system can formalize another major theorem with fewer lines, fewer tokens and less human steering. That would show whether this was a one-off feat of scale or a repeatable research tool.