Fermat’s Last Theorem gets a machine-checked proof

Anthropic says Claude spent 11 days working largely autonomously to write a proof of Fermat’s Last Theorem that a computer can check line by line, a formalization the math community expected to take years.

Written in Lean, the proof runs to 13 million lines, over 5x the size of Mathlib, the community library it builds on. Lean verified it using just its three standard axioms.

Kevin Buzzard of Imperial College London reviewed it and called the work an “extraordinary autoformalization achievement” that proves the theorem “with no assumptions other than the axioms of mathematics.”

Dozens of Claude agents coordinated through Prove2Me, an open platform from Anthropic researcher Tianyi Peng and collaborators at Columbia. The full proof and a written walk-through are on GitHub.