A math problem that stumped humanity for 358 years just fell to an AI. Claude, Anthropic’s model, produced the first computer-checked proof of Fermat’s Last Theorem in 11 days, working mostly on its own. Here’s what actually happened, and why it matters even if you barely passed algebra.
Fermat’s Last Theorem: the problem that outlasted empires
In 1637, a French lawyer named Pierre de Fermat scribbled a note in the margin of a math book. He claimed that no three positive integers a, b, and c can ever satisfy aⁿ + bⁿ = cⁿ for any exponent n greater than 2. Simple to state. Apparently impossible to prove. He added that he had a marvelous proof, but the margin was too narrow to contain it.
Classic move. For 358 years, mathematicians tried to find that proof and failed. In 1908, a German prize of 100,000 gold marks, worth a million dollars or two today, was offered for a correct proof. More than 600 incorrect attempts flooded in during the first year alone.
Andrew Wiles finally proved Fermat’s Last Theorem in 1995. His proof ran 129 pages and used mathematical machinery invented centuries after Fermat died. And even then, it almost fell apart: reviewers found a critical gap a few months after his 1993 announcement, and Wiles spent a year, most of it alone, patching it.
So the bar was high. The hardest kind of high. A problem with a 350-year reputation.
What the AI actually did
On September 4, 2026, Anthropic announced the first complete computer-checked proof of Fermat’s Last Theorem. Claude didn’t discover new math. It did something arguably more impressive: it re-proved the theorem in a form a computer can verify line by line, with zero human assumptions beyond the standard axioms of mathematics.
The numbers are wild:
- 11 days of mostly autonomous work, where a human community effort was expected to take years.
- 13 million lines of Lean code, the programming language used for machine-checked proofs. That’s over five times the size of Mathlib, the biggest community proof library in existence.
- 29,500 intermediate theorems proved along the way, out of 30,300 total.
- About 6 billion output tokens, which is how AI companies count the model’s “thinking.” That’s a lot of computing, roughly comparable to what a large research run consumes.
Human input was minimal, and it shows in the instructions the researcher gave: things like “Jacobian as a scheme sounds high priority.” That’s not doing the math. That’s project management.
Read Anthropic’s full write-up here if you want the technical details.
How a team of agents pulled it off
The interesting part for normal people isn’t the proof. It’s how the proof got done.
Claude didn’t work as one giant model having one giant thought. It worked as a team of agents, dozens at once, each tackling a sub-theorem. They used a platform called Prove2Me, which keeps a map of every theorem proved and every theorem still open. Agents pick a target, prove it, add it to the map, and move on.
The first attempts failed. The agents lost track of the project’s state and stopped collaborating effectively. What saved it was structural: separate the statements from the proofs, keep a shared graph of what’s done, and let agents search and reuse each other’s results. Once that framework was in place, the team finished in under two weeks.
Here’s the part that should make you pause: about 7% of the final proof’s code came from the *failed* attempts. The mistakes weren’t waste. They were feedstock.
Real mathematician Kevin Buzzard, who knows this problem better than almost anyone, called it an “extraordinary autoformalization achievement” and said the proof is solid enough to build on.
Why a computer-checked proof matters
This isn’t just math trivia. Mathematicians have a verification problem.
Human proof review is brutally slow. The Kepler conjecture spent four years in review. Perelman’s Poincaré conjecture took the community four years and three 300-page papers to accept. Some results sit in limbo for a decade. And sometimes, wrong proofs get accepted and other people build theories on top of them before anyone notices.
A computer-checked proof changes the math: a machine verifies every single logical step. No “seems right to me.” No trust in the author’s reputation. If the logic chain has a hole, the checker rejects it, full stop.
That’s why this matters beyond math: it’s the same trust problem you have with AI agents in your own work. How do you know the agent did the job right? The answer, increasingly, is to have the work checked mechanically instead of eyeballed.
What this means for you
Let’s translate it out of math-land.
First, this is concrete evidence that AI agents can sustain long, complex projects on their own. Not a 20-minute task. An 11-day campaign with thousands of moving parts, coordination failures, bug fixes, and a final result that stands up to scrutiny. That’s the self-improving, autonomous direction AI has been heading since agents became practical.
Second, it changes the “AI can’t really think” conversation. You can argue about whether a language model understands math or just manipulates symbols. You cannot argue that the proof is wrong, because a computer checked it. The output is verifiably correct, whatever the model was “doing” internally. That distinction, process versus result, matters when people ask whether AI can be trusted with real work.
Third, the practical translation for non-mathematicians: if an AI can hold a 13-million-line proof together, it can hold together a lot of ordinary work, too. Drafting, research, code, analysis. The gap between “AI assists” and “AI executes” just got narrower. That’s a useful thing to know whether you’re wondering what AGI even means or just planning your next project.
The honest caveats
A few things to keep in perspective.
The proof follows Wiles’s approach. This is a verification milestone, not a new mathematical discovery. Nobody woke up with a surprise theorem; a machine checked an existing one, and the feat was doing the checking at scale, autonomously.
It also cost real compute. Six billion output tokens isn’t free. This is frontier-lab territory, not something you’ll replicate on a laptop this year.
And the model wasn’t exactly the Claude you chat with. Anthropic says it used an internal research model “roughly comparable” to Claude Fable 5.1, plus a custom multi-agent harness. The capabilities are real, but they’re not directly the ones in your subscription yet.
Takeaway
Fermat’s Last Theorem took 358 years for humanity to solve. A team of AI agents re-proved it, in machine-checkable form, in 11 days. The math story is fun, but the agent story is the headline: autonomous AI is getting good at long, coordinated, verifiable work.
If you’re building anything with AI agents, the playbook here is worth stealing: split the work, keep a shared map of what’s done, let agents reuse each other’s results, and don’t throw away failed attempts. That’s how you go from “AI helps me” to “AI handles it,” and this project just proved the ceiling is higher than most people assumed.
