Here’s the first-edition lead. Anthropic posted it on 4 September 2026: a complete, computer-checked formalisation of Fermat’s Last Theorem in the Lean proof assistant, written largely autonomously over 11 days. About 13 million lines of Lean. Roughly 29,500 intermediate theorems in the finished argument. The company calls it the first end-to-end machine-checked proof of FLT. Kevin Buzzard at Imperial College London — the mathematician who has led the human Lean FLT project since 2024 — downloaded the repository, compiled it, and said it checks out. New Scientist’s Matthew Sparkes carried the same story on 5 September. The hook is the check. The numbers are the story.

Hold the tally before you hold the romance. Eleven days of agent work. Thirteen million lines. Twenty-nine thousand five hundred intermediate theorems used in the final proof, with Anthropic also reporting about 30,300 theorems proved along the way. More than five times the line count of Mathlib, the community Lean library the artefact builds on. Lean’s three standard axioms only. A comparator confirming the proved statement matches Mathlib’s own statement of FLT. Buzzard’s public note, 4 September: he compiled the codebase, ran the comparator, and titled his post “FLT: Anthropic has beaten me to it.” That is the wire. Not a new theorem. A new kind of receipt.

Fermat’s claim is the one you already know in the short form. No positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any integer n greater than 2. Pierre de Fermat wrote it in a margin around 1637. Andrew Wiles proved it in the mid-1990s; the published argument with Richard Taylor is the human proof the formalisation is translating, not inventing. Anthropic’s research post is careful on that point. What’s new is the machine check: every step written so Lean’s kernel can verify the logic the way a calculator verifies arithmetic. Human proofs skip “obvious” steps. Lean will not.

Lean checked Fermat’s Last
The Standard illustration

The human formalisation project is not a rumour. Buzzard’s Imperial effort has been public since 2024, scoped as a multi-year job. The community blueprint for just the early phase runs to about 86 pages. New Scientist reported that Buzzard had said advances in automated help made him expect the work to finish faster than when he started — and that Anthropic’s announcement has now overtaken the race to a complete Lean FLT. His own blog is blunter still: the Anthropic artefact proves the whole theorem, not only the reduction he had promised funders for a first phase. He also says his EPSRC work is not finished. Mathlib pull requests and a human-readable dynamic document were always part of the bargain. Formalisation is not the same job as exposition.

Anthropic names Tianyi Peng as the researcher who set the test. The successful run used Prove2Me, an open collaborative platform Peng’s group has described for coordinating formalisation “missions,” plus a multi-agent harness. Dozens of agents defined concepts, proved intermediate results, and chained them upward against a shared directed acyclic graph of theorem statements. Early attempts without that shared state failed; Anthropic says those failed runs still contributed a small slice of non-boilerplate lines in the final tree. Human guidance, on the company’s telling, stayed high-level — priority nudges, not line edits. The finished proof was checked by Lean. Anthropic also reports an independent kernel check with nanoda on an exported environment.

What the proof actually follows matters if you’re going to trust the headline. Anthropic says the argument tracks Darmon–Diamond–Taylor’s exposition of the Wiles–Taylor modularity path: Frey curve, Mazur irreducibility in the cases needed, Langlands–Tunnell at 3, the 3–5 switch, a modularity-lifting step, Ribet level lowering, and the contradiction at level 2. Deep theorems appear in the special cases the argument requires. The opening reduction adapts material from the Imperial FLT project and from flt-regular, with credit. That lineage is why Buzzard’s compile matters. He is not a bystander. He is the person who has been building the human scaffolding this tree sits on.

Read the scale without confusing it for elegance. Thirteen million lines is partly length because machine-written formalisation is verbose and not yet in Mathlib style. Anthropic says as much. Mathlib is concise and reviewed; this artefact is huge, slow to compile — Buzzard reported roughly twenty times Mathlib’s compile time on a 96-core machine — and not a drop-in library patch. The scientific claim is narrower and stronger: a sorry-free proof, three standard axioms, statement matched to Mathlib’s FLT, kernel-checked. Wiedijk’s list of 100 formalisation challenges, Buzzard notes, now has FLT closed. That is a benchmark closing, not a rewriting of number theory’s history.

Why the verification burden matters here is simple. Wiles’s original verification took months and found a gap that needed a year to repair. Peer review of long modern proofs can take years. As more mathematics arrives with machine assistance, a Lean receipt is one way the community keeps the ground under its feet. Buzzard’s quote in Anthropic’s post goes to that: if automatic formalisation of FLT is possible now, the field has taken a step toward automatic formalisation of the modern literature — tools that can root out errors and lighten refereeing, and that can check purported machine-written mathematics that is otherwise expensive for humans to audit. Anthropic is careful not to claim this replaces a human-readable write-up. The company says a formalised proof should sit beside exposition, not erase it.

The dates line up cleanly. Anthropic research post: 4 September 2026. Buzzard’s “beaten me to it” post: same day. New Scientist: 5 September, Sparkes. Prove2Me paper on arXiv: late August 2026. The Lean repository is public on GitHub under Anthropic’s account, with a written walk-through. I’m not pretending I re-checked 13 million lines. I’m reporting who did, what they said, and which numbers are in the primary posts.

Token cost and model label are in Anthropic’s post if you need the industrial scale: on the order of six billion output tokens from an internal research model the company describes as roughly comparable to a Claude Fable 5.1-class system. That figure is how you know this was a research campaign, not a weekend demo. It is also how you keep the story honest. The achievement is formalisation throughput under a shared-state harness, reviewed by a hostile-friendly expert who wanted the human project to finish first. Buzzard congratulated them and kept his Mathlib work on the calendar. Both reactions can sit in one paragraph.

So on Sunday 6 September 2026: first complete computer-checked FLT in Lean, on Anthropic’s and Buzzard’s independent accounts. Eleven days. Thirteen million lines. About 29,500 intermediate theorems in the final chain. Lean axioms only. Mathlib statement match. Human project since 2024 reviewed and confirmed. The Anthropic research post and New Scientist carry the primary record. The theorem was proved in the 1990s. The check landed this week. That is enough news for one lead: a hard claim, a named checker, and a pile of countable lines you can point at.