Anthropic's AI formalizes Fermat's Last Theorem in Lean

Anthropic has published a complete, machine-checked proof of Fermat's Last Theorem written in Lean. The company says an internal research model generated it in 11 days. The finished result is about five times the size of Mathlib, the main open library of formalized mathematics.

Lean is a proof assistant. You write mathematics as code, and a small program called a kernel checks every step. Fermat's Last Theorem says no three positive whole numbers a, b and c satisfy a^n + b^n = c^n when n is above 2. Andrew Wiles proved it in 1995. Nobody had yet written that proof in a form a computer could verify end to end.

What is actually in the repository

Anthropic's research post went up on September 4, 2026. The code sits on GitHub under the Apache 2.0 license.

Its README states the formal theorem. For positive integers a, b and c, and any n of at least 3, a^n + b^n never equals c^n.

Item	Figure
Lean toolchain	4.33.1
Mathlib revision	v4.33.0
Theorems	29,511
Modules	60,475
Build time	5.5 hours at 96 parallel jobs
Peak memory	230 GB
Export size	37.8 GB

Two claims in the README matter more than the size. The proof contains no sorry, which is Lean's placeholder for a step nobody finished. And it rests on only three axioms: propext, Classical.choice and Quot.sound. Those three ship with Lean itself. Nothing extra was assumed to make the argument close.

Anthropic says the model proved 30,300 theorems in total, and that about 29,500 ended up in the final proof. It reports 6 billion output tokens and 13 million lines of generated Lean. The work ran through Prove2Me, a platform that splits a formalization into small statements and hands them to agents working in parallel.

How the proof was checked

Three separate checks were run, and this is the part worth understanding.

Lean's own kernel accepted the proof first. A tool called comparator, at version 4.33.0, then re-checked it in about 15 hours. Finally Nanoda, an independent kernel written in Rust, verified 1,052,234 declarations in roughly 30 minutes.

Nanoda matters because it shares no code with Lean. A bug in Lean's kernel would not be caught by Lean's kernel. A second implementation, in a different language, is a real check on that risk.

What mathematicians make of it

Kevin Buzzard leads the Xena Project. He holds a £1M grant from the UK research funder EPSRC, spread over five years, to formalize this exact theorem. He wrote on his blog that Anthropic got there first.

Buzzard is not disputing the result. "I am 99.9% sure that the proof of FLT is OK," he wrote. On Anthropic's page he calls the work an "extraordinary autoformalization achievement".

He also draws a boundary around it. The formalization "just faithfully follows the early literature on the proof and adds nothing," he wrote. It tracks the 1995 Darmon-Diamond-Taylor account of the Wiles argument. No new mathematics was found here. What is new is that the old mathematics is now machine-checkable.

Buzzard notes the proof covers primes of at least 17. Smaller irregular primes had already been formalized by others. A commenter on his post, David Jao, put the API cost of the run at roughly $300,000.

What this means for developers

If you write Lean, you can clone the repository, but check your hardware first. A 5.5-hour build at 96 jobs, with a 230 GB memory peak, rules out almost every laptop. Read the generated HTML documentation instead. It is 390 MB and needs no build.

The transferable lesson is not that a model wrote 13 million lines. It is that nobody had to read them. A kernel decided whether the code was correct, in minutes, without trusting whatever produced it.

That only works where a checker exists. Lean has one. Your web service does not. Before treating this as a template, ask what would play the kernel's role in your own stack. A type system, a property test, or a fuzzer are the usual candidates.

If you do review AI-written Lean, two mechanical checks carry most of the weight. Search for sorry, and print the axiom list. Anthropic's own claim rests on those two facts, and both are cheap to confirm yourself.

The cost gap is the last thing to note. Producing the proof took 11 days and billions of tokens. Re-verifying it in another language took half an hour. Anthropic has pointed research models at lab work before, and the same pattern holds here. Generating is expensive. Checking is cheap.