Andrew Wiles proved Fermat's Last Theorem in 1994. What happened over 11 days in early August, Anthropic announced on Friday, is a different and stranger thing: a swarm of Claude agents wrote a complete, machine-checked version of that proof — 13 million lines of code in the Lean theorem prover — working, in Anthropic's words, "largely autonomously."

The distinction matters, so it is worth being precise. Wiles's proof is a human argument that other humans have checked and accepted. A formalisation is something else: every logical step rewritten in a language a computer can verify, so that a machine, not a person's judgement, certifies that nothing was skipped or fudged. Mathematicians have been chipping away at formalising Fermat's Last Theorem in Lean for years — Kevin Buzzard of Imperial College London leads the best-known human effort, and a full formalisation has generally been treated as a multi-year project. Anthropic's claim is that Claude got there first, and did most of the work itself.

What was actually done

According to Anthropic, a team of Claude agents — running on the open-source Prove2Me platform with a Claude Code-based multi-agent harness, powered by an internal research model it describes as roughly comparable to Claude Fable 5.1 — ran for about eleven days in early August. Along the way they produced roughly 30,300 intermediate theorems (about 29,500 of them used in the final proof) and burned through some six billion output tokens.

Crucially, this was not built from nothing. A formalisation "starts from the tiny fraction of math that's been formalised already," Anthropic notes, and Claude's proof builds on Mathlib, Lean's community-maintained library of formalised mathematics. The achievement is the enormous, unglamorous mile of formal argument on top of that foundation — the part that has defeated schedules for years.

Why anyone should believe it

The reassuring thing about a formal proof is that it is not a matter of trust. Lean either accepts the argument or it does not, and Anthropic says the finished proof checks out using only Lean's three standard axioms — the bedrock assumptions of ordinary mathematics — with a comparator confirming that the theorem Claude proved is Mathlib's own statement of Fermat's Last Theorem, not some weaker look-alike.

More telling than Anthropic's own account is who vouched for it. Buzzard — the mathematician who has spent years trying to formalise exactly this, and one of the most exacting voices in the field — reviewed the result and, on his own blog, pronounced himself "99.9% sure that the proof of FLT is OK," adding that the number-theory community is "100% sure." His post is titled, with good grace, "FLT: Anthropic has beaten me to it." When the person most invested in doing something the hard way says the machine did it properly — in public, under his own name — that is worth more than any benchmark.

What it means, and what it doesn't

It is easy to over-read this, so a few guardrails. Claude did not discover a new theorem; it formalised a proof that has stood for three decades. It did not work from a blank page; it stood on Mathlib and on decades of human mathematics. And the account is, for now, Anthropic's own, describing an internal model on an internal platform.

But strip the hype and something real is left. Formalisation is among the most demanding, least forgiving work in mathematics — there is no bluffing a proof assistant — and it has been a bottleneck precisely because it is so laborious that few humans want to do it. An AI system that can grind through 13 million lines of it, largely unsupervised, and come out the other side with a proof the field's hardest marker will sign off on, is a new kind of collaborator. The interesting question is no longer whether these systems can do rigorous mathematics. It is what the mathematicians do with the time they get back.