Resolution Grants $1M to Mathlib’s Formal Commons

Resolution is granting $1M to The Formal Commons Project.

The Formal Commons Project is a two-year project within the Mathlib Initiative to develop protocols and tools that allow the Mathlib ecosystem to reckon with the ongoing AI revolution in mathematics writ large. Mathlib’s existing standards and practices work well for the world of human-generated proofs, but new processes will be needed to glean real value from AI-generated proofs without being drowned by them.

Mathlib is a community-driven, open-source library of formalized mathematics written in the Lean theorem-prover. The Mathlib Initiative launched in 2025 as a program of Renaissance Philanthropy. Led by Johan Commelin, Oliver Nash and Adam Topaz, it provides the editorial support, infrastructure and ecosystem coordination for Mathlib that a purely volunteer model could no longer sustain.

We recently announced our autoformalization of the resolution of singularities, and discussed how we see largescale autoformalization efforts using Mathlib enabling new approaches to mathematical research and new applications to AI safety. Our grant to The Formal Commons Project hopes to advance the frontier of this type of work.

Renaissance Philanthropy is a nonprofit organization with a mission to fuel a 21st-century renaissance by increasing the ambition of philanthropists, scientists and innovators. The organization designs time-bound, thesis-driven funds led by field experts and inspires talent to take action through playbooks and communities. In the first two years, Renaissance Philanthropy catalyzed $533M in philanthropic funding for science, technology, and innovation, launching 22 time-bound, thesis-driven, philanthropic funds and programs addressing global challenges.

Our autoformalization research at Resolution aims to scale the production of machine-verified proofs. We believe that The Formal Commons project will significantly empower our own autoformalization work.

Join us

If this kind of work excites you, we’d like to hear from you. We’re looking for people who know Lean and want to build the formal foundations for a science of learning, and for research engineers who want to work on research automation, from agent orchestration to making large Lean builds fast.