AI verified Fermat's Last Theorem — in 11 days

For 350 years, Fermat's Last Theorem taunted mathematicians. Andrew Wiles finally cracked it in 1995 after seven years of solitary work, producing a 129-page proof that took experts months to verify. Now Anthropic's Claude has done something arguably more impressive: it produced the first complete, computer-checked formalization of that proof — in 11 days.

Announced on September 4, 2026 (UTC-4), the result is the first end-to-end machine-verified proof of Fermat's Last Theorem (FLT). Claude wrote 13 million lines of Lean code, proved 30,300 intermediate theorems, and relied on nothing beyond Lean's three standard axioms. No unproven placeholders. No hand-waving. Every single logical step checked by a computer.

What "formalizing" actually means

A proof written for humans skips steps. A mathematician might write "it follows easily that" and move on. A proof assistant like Lean can't do that — it needs every deduction spelled out explicitly, down to the last axiom. If even one link in the chain is broken, the whole thing fails to compile.

That's why formalizing FLT was expected to take years. The community blueprint for just the initial phase runs 86 pages. Kevin Buzzard at Imperial College London received £1 million over five years to lead a formalization effort. He got partway there. Claude finished the whole thing in less than two weeks.

Andrew Wiles announcing his proof at Cambridge in 1993. It took him seven years; Claude formalized it in 11 days.

How Claude pulled it off

The project was initiated by Tianyi Peng, an Anthropic researcher and Columbia University professor (Tsinghua Yao Class alum, MIT PhD). Rather than a single agent writing continuously, dozens of Claude agents worked in parallel — defining concepts, proving intermediate lemmas, and chaining results toward the root theorem.

The breakthrough came when the team switched to Prove2Me, an open platform Peng's group at Columbia built for collaborative formalization. Prove2Me maintains a directed acyclic graph of theorem statements so agents know what to prove next, separates statements from proofs to speed up compilation, and indexes everything in natural language for search and reuse.

Human input was minimal. Peng's interventions were things like "Jacobian as a scheme sounds high priority" and "push the Mazur theorem to be done soon." The agents did the rest.

The proof itself follows a simplified version of Wiles's argument from Darmon, Diamond, and Taylor — via the Langlands–Tunnell theorem and Ribet's level-lowering. It covers FLT for prime exponents p ≥ 5; smaller cases were already formalized by others.

The proof's dependency graph: Mazur's irreducibility, Ribet's level lowering, and Wiles's modularity all converge on Fermat's Last Theorem.

The numbers

The root theorem compiled successfully on August 17, 2026 at 22:00:57 (UTC-4) — August 18 at 02:00:57 (UTC). Claude's own log entry reads: "🏁🏁🏁The FLT root reads PROVED on prove2me. Historic moment for this campaign."

Why this matters

This isn't a new mathematical discovery. Wiles proved FLT in 1995, and the number theory community is confident the proof is correct. What's new is that a machine can now verify it independently — and quickly.

Buzzard, who independently compiled and checked Anthropic's codebase, put it best: "If thousands of pages of the literature can be formalized end-to-end by some kind of AI swarm in an 11 day period now, then in the future we will start to see formalization of modern research being done on the fly."

The implications go beyond one theorem. Peer review in mathematics is slow and error-prone. Papers routinely cite results that are "known to the experts" but never formally written down. If AI can formalize complex proofs on demand, every published result could come with a machine-verified certificate of correctness. That changes what "trust" means in mathematics.

It also closes out Freek Wiedijk's famous list of 100 formalization challenges — FLT was the final holdout, a benchmark the community has chased for 20 years.

The model used was an internal Anthropic research model roughly equivalent in capability to Claude Fable 5.1. The full proof is on GitHub under Apache 2.0, so anyone can compile it and verify for themselves.

Fermat claimed his margin was too narrow for a proof. Three and a half centuries later, the proof fits in 13 million lines of Lean — and a computer checked every single one.