A 358-Year-Old Mystery Meets a Machine That Checks Every Step
In 1637, Pierre de Fermat scribbled a now-legendary note in the margin of his copy of Arithmetica, claiming that no three positive integers a, b, and c can satisfy the equation a^n + b^n = c^n for any integer n greater than 2. He added that he had discovered a truly marvelous proof, which the margin was too narrow to contain. For more than three centuries, that claim haunted mathematics. Andrew Wiles finally proved it in the mid-1990s, and the proof itself became the stuff of legend: more than a hundred pages of dense, interlocking argument that took years for the community to fully absorb.
This week, Anthropic announced something different and, in its own way, just as significant: Claude did not discover a new proof, but it did become the first system to formalize Wiles's proof in Lean, a proof assistant that checks every logical step mechanically. The run finished in 11 days. The output is more than 13 million lines of Lean code, the largest formal proof ever written. If you have spent any time around mathematicians, you know how fast that is: experts expected this particular formalization project to take years.
What Claude Actually Did
Formalization is not the same thing as proving, and keeping the two apart matters. Wiles's 1995 argument, built on the work of many predecessors, established the theorem beyond doubt. What nobody had done was translate that argument into a form that a proof assistant such as Lean can verify automatically. That translation is brutally hard: every implicit assumption must be made explicit, every dependency tracked, and every "obvious" step expanded until a machine can follow it.
According to Anthropic's research post, Claude generated more than 13 million lines of Lean code, proved 30,300 individual theorems along the way (29,500 of which appear in the final proof), and consumed roughly six billion output tokens. Lean verified the finished proof using only its three standard axioms. To put the scale in context, the artifact is about five times the size of Mathlib, the community library of formalized mathematics that the proof builds on, while the human-readable version of Wiles's argument runs to only a few hundred pages.
Mathematicians who reviewed the result were quick to underline what did and did not happen. "This extraordinary autoformalization achievement proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics," wrote Kevin Buzzard of Imperial College London, who has spent years campaigning for formal verification in mainstream mathematics. He added that if automatic formalization of this result is possible now, the field has taken a big step toward formalizing the modern mathematical literature as a whole.
Why Formalization Is the Real Bottleneck
The reason this matters is that verification, not discovery, has quietly become the bottleneck in modern mathematics. Proofs have grown so large and so specialized that no single human can check them end to end. When a major result is announced today, the community often spends years probing it for gaps. Formal verification changes the economics of certainty: a proof assistant either accepts a step or rejects it, with no middle ground and no appeal to authority.
A Lean proof does not accept plausible-sounding arguments. The compiler either verifies the step or rejects it — which is why formalization is the least forgeable evaluation task in AI.
That property also makes results like this unusually trustworthy as an AI benchmark. A model cannot bluff its way through Lean the way it can through a multiple-choice test. Every one of those 13 million lines had to compile, or the run would have failed. For anyone skeptical about claims of machine reasoning, this is about as close to a falsifiable demonstration as the field currently offers.
The Orchestration Breakthrough: Prove2Me
Here is the detail that most non-specialists will miss: Anthropic's first attempt to formalize Fermat's Last Theorem failed. The same model succeeded only after the team introduced Prove2Me, an open collaborative platform designed by Tianyi Peng and collaborators at Columbia University. Prove2Me maintains a directed acyclic graph of theorem statements and coordinates many Claude agents working against it at once.
That division of labor is not a nice-to-have; it is the whole trick. You cannot prove a theorem until its prerequisites exist, so a single agent working linearly stalls the moment it hits a missing dependency. Early runs collapsed for exactly that reason: agents accumulated too much local context, lost track of what had already been proved, and duplicated work across the graph. Prove2Me fixed the structural problem rather than the model. Dozens of parallel agents each claimed a node, while the graph kept track of what depended on what, making an impossible single-agent task into a tractable parallel one.
- 11 days of wall-clock time, using dozens of parallel Claude agents
- 13 million+ lines of Lean code generated
- 30,300 theorems proved, 29,500 used in the final proof
- ~6 billion output tokens consumed across the run
- 1,052,234 declarations independently confirmed by a second proof kernel
The lesson extends far beyond mathematics. Time and again in 2026, the harness around a model turns out to be doing as much work as the model itself. Before teams upgrade to a more expensive model, they should ask whether task decomposition is the actual constraint — a question the Fermat run answers with a clean natural experiment.
Two Kernels Are Better Than One
Trusting a 13-million-line proof would be unreasonable if Lean's built-in checker were the only safeguard, so the team added a second line of defense. The completed proof was also run through nanoda, an independent proof kernel written in Rust by different developers, which confirmed that all 1,052,234 declarations are correct.
A proof kernel is a small, heavily scrutinized piece of software that checks logical steps; the entire credibility of formal verification rests on its correctness. Running the artifact through two kernels written in different languages guards against the nightmare scenario in which a bug in a single checker silently accepts an invalid step. Mathematicians have asked for exactly this discipline since formal verification was proposed as an answer to unverifiable proofs, and it is refreshing to see an AI lab honor it rather than chasing the headline.
What It Means for Mathematics, and for AI
Anthropic also reported a companion run: Claude formalized Vinogradov's Three Primes Theorem in three days on consumer Claude Max plans — a reminder that this capability is not locked inside a research cluster. As formalization pipelines become cheaper and more parallel, expect a wave of activity around the great unformalized theorems of the modern literature.
Be careful, though, about the hype loop. Claude did not dream up a new proof strategy, and nobody should claim the machine did the creative work that Wiles did. What happened is arguably more useful: a system that can check a proof of this size in under two weeks changes the economics of mathematical certainty, and that is a genuine contribution regardless of who deserves credit for the original insight.
The Bottom Line
The Fermat formalization is a milestone for three separate reasons: it is the largest Lean proof ever written, it is the cleanest public demonstration yet that orchestration matters as much as raw model capability, and it makes a serious case that AI can accelerate the slowest, most valuable part of mathematics — making sure the results are actually right. The margin may have been too narrow for Fermat's own proof, but no margin is too narrow for a machine that checks every single line.
