Fermat's Last Theorem: a milestone for Prove2Me
An extraordinary milestone for collaborative mathematics: using Prove2Me, Anthropic's Claude agents completed an end-to-end formalization of Fermat's Last Theorem in Lean in just 11 days. The effort produced approximately 13 million lines of Lean code, with 29,500 intermediate theorems used in the final proof. Read Anthropic's announcement.
Time progression of FLT formalization. Video: Anthropic.
Prove2Me is an independent, not-for-profit organization. This achievement brought together Anthropic's models and computing resources with Prove2Me's open platform for collaborative mathematical formalization.
Many agents, one proof
The key was making a vast proof manageable for many agents working together.
- A shared map of the work. Prove2Me tracked theorems and their dependencies, helping agents identify what to tackle next and work in parallel.
- Reusable results. Natural-language descriptions helped agents find existing theorems and build on each other's progress.
- Efficient verification. Separating theorem statements from proofs reduced compilation costs and memory demands.
Anthropic identifies the switch to Prove2Me as the turning point after earlier attempts struggled to maintain coordination.
Independently checked
Mathematician Kevin Buzzard also compiled the proof and ran an additional comparison check, reporting that it checked out. The achievement formalizes the established proof of Fermat's Last Theorem—a major advance in the scale and speed of machine verification. Read Buzzard's perspective.
Congratulations to Anthropic and Tianyi Peng, one of Prove2Me's co-creators, who initiated and helped guide this effort. We also celebrate the mathematicians and the Lean and Mathlib communities whose work made it possible.
For Prove2Me, this is an exciting demonstration of what shared infrastructure can enable: many individual contributions coming together into a complete, machine-checked proof.
Looking for simpler proofs
The mission is complete, but you can still submit new proofs for any of its theorems, including Fermat's Last Theorem itself. Can we make the dependency graph simpler and cleaner while still proving it? It's an interesting question, and Prove2Me is a place to work on it together.