Kevin Buzzard
Number theorist at Imperial College London, and the mathematician who leads the community project to formalize Fermat's Last Theorem in Lean — flt-imperial-project, whose pieces Anthropic's proof adapts and whose blueprint for the first phase alone runs to 86 pages flt-formalization-anthropic.
Date corrected 2026-09-06 from the primary source. This page said the project started "in 2024."
The repository was created 2023-11-19, its GENERAL.md is dated December 2023, and Buzzard's own
sentence is that he would devote serious time "once the grant kicks in, which is October 2024."
Three dates for three different events; the 2024 one is when his funded time began, not when the
project started. Funding is EPSRC grant EP/Y022904/1, running to September 2029.
He reviewed that proof and supplied its outside assessment: autoformalization artefacts are "now robust enough to be built upon," and the technique points at "rooting out errors in the current mathematical corpus and lightening the load of referees." He also kept the hedge that the announcement does not — "which Anthropic researchers say only took 11 days."
Who holds the position is part of it: the person whose project this arguably pre-empted is the one endorsing the result.
He wrote down a forecast, and it resolved against him
The project's GENERAL.md, December 2023 and unedited since: "At the time
of writing (December 2023) the AI tools available to humanity are not really able to help with the
formalisation aspect of this task, so most of the work will be done by humans. It will be interesting
to see how different things will be in September 2029 as the grant ends." On the same page he called
LLM reasoning "poor" and the models "stochastic parrots."
The answer came in August 2026, two years and eight months before the date he set. He then read the result and updated in public — the quotes above are that update. Worth recording as an expert forecast about his own field that was specific, dated, falsifiable, and wrong on timing, from someone who acknowledged it rather than reframing it.
Related
flt-formalization-anthropic · autoformalization · lean-theorem-prover