FLT: Anthropic has beaten me to it
Kevin Buzzard @XenaProject · blog · 2026-09-04 · ★★★★ · archived
The leader of the human Lean FLT project confirms Anthropic's 11-day AI formalisation of Fermat's Last Theorem is real, and says it tells us 'essentially nothing' mathematically.
Summary
Kevin Buzzard (Imperial College) wrote on his Xena Project blog on 4 Sep 2026, the day Anthropic announced it. He has led the EPSRC-funded human project to formalise FLT in Lean since 2024. He reports that Anthropic's internal model produced a complete Lean proof of FLT in about 11 days: 13.4M lines, compiling about 20x slower than mathlib. It follows the 1995 Darmon–Diamond–Taylor exposition and completes the last item on Freek Wiedijk's "100 theorems" list. Buzzard calls it a milestone for autoformalisation, not new mathematics. He argues that autoformalising hard material will eventually make refereeing much easier. His human project continues, with different goals: upstreaming to mathlib and readable documentation. Anthropic's post quotes him. Checked via WebFetch.
Archived text
"Note that mathematically this work of anthropic tells us essentially nothing"
People
Related events
All posts · id: 2026-09-04-xenaproject-flt-anthropic-beaten-me