An internal Anthropic research model produced the first computer-checked proof of Fermat's Last Theorem in Lean

Sources: primary, repository, Buzzard's account, discussion, Buzzard thread
Summary: Anthropic published on 2026-09-04 a Lean formalization of Fermat's Last Theorem produced over 11 days by a general-purpose internal research model it describes as roughly comparable to Claude Fable 5.1, run as dozens of agents through a Claude Code-based multi-agent harness on the Prove2Me platform and consuming about six billion output tokens. The formalization runs to roughly 13 million lines with 30,300 theorems proved and 29,500 used. Lean checks the proof against its three standard axioms, and a comparator confirms the formal statement matches Mathlib's statement of the theorem. Kevin Buzzard writes on his own blog that the theorem is the final entry in Freek Wiedijk's list of 100 formalization challenges, closing a benchmark open for 20 years. Buzzard also notes that the repository's proof covers exponents above a threshold, with the smaller exponents supplied by the earlier flt-regular formalization rather than by this work.
Why it matters: Buzzard compiled the repository and ran the comparator himself, on a machine and documents Anthropic provided, which makes this one of the few AI-produced results a reader can check, and he states it adds no new mathematics.