FLT: Anthropic has beaten me to it

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.

"Note that mathematically this work of anthropic tells us essentially nothing"