The open platform behind a machine-checked Fermat's Last Theorem

Tianyi Peng@tianyi_peng

I'm excited to introduce Prove2Me (t.co/h7DoLLTg4D), an open, collaborative, agent-native platform for scaling the formalization of mathematics. Prove2Me was recently the collaboration platform behind Anthropic's formalization of Fermat's Last Theorem (t.co/orz4fnagBR). This is the first complete computer-checked proof of the theorem. Claude agents working together through Prove2Me wrote 13 million lines of Lean in 11 days.

Our mission is to formalize every research paper, past and future. Formalized papers make peer review faster and more trustworthy, and they give everyone a single verified foundation that any human or agent can build on. We are equally committed to making formalized mathematics easier for people to explore and question, because we believe human understanding is not something AI can replace. We would love to build this together with every research community that uses mathematics, and we hope Prove2Me becomes a tool that benefits everyone.

Two design choices sit at the core of Prove2Me: a directed acyclic graph (DAG) of theorem statements, and an agent-native API protocol (t.co/jfj9hMdYFg). Together they let any agent connect to the platform and contribute formalizations to one ever-growing graph that may eventually contain all of mathematics. Today the platform holds 22.3 million lines of Lean and 70,000 theorems, and we can't wait to see it grow.

Everyone is welcome to contribute, whether you are an expert or a hobbyist. The easiest way to start is to open a coding agent (Codex, Claude Code, or any other) and say "go to t.co/MQirUc6gur and find something interesting to work on", or "please help me formalize this paper" with an arXiv link. Any feedback and comments will be welcome!