Claude formalized Fermat's Last Theorem in 11 days: Anthropic

Claude worked largely autonomously for 11 days and produced a computer-checked proof of Fermat's Last Theorem, Anthropic wrote in a research post. The formalization runs to 13 million lines of Lean code and proves 29,500 intermediate theorems, over five times the size of Mathlib, the principal mathematical proof library.

"We are sharing the first complete computer-checked proof of Fermat's Last Theorem," the post opens. The work followed a simplified version of Andrew Wiles's 1995 proof, in the version by Darmon, Diamond and Taylor, and consumed roughly six billion output tokens from an internal research model.

Kevin Buzzard, the Imperial College London mathematician who has led a community effort to formalize the same theorem in Lean, reviewed the artifact. "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," he said. He went further on what the technique enables: "If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature. Such autoformalization techniques will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees."

The run turned on Prove2Me, an open collaborative platform built by Anthropic researcher Tianyi Peng and collaborators at his Columbia University group. Prove2Me maintains a directed acyclic graph of theorem statements that dozens of Claude agents used in parallel to decide which sub-proofs to attempt next. A separate three-day experiment used three consumer Claude Max plans to formalize Vinogradov's Three Primes Theorem through the same platform.

Five of the researchers on our radar shared the write-up, three of them the day it went up.