Anthropic's Claude Formalizes Fermat's Last Theorem in Lean

Anthropic says Claude produced the first end-to-end, computer-checked proof of Fermat's Last Theorem in the Lean programming language over 11 days, working largely autonomously. According to Anthropic's research post, the run generated 13 million lines of Lean code, proved 30,300 theorems (29,500 of them used in the final proof) and consumed roughly six billion output tokens. Lean verified the result using only its three standard axioms.

"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," writes Kevin Buzzard, the Imperial College London mathematician who reviewed the proof. He goes further: "If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature."

The work was assembled on Prove2Me, which Anthropic describes as "an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University." Peng is an Anthropic researcher whose Columbia group builds tools for AI formalization. Prove2Me maintains a directed acyclic graph of theorem statements and coordinates multiple Claude agents against it. The finished artifact runs roughly five times the size of Mathlib, the community library the proof builds on. A companion run formalized Vinogradov's Three Primes Theorem in three days using consumer Claude Max plans.

The proof follows a simplified version of Andrew Wiles's 1995 argument, tracing an exposition by Henri Darmon, Fred Diamond and Richard Taylor. The claim comes from Anthropic itself and one named external reviewer; no third-party replication is described. It lands amid heavy Anthropic coverage this quarter, one of 335 Anthropic items we have tracked in the last 90 days, and moved through the mathematical corners of that beat faster than most releases.