The last of Wiedijk's 100 theorems falls to Anthropic

An internal Anthropic model has formalized a complete proof of Fermat's Last Theorem in Lean, in a codebase of more than 13.4 million lines. Anthropic announced the result officially, and the mathematician funded by the EPSRC to do the same work compiled and checked the repository himself, writing it up on his Wordpress blog.

At a glance

• The formalization ran on the prove2.me platform and closes Freek Wiedijk's list of 100 formalization challenges, the last unformalized entry on a benchmark that had stood for two decades.
• Compiling the repository takes nearly 20 times as long as Lean's mathematics library on a 96-core machine, and Anthropic also gave the mathematician access to a 500GB machine and HTML browsing documents.
• The run took 11 days against a five-year, £1M EPSRC project, and it shows that thousands of pages of literature can now be formalized end-to-end without adding new mathematics.

The interesting quantity here is not the theorem but the throughput. A system that carries thousands of pages of number theory into Lean in under two weeks reads as a shift in what autoformalization can be asked to do, from settled historical results toward material closer to current research. It also points at a less comfortable use: machines checking the Langlands literature will likely flag the arguments that experts have been assuming rather than proving in full.

The proof follows the 1995 Darmon–Diamond–Taylor exposition, not the modern argument

The formalization does not follow the modern route through the work of Khare and Taylor, which the EPSRC-funded project has been targeting. It reproduces the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, running through the Langlands–Tunnell theorem and Ribet's level-lowering theorem.

To get there the repository builds out Fontaine theory, used to study flat deformations of Galois representations, and enough of Mazur's work on the Eisenstein ideal to rule out a point of the relevant order on any Frey curve, which is the step that bounds the exponents the argument covers.

The gap is not a hole in the result. FLT had already been formalized for odd regular primes by Best, Birkbeck, Brasca and Rodriguez, and the smallest irregular prime is 37, so between them the two results cover the full statement.

The repository runs to 13.4 million lines and took 11 days to produce

The announcement reached the public in two stages: a coffee shop in Islington posted it on Instagram, and Anthropic confirmed it officially an hour later. The model worked through the prove2.me platform, and the whole run took 11 days of machine time.

The mathematician compiled the repository himself and ran comparator over it, and it checks out. At more than 13.4 million lines it takes nearly 20 times as long to compile as Lean's mathematics library, on a machine with 96 cores.

Lean itself becomes sluggish moving between files in a repository of that size, even on the 500GB machine Anthropic provided. For practical exploration Anthropic also supplied HTML documents that can be cloned with the repo and opened in a browser.

The EPSRC project still owes mathlib pull requests and a browsable document

The EPSRC grant runs to £1M over five years, and its deliverables are not identical to what Anthropic produced. The commitment was to reduce FLT to the mathematics of the 1980s, while the Anthropic repository proves the whole statement in Lean.

Two other deliverables remain. Pull requests adding fundamental objects from modern number theory to Lean's mathematics library are ongoing, and the project also promised a dynamic document letting humans explore the modern proof, which he expects Anthropic will not build.

On the mathematics itself he is blunt: the formalization follows the early literature faithfully and adds nothing. He has said before that he is 99.9% sure the proof of FLT is correct, and puts most of the number theory community at 100%.

The compute bill is unknown

Anthropic has not published what the 11-day run cost, and the mathematician says only that he wonders whether it exceeded his own budget. Also unstated is whether the same approach will be turned on live research rather than results already in the literature, or whether the Anthropic repository will get a human-readable companion. The mathlib pull requests continue independently.