Anthropic publishes a 29,511-module Lean 4 proof of Fermat's Last Theorem
- Anthropic published a machine-checked Lean 4 proof of Fermat's Last Theorem containing 1,450 definition modules, 29,511 theorem statements, and 29,511 proof modules.
- The repository's FinalCheck.lean derives Mathlib's FermatLastTheorem and reports only
propext,Classical.choice, andQuot.soundas axioms forfermat_last_theorem. - The proof builds on Lean 4.33.1 with Mathlib v4.33.0; it is a port of a proof first checked on Lean 4.30.0, with theorem, axioms, and argument structure unchanged.
- Lean's comparator accepts the proof against a Mathlib-only challenge file, and nanoda, an independent Lean kernel implementation, accepts the same environment.
- The project includes an offline static HTML presentation, re-run scripts for comparator and nanoda verification, and a proof-path document mapping argument steps to Lean theorems.
Hacker News opinions
I wonder whether any of this Lean code can be contributed to existing libraries. Formalizing the prerequisites is a lot of work, and it would be a shame if it all stayed trapped in one capstone proof.
In my experience, LLMs can close theorems well when they have an LSP to inspect the proof tree, but they have the same problem they have in large software projects: finding reusable lemmas and library structure. Kevin Buzzard has said he would accept a huge, ugly proof if it were a proof.
How do we establish that the Lean interpreter and the rest of the toolchain are error-free? At some point this seems like turtles all the way down.