Formalizing Fermat's Last Theorem
Published "Formalizing Fermat's Last Theorem" — formalized Wiles's proof of Fermat's Last Theorem in Lean using an internal general-purpose research model described as roughly on par with Claude Fable 5.1. Reports that it took 11 days, about 6 billion output tokens and 13 million lines of Lean code, proving 30,300 theorems (29,500 of them used in the final proof), and states that Lean checked it using only the 3 standard axioms. Many Claude agents collaborated on Prove2Me, a collaborative formalization platform designed by Tianyi Peng's team at Columbia, and it states that Kevin Buzzard (Imperial), who had led the Lean community's FLT formalization, reviewed it and confirmed it as the first end-to-end machine-checked proof of FLT. It follows the simplified exposition by Darmon, Diamond and Taylor rather than Wiles's original paper
Why it matters
A claim that an agent swarm carried out, in a short time, a large formalization project that the human community had been pursuing over a span of years. Because the output is a checkable artifact (a Lean proof), it can, unlike a benchmark, be rechecked externally — making it, among claims of autonomous research, a case that is relatively easy to check
Source — Primary sources first; secondary reports are labelled “Press”
Officialanthropic.comhttps://www.anthropic.com/research/formalizing-fermats-last-theoremAdded in Week 36, 2026 · See that week