Formalizing Fermat's Last Theorem
Points and comments are a snapshot, not live.
Claude autonomously produced a computer-checked proof of Fermat's Last Theorem in 11 days.
Anthropic announces that Claude wrote a 13-million-line Lean proof of Fermat's Last Theorem in 11 days, proving 29,500 intermediate theorems. The proof follows a simplified version of Wiles's proof from Darmon, Diamond, and Taylor. It used the Prove2Me open platform to coordinate agents and maintain a directed acyclic graph of theorem statements. The effort consumed roughly six billion output tokens from a model comparable to Claude Fable 5.1. The finished proof was checked by Lean using only its three standard axioms. Anthropic notes the proof is over 5x the size of Mathlib but likely much longer than necessary.
What commenters are saying
Commenters are impressed by the speed but note Kevin Buzzard's nuanced reaction: he says the work proves FLT but doesn't create the human-readable exposition or library contributions he was funded to produce. Some question the cost-estimates suggest $300k at API prices for 6 billion output tokens-and note that Anthropic has a trillion-dollar market cap. Several commenters find Lean's syntax hard to read, preferring Rocq or Naproche. One commenter flags that this completes the last box on Freek Wiedijk's list of 100 theorems for Lean.