Anthropic published a machine-checked formalisation of Fermat's Last Theorem in Lean 4 on 4 September; the GitHub API puts the repository's creation at 14:21:04 UTC. The claim that travelled was that Claude proved Fermat's Last Theorem in 11 days. The repository's own files describe something narrower and, in one respect, more interesting.
What the attribution file says
The repo ships an ATTRIBUTION.md recording 106 files that contain material from the Imperial College London FLT project led by Kevin Buzzard and from the flt-regular project — "54 under Definitions/, 52 under P2M/Sol/; and the 23 files that reproduce Mathlib text". Dozens of rows read "whole file (100%)". The NOTICE file dates the borrowing: "Material was taken from the project's main branch as of 2026-05-21". On the toolchain port to Lean 4.33, the attribution file records that it "left the other 41 byte-identical".
The verification is real
None of that undoes the checking. The README reports that all 60,475 modules built, that #print axioms fermat_last_theorem is guarded to the three standard axioms, and that no module contains axiom, sorry, native_decide, unsafe or partial def. Compilation took 5 hours 32 minutes at 96 jobs with a peak of 153 GB of memory. Anthropic's own figures: 13 million lines of Lean, 29,500 intermediate theorems used in the final proof, about six billion output tokens.
What the received framing gets wrong
Three things. Claude proved nothing new — this is autoformalisation of the 1995 Darmon–Diamond–Taylor exposition of the Wiles–Taylor–Wiles argument, a proof humans finished thirty-one years ago. It is not unassisted: by Anthropic's own accounting, a ninth of the repository carries human Lean text, some of it verbatim. And Buzzard, the mathematician whose review Anthropic cites, wrote on his own blog the same day that "mathematically this work of anthropic tells us essentially nothing" and that the formalisation "just faithfully follows the early literature on the proof and adds nothing." Several outlets also called it the largest file of its kind; it is 60,475 modules, not a file.
The honest claim is still large
Machines can now translate thousands of pages of existing mathematical literature into kernel-checkable form in under two weeks, seeded by several years of volunteer Lean work. That is a real result about translation speed. It is not a result about mathematical discovery, and the README concedes the residual gap itself: "What no tool can check is that each intermediate theorem means what its name suggests."