Anthropic publishes machine-checked proof of Fermat's Last Theorem in Lean 4
Anthropic has released a complete, machine-checked proof of Fermat's Last Theorem in the Lean 4 theorem prover, built on Mathlib. The proof follows the classic Frey–Serre–Ribet–Wiles–Taylor–Wiles argument and is verified by Lean's kernel, the independent Rust-based kernel nanoda, and the comparator tool. The repository includes 60,475 modules, 29,511 theorems, and a browsable HTML version of the proof. It's a research artifact, not maintained, and not accepting contributions.
Together, these checks establish that the statement above follows from the three axioms, given trust in the Lean kernel (or nanoda) and the checking tools.
- black_knight
I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries.
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!
(Repost of a earlier comment, but I feel it fits better here)
- superposeur
Much of the value of proof is in the development of math definitions and intermediate theorems needed to get you there, Grothendiek-style. This ability seems still to be beyond AI (at least, I haven’t heard of any fundamentally new and useful definitions such as “scheme” or “modular form” emerging from the latest blizzard of AI proofs). BUT, I wonder if AI could develop this skill too through a process of efficiently refactoring a big Lean proof into Lean pieces, then interpreting the pieces back into new, human-grokable definitions with evocative names?
- mcapodici
What a time to be alive stuff.
https://github.com/anthropics/fermats-last-theorem/blob/main...
- chvid
I think an interesting problem, perhaps even more interesting problem, would be the shortest / most concise / easiest to understand (formally verifiably) proof.
- rawling
Front-page discussion: https://news.ycombinator.com/item?id=49568506