Claude formalizes Fermat's Last Theorem in Lean

Anthropic researchers used Claude to produce the first computer-checked proof of Fermat's Last Theorem in Lean, the proof assistant mathematicians use to verify arguments line by line. The work, led by Tianyi Peng, took 11 days and produced about 13 million lines of Lean code, proving 30,300 separate theorems, of which 29,500 feed into the final result. The model followed a streamlined version of Andrew Wiles's 1995 proof, and the run cost roughly 6 billion output tokens from an internal research model.

The interesting part is how it was coordinated. Claude worked largely on its own through a platform called Prove2Me, which keeps a graph of theorem statements so many agents can split the work, compile in parallel, and reuse earlier results by searching plain-language descriptions of what each lemma proves. The finished proof is more than five times the size of Mathlib, the community's main formal math library.

Kevin Buzzard of Imperial College London, who leads a separate long-running effort to formalize the same theorem by hand, said this suggests automatic formalization of the modern mathematical literature is now within reach, which could catch errors in published proofs and lighten the load on human referees. You can read the writeup for the method in detail.

Why it matters

If you work in mathematics or formal verification, the bottleneck is shifting: a machine-checked proof of a deep result no longer takes years of human labor, so the open question becomes whether you trust the tooling and can audit what the model actually produced.