Claude formalizes Fermat’s Last Theorem in Lean
Anthropic reported on September 4, 2026 that Claude produced the first complete computer-checked proof of Fermat’s Last Theorem, writing about 13 million lines of Lean and proving roughly 29,500 intermediate theorems over about 11 days of largely autonomous multi-agent work on the Prove2Me platform, using Lean’s three standard axioms and a statement matched to Mathlib’s FLT. Anthropic researcher Tianyi Peng directed high-level priorities; Kevin Buzzard reviewed the result and called the autoformalization extraordinary, saying such techniques could help check AI-generated math and lighten refereeing. Anthropic frames this as verification of Wiles’s theorem path (via Darmon–Diamond–Taylor), not novel mathematics like a new Riemann result, and not a Claude consumer product launch.
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.