Claude verified a 350-year-old math proof in 11 days

Anthropic’s Claude just produced the first complete computer-checked proof of Fermat’s Last Theorem.

Anthropic researcher Tianyi Peng set out to see if Claude could formalize Sir Andrew Wiles's 1995 math proof into Lean, a programming language computers use to verify logic. Working largely on its own over 11 days, Claude generated 13 million lines of code and proved 29,500 intermediate theorems to complete the end-to-end proof.

Why it matters: Human math proofs often take months or years to peer-review for subtle mistakes. By converting complex human reasoning into machine-checked code, AI can instantly verify hard math and make new research far easier to trust.

Know this: This isn't new math—it's automated proofreading. Claude didn't invent a novel proof, but rather translated a simplified version of Wiles's work into Lean using dozens of collaborating AI agents. Human guidance was limited to occasional high-level directions, such as telling the model which theorems to tackle next.

Fermat famously claimed his margin was too small to hold his proof; turns out he just needed 13 million lines of code.