Claude formalized Fermat's Last Theorem in 11 days

🤖 Claude formalized Fermat's Last Theorem in 11 days

Anthropic announced on September 4 the first complete machine-checked proof of Fermat's Last Theorem: the Claude model nearly autonomously led the formalization in Lean for 11 days. The result is 13 million lines of Lean 4 code and 29,500 intermediate theorems; verification includes building 60,475 modules, checking against Mathlib, and an independent Rust core.

🌍 The task of formalizing FLT, which Kevin Buzzard at Imperial College London had been working on since 2024, was considered purely human — an LLM agent pipeline completed it in 11 days. So far, this is a single demonstration without peer review.

👤 The code is open under Apache 2.0: 29,511 theorems can be read offline in HTML with a dependency graph, and a full rebuild takes about 5.5 hours on 96 threads. Correctness is checked by the Lean core, not by trust in the lab.

Source 1: https://www.anthropic.com/news/formalizing-fermats-last-theorem Source 2: https://github.com/anthropics/fermats-last-theorem