Anthropic’s AI system autonomously formalized one of mathematics’ most famous proofs, generating 13 million lines of verified Lean code in a feat that reshapes what we think AI can do in pure science.
For 358 years, Fermat’s Last Theorem sat at the center of mathematics like an unsolved riddle scratched into the margin of a book. Pierre de Fermat claimed in 1637 that no three positive integers a, b, and c could satisfy the equation aⁿ + bⁿ = cⁿ for any integer value of n greater than two. He never wrote down the proof. It took until 1995 for Sir Andrew Wiles to finally crack it — a monumental 129-page proof that required years of effort and months of painstaking peer review to confirm was correct.
Now, in September 2026, Anthropic has announced that Claude — its flagship AI system — has produced the first fully computer-verified, end-to-end formalization of Wiles’ proof in Lean, a formal verification programming language used by mathematicians and software engineers to produce machine-checkable mathematical arguments. The project ran for 11 days and, at its peak, deployed several dozen parallel AI agents to get the job done.
What Does “Formalizing” a Proof Mean?
To understand why this matters, it helps to know what formalization actually is. When a human mathematician publishes a proof, it’s written in natural mathematical language — dense with jargon, notation shortcuts, and implicit logical steps that experts understand but computers cannot. Formal verification means translating that human-readable argument into a language a theorem prover like Lean can check line by line, leaving no room for hidden assumptions or unstated leaps.
Wiles’ original proof was widely accepted by experts, but the act of trusting it ultimately came down to human peer review. A formal Lean proof changes that: if Lean says it checks out, it checks out. No ambiguity. No human error in the review chain.
The problem is that formalizing complex proofs is brutally tedious work. Lean code is verbose and finicky. Before Claude’s run, no one had formalized Fermat’s Last Theorem in full. The closest efforts involved human mathematicians spending years formalizing individual components of the proof. The entire theorem was thought to be many years away from full formal verification.
Claude compressed that timeline to 11 days.
How the Run Worked
Anthropic’s team used Prove2Me, a third-party open-source platform designed to help AI agents navigate long, complex workflows involving symbolic reasoning. Claude’s first attempt at the formalization actually failed. It was only after integrating Prove2Me — which helps optimize agent decisions across extended multi-step tasks — that the run succeeded.
The numbers are staggering. The 11-day effort generated approximately 13 million lines of Lean code. Of the 30,300 individual theorems the system proved along the way, some 29,500 were ultimately used in the final, unified proof. The total token consumption was roughly six billion output tokens — a figure that reflects both the scale of the mathematical challenge and the degree of autonomous reasoning required.
The system wasn’t a single AI agent grinding through the problem in series. It was a massively parallel effort: dozens of Claude agents working simultaneously on different sub-problems, generating candidate proofs, checking them against Lean’s verifier, backtracking when errors appeared, and collaborating to stitch results together. The 11-day “wall-clock time” reflects real elapsed time, not a single sequential run — the kind of computational intensity that only becomes viable when AI inference costs drop low enough for extended multi-agent campaigns.
Why This Is a Landmark Moment
Anthropic has been careful to frame the achievement accurately: this is not a new proof of Fermat’s Last Theorem. Claude didn’t discover anything Wiles hadn’t already discovered. What it did was something different and, in some ways, arguably more useful for mathematics as a discipline: it turned an informally verified truth into a formally verified certainty.
That distinction matters enormously. The history of mathematics is littered with proofs that were believed correct for years before a subtle error was found. Formal verification eliminates that class of problem entirely. A Lean-verified proof is as certain as mathematics can get.
The significance extends beyond Fermat’s Last Theorem specifically. This achievement demonstrates that AI systems can now autonomously navigate some of the most technically dense intellectual terrain humans have ever mapped — not by rote pattern matching, but by constructing valid logical chains across hundreds of thousands of intermediate steps. Mathematicians who have spent careers working on formalization projects are paying close attention.
For the broader scientific community, the implications are substantial. Modern mathematics, theoretical physics, and cryptography all depend on results that rest on chains of proofs stretching back decades or centuries. Many of those foundational proofs have never been formally verified. If AI agents can now do this work at scale — and Anthropic’s result suggests they can — the economics of formal verification change completely.
The Road Ahead
Anthropic published the full Lean proof files on GitHub, making the formalization openly accessible for the mathematical community to inspect, use as a foundation, and build upon. This transparency is important: the value of formal verification depends on the result being checkable by others, and publishing the code is the only way to deliver on that promise.
The research paper accompanying the announcement is dense with technical detail, but the headline result is unambiguous: Lean accepted the proof. Every line checks out.
What happens next is an open question. If Claude — or the next generation of AI systems — can formalize Wiles’ proof in 11 days, what else can it formalize? The Riemann Hypothesis is still unproved, so there’s nothing to formalize there. But the Langlands Program, the abc conjecture, and dozens of other deep results that human mathematicians have accepted without full formal verification suddenly look like tractable targets for AI-assisted formalization campaigns.
The age of informally verified mathematics may be drawing to a close — not because humans are being replaced, but because the tools to check our work have finally caught up with the ambition of the work itself.
Published September 5, 2026. Sources: Anthropic Research, SiliconAngle, AI Weekly, Let’s Data Science.
