Claude Produces First Computer-Checked Proof of Fermat's Last Theorem in 11 Days

Anthropic has shared what it describes as the first complete computer-checked proof of Fermat's Last Theorem (FLT), accomplished by Claude working largely autonomously over 11 days. The AI wrote 13 million lines of Lean proof-assistant code and proved 29,500 intermediate theorems to produce an end-to-end formalization that relies on no assumptions beyond the standard axioms of mathematics.

FLT — first conjectured by Pierre de Fermat around 1637 — states that no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n > 2. The first human proof, by Sir Andrew Wiles in 1995, ran to 129 pages and required months of verification. Efforts to formalize that proof for computer checking have been ongoing for over a decade, including a community initiative launched in 2024 by Kevin Buzzard at Imperial College London.

The project was initiated by Anthropic researcher Tianyi Peng, whose group at Columbia University builds tools for AI formalization, to test whether Claude could advance the formalization effort. The outcome exceeded expectations. Buzzard, commenting on the result, said: 'This extraordinary autoformalization achievement proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics… AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.'

Anthropic frames the work not as novel mathematics but as a verification milestone — analogous to checking a computation with a calculator. The company suggests that as AI produces more proofs, robust formalization tools could significantly reduce the years-long burden of peer verification in mathematics.