Claude AI Formally Verifies Fermat's Last Theorem in Lean

Fermat scribbled his famous claim in a book margin in 1637 and never showed his work. Andrew Wiles finally proved it in 1994, after seven years of effort largely in secret. Now, more than three decades later, Anthropic says its Claude AI went back through that entire proof and rebuilt it from the ground up in a form a computer can check line by line, with zero room for human error.

What Claude Actually Did

This wasn't Claude discovering new mathematics. Wiles' proof already stood. What Claude did, according to Anthropic, was formalize it — translate the informal, prose-and-symbols argument that human mathematicians read and trust into Lean, a proof assistant that behaves like an extremely strict programming language for logic. Every step in a Lean proof has to be spelled out so precisely that the software itself can confirm there are no hidden gaps, unstated assumptions, or subtle errors, something even expert peer reviewers can miss in a 100-plus-page human proof.

Anthropic says the run took 11 days and was largely autonomous, coordinated through a platform called Prove2Me built by Tianyi Peng and collaborators at Columbia University. Prove2Me breaks a target theorem into a web of smaller dependent statements and sets multiple Claude agents loose on proving each piece.

• 13 million lines of Lean code generated over the run
• 30,300 theorems proved, of which 29,500 were actually used in the final proof
• Roughly 6 billion output tokens consumed
• Verified using only Lean's three standard axioms — no shortcuts, no unproven assumptions

Why Checking Old Math Is News

It's fair to ask why re-proving something already accepted as true matters. The answer is trust. A traditional math proof is only as solid as the handful of experts who read it carefully enough to vouch for it — and history has examples of accepted proofs that later turned out to have quietly hidden holes. A Lean-verified proof removes that dependency on human review entirely; the logic is checked mechanically against foundational axioms, the small set of self-evident starting assumptions everything else is built from.

"This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics," said Kevin Buzzard, a mathematician at Imperial College London who reviewed the work. "If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature."

That last line is the real headline. If an AI can formalize a landmark 20th-century proof in under two weeks, the backlog of mathematics sitting in journals — theorems nobody has ever double-checked at this level of rigor — suddenly looks like a tractable problem instead of an impossible one.

Where India Fits In

Anthropic opened an India office earlier this year and has been building out its presence here, which makes this kind of research output more than a curiosity for Indian readers — it's a preview of the tools that will eventually show up closer to home. India has a deep bench of mathematics and computer science talent coming out of the IITs, ISI Kolkata, and TIFR, and formal verification isn't just an academic exercise here. The same discipline of mechanically proving a system does exactly what it claims applies directly to correctness-critical Indian infrastructure — UPI's payment rails, RBI-regulated banking software, and the smart contracts increasingly used in fintech, all domains where a single unverified edge case can cost real money. AI-assisted formalization tools maturing this fast could eventually let Indian engineering teams verify critical code with a fraction of the manual effort formal methods have traditionally required.

What This Doesn't Solve Yet

None of this means AI is inventing new mathematics on its own. Formalizing an existing proof, however impressive the scale, is a different task from discovering an original one — Claude had Wiles' roadmap to follow, even if filling in every logical step itself was the hard part. Anthropic's own framing is that this is a step toward machines that can check humanity's mathematical literature at scale, not a claim that human mathematicians are no longer needed.

The more interesting question is what happens once formalization stops being a rare, 11-day showcase and becomes routine. A world where every important proof gets machine-verified within days of publication changes how retractions happen, how fast errors get caught, and how much blind trust the field has to extend to any single paper. For a country producing as many math and CS graduates as India does every year, that's not a distant academic shift — it's a new kind of work about to exist.