Lean FRO and Mathlib receive $10M from XTX Markets Founder Alex Gerko to further advance the use of AI for mathematical research
FOR IMMEDIATE RELEASE
July 24, 2025
Contact: media@renphil.org; richard.hillary@xtxmarkets.com; pr@convergentresearch.org
Donation to bolster automated theorem proving
In a major boost to the future of mathematics research, Lean FRO and Mathlib today announced announced $10 million in new funding from Alex Gerko, Founder and CEO of XTX Markets, to strengthen the open-source infrastructure for formal theorem proving and advance the use of AI in driving fundamental advances in mathematical research.
Gerko is supporting two pioneering initiatives, both built around Lean, a programming language and “proof assistant” that helps researchers around the world write and verify mathematical proofs. Heralded by experts like Fields medalist Terence Tao, Lean is gaining momentum because it can generate machine-checkable proofs, eliminating the need for manual verification. This allows both humans and AI to build on each other’s contributions.
Gerko will donate $5 million to Lean FRO, the focused research organization supported by Convergent Research. This support will make Lean easier to use by adding more natural language capabilities. It will also help create a more powerful interface between formal and informal mathematics, allowing researchers and mathematicians to use it for bigger, more ambitious projects.
In addition, Gerko will donate $5 million to Mathlib, an open-source, community-driven online library that formalizes foundational mathematical knowledge in Lean. The funding will help expand the breadth and depth of mathematics formalized in Lean and add more functionality, including definitions useful for programming.
By improving formal proof systems like Lean and further developing Mathlib, researchers hope to simplify and accelerate the formalization of mathematics, offering key datasets and infrastructure for future AI tools that could aid in the discovery of new mathematical theorems and help solve real-world problems in science, engineering, and finance.
“Lean FRO is building the infrastructure mathematicians need to solve advanced math problems and theorems with confidence and rigor,” said Adam Marblestone, CEO and co-founder of Convergent Research. “This support allows us to move faster, dream bigger, and open math to a wider community.”
With the funding for Mathlib, a new Mathlib Initiative will be incubated at Renaissance Philanthropy, which also runs the AI for Math Fund. XTX Markets is the fund’s founding donor.
“We are excited to support Mathlib and the important work it is doing,” said Tom Kalil, CEO of Renaissance Philanthropy. “AI is opening new doors for mathematical discovery and collaboration in ways that were never before possible, such as automated theorem proving. Alex Gerko’s funding will help accelerate that shift by supporting the tools and models that can drive fundamental breakthroughs.”
To learn more about the Mathlib Initiative at Renaissance Philanthropy, email info@renphil.org.
To learn more about Lean FRO, visit https://lean-lang.org/fro.
About Convergent Research
Convergent Research brings together scientific founders and funders to design, launch and operate Focused Research Organizations (FROs) across a range of fields. Our FROs, like the Lean Focused Research Organization, build pivotal infrastructure that bridges gaps to breakthrough scientific research, proving out a new operating model for science that enables a high level of team science and systems engineering for public goods creation. Since our founding in 2021, we've secured almost $400 million in funding from 30-plus individuals and institutions.
About Renaissance Philanthropy
Renaissance Philanthropy is a nonprofit organization that fuels a 21st-century renaissance by increasing the ambition of philanthropists, scientists, and innovators. In the first year, Renaissance Philanthropy catalyzed more than $214M in philanthropic funding for science, technology, and innovation, launching 10+ initiatives across AI, education, climate, health, and scientific infrastructure. The organization designs time-bound, thesis-driven funds led by field experts and inspires talent to take action through playbooks and communities. From accelerating mathematical discovery to expanding talent mobility, Renaissance Philanthropy is building the connective tissue between exceptional ideas and resources to create breakthroughs that transform entire fields.