Anthropic says it has computer-checked Fermat's Last Theorem

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.