Claude writes first complete computer-checked Lean proof of Fermat's Last Theorem

Anthropic claims a first in machine-verified mathematics

Anthropic has published what it describes as the first complete, computer-checked proof of Fermat's Last Theorem (FLT). According to the company, Claude worked largely autonomously for 11 days to write the proof in the Lean proof assistant, producing roughly 13 million lines of Lean code and the 29,500 intermediate theorems that make up the final argument — a formalization mathematicians had expected to take years.

Why the theorem was so hard to check

FLT states that no positive integers a, b, and c satisfy aⁿ + bⁿ = cⁿ for any n greater than 2. As Anthropic recounts, Fermat noted the claim around 1637 in the margin of his copy of Diophantus's Arithmetica, alongside a famous remark that the margin was too narrow to contain his proof. A prize announced in 1908 drew 621 incorrect attempts in its first year alone.

More than 350 years passed before Sir Andrew Wiles published the first accepted proof in May 1995. It ran 129 pages, relied on modern techniques far beyond anything available to Fermat, and survived a difficult review: a gap surfaced two months into the verification of Wiles's 1993 lectures, and it took Wiles and his former student Richard Taylor about a year to close it. The Dutch computer scientist Jan Bergstra later proposed converting the proof into a machine-checkable form, and in 2024 Kevin Buzzard of Imperial College London kicked off a multi-year community effort to formalize FLT in Lean.

How Claude produced the proof

According to Anthropic, Tianyi Peng — an Anthropic researcher whose group at Columbia University builds AI formalization tools — set out to test how far Claude could get, and the result exceeded his expectations. Dozens of Claude agents collaborated to define concepts, prove intermediate theorems, and combine them into harder statements, following a simplified version of Wiles's proof by Darmon, Diamond and Taylor. Human input was limited to occasional high-level steering from Peng, such as prioritizing certain sub-results.

The early attempts failed. Anthropic says the agents initially lost track of the project's state and stopped collaborating effectively. The breakthrough came with Prove2Me, an open collaborative platform built by Peng and his Columbia collaborators. It maintains a directed acyclic graph of theorem statements that agents used to decide what to attempt next, splits statements and proofs into separate files to speed up Lean compilation, and keeps natural-language descriptions of each theorem so agents can search and reuse prior work.

The final push used a Claude Code-based multi-agent harness and consumed about six billion output tokens from a general-purpose internal research model Anthropic describes as roughly comparable to Claude Fable 5.1. Failed early attempts contributed around 7% of the non-boilerplate lines in the finished proof, and Claude proved 30,300 theorems in total along the way, of which 29,500 appear in the final version. Buzzard, who reviewed the result, called it an "extraordinary autoformalization achievement" that establishes FLT with no assumptions beyond the axioms of mathematics, adding that AI formalization artifacts are now robust enough to be built upon.

Verification, not new mathematics

Anthropic draws a contrast with its recent AI-driven work on the Riemann hypothesis, which produced novel mathematics. Here the theorem was already proved; the advance is the check itself. Proof assistants like Lean verify logic algorithmically, but the bottleneck has always been rewriting human proofs — which skip obvious steps and lean on centuries of published work — into the fully explicit form a machine requires. The blueprint the community was using for just the initial phase of the FLT formalization runs to 86 pages. Claude's finished proof is more than five times the size of Mathlib, the main community library of formalized mathematics it builds on. Anthropic's account gives the timeline as both 11 days of autonomous work and a little under two weeks for the overall effort.

Why it matters

If formalizing a proof of this scale becomes cheap, the economics of trusting mathematics change. Deep results can take months or years for humans to verify, while a Lean-checked proof is confirmed mechanically. As AI systems generate more mathematical claims, autoformalization offers a way to keep the burden of evaluation from becoming unmanageable. Anthropic frames the hope as making it easier, not harder, to trust the body of knowledge mathematics rests on. Two caveats are worth noting: the compute cost — six billion output tokens — suggests this is still far from routine, and the details so far come from Anthropic's own account of the work rather than an independent assessment.