Formalizing Fermat's Last Theorem
Archived — this story has rotated out of today’s deck. It is kept here in full.
The gist
Anthropic's Claude formalized Fermat's Last Theorem in Lean, producing 13 million lines of code in 11 days. This machine-checked proof confirms Wiles's 1994 result, marking a leap in AI-driven formal.
Background
Fermat's Last Theorem, proposed in 1637, states no whole numbers satisfy a^n + b^n = c^n for n>2. Andrew Wiles proved it in 1994 after seven years of work, but his 129-page proof was not machine-checkable. Formalization converts such proofs into a language computers can verify, eliminating human error. Since 2024, a community effort led by Kevin Buzzard at Imperial College has been working to formalize FLT in Lean, a project expected to take years. Anthropic's Claude accomplished this in 11 days using a multi-agent platform called Prove2Me, producing the largest Lean proof ever.
How it unfolded
- 1994Andrew Wiles proves Fermat's Last Theorem after seven years of work; the proof is later published in 1995.
- 2004 -2024Freek Wiedijk lists FLT as a formalization challenge; Kevin Buzzard's team begins a multi-year Lean formalization effort in 2024.
- Sep 4, 2026Anthropic publishes 'Formalizing Fermat's Last Theorem,' announcing Claude's complete machine-checked formalization in Lean, built on Mathlib and existing projects.
- Sep 5, 2026News outlets report the achievement; prediction markets spike to 99% for a formalized proof by 2029, and mathematicians like Buzzard praise the result.
Who’s saying what
- Official
- Anthropic states Claude produced an end-to-end, machine-checked formalization of Fermat's Last Theorem in Lean, built openly on existing work.
- Expert
- Kevin Buzzard calls it 'a major step toward the automatic formalization of modern mathematical literature,' noting the proof is multi-layered.
- Caution
- Some observers note the result is a formalization of Wiles's known proof, not new mathematics, and Anthropic's process claims are not independently verified.
Still unverified
Anthropic's claims of 11 days, ~6B tokens, and dozens of agents are not independently verified; the formalization's correctness is machine-checked but the process details are company-reported.