The Imperial FLT project — the human formalization, still running

Kevin Buzzard's "ongoing multi-author open source project to formalise a proof of Fermat's Last Theorem in the Lean theorem prover." Repository read 2026-09-06 with its README and GENERAL.md.

This is not the project Anthropic finished, and the difference is the point of this page. Two days after a company announced a machine-checked proof of FLT, this repository was pushed to — at 14:13 UTC on the day this page was written. It has not stopped, and the reasons it has not are all written down in a document dated December 2023.

The repository

A date correction this ingest forces: kevin-buzzard said the project started "in 2024." The repository was created 2023-11-19, GENERAL.md is dated December 2023, and Buzzard writes that he would devote serious time "once the grant kicks in, which is October 2024." Three defensible dates for three different things; the page now says which is which. The Lean FRO timeline records the project as established December 2023.

A different proof, not the same one

The two FLT formalizations take different routes through the mathematics, and conflating them would be the easiest mistake available here.

| | Imperial project | Anthropic | |---|---|---| | Proof followed | not the original Wiles/Taylor–Wiles: a newer route via Khare–Wintenberger, Kisin and others | Wiles's 1995 proof, by way of the Darmon–Diamond–Taylor exposition | | Route designed by | Richard Taylor, after discussions with Buzzard | — | | Shared core | R = T: a deformation ring is isomorphic to a Hecke algebra (Mazur–Tilouine, proved in key cases by Wiles) | the same theorem, a different road to it | | Method | humans, blueprint-managed, PRs upstream to mathlib | agents against a prove2me DAG, 11 days |

Anthropic's post says its work adapts pieces of the community effort. That is compatible with the routes differing: shared lemmas, different architecture.

The stated goal is a reduction, not a theorem

The most-missed sentence in the project's own documentation: "The project will have achieved its initial goal if it successfully reduces Fermat's Last Theorem (initially proved in the 1990s) to a collection of several far more complex mathematical claims, all of which were known by the end of the 1980s."

So the 2029 target was never "a complete proof from the axioms." It is a reduction, built from both ends at once — "This project will start everywhere at once" — with foundational material PR'd into mathlib as it goes and the two halves eventually meeting. That design decision is why the project survives being scooped: the deliverable is the library, and the theorem is the forcing function.

Buzzard's four stated reasons make this explicit, and only one of them is about FLT:

1. Digitisation enables new uses. "Without the digitisation of music there would be no Spotify." The modern number theory the project formalizes goes into Mathlib, aimed at interactive error-free textbooks and papers that can be "interactively 'unfolded down to the axioms.'"
2. Training data for machine reasoning — a large body of Lean code usable "as high-level training data or in conjunction with a future large language model."
3. Many objects of modern number theory cannot even be stated in any theorem prover. Not proved — stated. Formalizing FLT forces the definitions into existence.
4. Freek Wiedijk's list of 100 challenge problems for formalization stood at 99 of 100, with FLT the only one left.

Reason 3 is the one this corpus had no page for, and it reframes what mathlib is: not a library of proofs but a library of definitions, without which whole areas of mathematics are unsayable to a machine.

The December 2023 prediction, and what happened to it

Written into GENERAL.md and still there today:

"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."

And in reason 2, on the same page: large language models "have got very good at mimicking humans, however their ability to reason (i.e., to think logically rather than just being stochastic parrots) is poor."

The answer arrived two years and eight months early. In August 2026 a model produced 13 million lines of Lean and a machine-checked FLT in 11 days. The invitation to compare is the project's own, which is why this page treats it as evidence rather than as a gotcha: a specific, dated, falsifiable forecast by an expert about the near-term usefulness of AI in his own field, made in public and resolved against him inside three years. Cluster F holds several such — tech-adoption-curve-twenty-years found most significant post-2000 technologies were never flagged early — and this is the sharpest one the corpus has, because the forecaster named the date the answer would be checked.

Buzzard has since read Anthropic's proof and called autoformalization artefacts "now robust enough to be built upon" (kevin-buzzard). He updated. The document has not been rewritten.

What the project still has that the 11 days did not produce

Stated plainly because the corpus should not overclaim in either direction:

• Mathlib contributions. Anthropic's 13 million lines are a proof; Buzzard's PRs are library. Anthropic's own caveat is that its proof is "likely much longer than it needs to be." Nothing in the corpus says how much of that output is reusable by anyone else, and that is the open question.
• A blueprint — a human-readable LaTeX map of the proof, built with Patrick Massot's blueprint software, still marked WIP. It is documentation of why, which a type-checked artifact is not.
• Trained people. Buzzard describes the work as "a good source of smaller Lean projects suitable for PhD students in number theory who are interested in learning the language."
• A route nobody has formalized yet. Khare–Wintenberger and Kisin remain unformalized whatever happened to Wiles's original argument.

What is not here

No progress percentage, no count of completed blueprint nodes, and no statement from the project about the Anthropic result — the repository has said nothing about it in the two days since. The blueprint badge reads WIP. Whether the grant's remaining three years get re-scoped is unrecorded, and this page should be revisited rather than guessed at.

Related

kevin-buzzard · flt-formalization-anthropic · lean-theorem-prover · mathlib · autoformalization · prove2me · lean-lang-org · formal-verification · tech-adoption-curve-twenty-years