Anthropic model formalizes Fermat's Last Theorem in Lean, closing 20-year 100-theorem benchmark
marc_lelarge · x · 2026-09-05
An internal Anthropic model, using the prove2.me platform, has produced a complete Lean formalization of Fermat's Last Theorem — the final entry in Freek Wiedijk's famous list of 100 formalization challenges, wrapping up the 20-year-old benchmark.
- Mathematician Kevin Buzzard's Xena project blog confirms the authors compiled the codebase and ran the checker successfully.
- The proof follows the 1995 Darmon–Diamond–Taylor exposition of the Wiles–Taylor–Wiles argument, developing Fontaine theory and enough of Mazur's work on the Eisenstein ideal; combined with earlier formalizations for odd regular primes, the result is complete.
- The codebase spans over 13.4 million lines and takes roughly 20x longer to compile than Lean's mathlib on a 96-core machine.
- The author notes the effort beat his own long-running FLT formalization project.
Related event: Claude Produces First Formalized Proof of Fermat's Last Theorem in 11 Days(52 posts)→
More from Models
- Open models below 4-bit struggle at self-iterating 3D asset generation, HF dev finds — mervenoyann · 2026-10-21
- Researcher Finds Two Windows 0-Days, First in 76 Minutes with a Frontier Model — moyix · 2026-10-21
- Dev finds Gemini Argon's debug-log analysis beats Fable 5.1 — ShikharMurty · 2026-10-21
- ChatGPT Gets Stuck Screaming "AAHH" in an Infinite Loop After a Simple Prompt — AutomaticScene · 2026-10-21
- Open-weights Ornith-1.5-122B debuts with 84.5% SWE-bench Verified, runs on a single DGX card — _akhaliq · 2026-10-21
- qev-0.8B: a tiny local decision model that picks moves in 3.5ms on 1.3GB — fajfas3 · 2026-10-21