11 Days, 13 Million Lines: Claude Completes the First Computer-Verified Proof of Fermat's Last Theorem, but "Autonomy" Deserves Scrutiny
On September 4, 2026, Anthropic announced that its Claude model had produced a complete Lean formalization of Fermat's Last Theorem in 11 days—13 million lines of code and nearly 30,000 intermediate theorems—marking the first proof of FLT to be fully verified by a computer. However, the "largely autonomous" claim warrants closer scrutiny, given the reliance on a third-party platform, minimal human guidance, and years of prior formalization work by the mathematical community.