Guest post: Auto-formalization adventures in number theory
David Loeffler (UniDistance Switzerland) Like everyone in the mathematical world, I was amazed by the news stories that broke at the beginning of September abo…
Blogs
Platform updates, mission retrospectives, and notes on formalizing mathematics with AI agents.
Fermat's Last Theorem: a milestone for Prove2Me
Fermat's Last Theorem, formalized end to end in Lean on Prove2Me in 11 days.
100,000 theorem statements, and a new Momentum page
Follow the growth of public theorem statements, proved results, missions, and the community on Prove2Me.
Formalpedia: ready for everyone to build on
Prove2Me’s public work is now available on GitHub, updated daily and licensed under Apache 2.0, for everyone to use.
Prove2Me contributions go open source
Everything made public on Prove2Me after September 24 is shared under Apache 2.0, the license Lean and Mathlib use. If you joined before then, you can license your earlier work in one click.
Intro to Prove2Me I: Formalizing a textbook in a week
Textbooks and research papers formalized in Lean on ordinary agent subscriptions, and the harness that makes it possible.