AI For Math Fund Announces $18 Million In Grants to Accelerate Breakthrough Discoveries in Mathematics
FOR IMMEDIATE RELEASE
Contact: Richard Hillary richard.hillary@xtxmarkets.com; media@renphil.org
WASHINGTON, D.C. / LONDON, Sept. 17, 2025 – Renaissance Philanthropy and XTX Markets today announced $18 million in grants from the AI for Math Fund, one of the largest ever philanthropic commitments supporting the development of AI and machine learning-based tools to advance mathematics.
The Fund’s first 29 winning projects include mathematicians and researchers at universities and organizations working to develop systems that help advance mathematical discovery and research across several key tasks. These include datasets of cutting-edge formalized mathematics, software tools to advance the synergies between AI and mathematics, and some high-risk, high-return ideas for applying AI to fundamental mathematics and applications. The grant awards range up to $1 million.
Launched in December 2024 with a $9 million commitment from XTX Markets, the Fund received 280 submissions from teams of researchers and mathematicians around the world. The number of high-quality applications was such that XTX Markets doubled its funding to $18 million.
Simon Coyle, Head of Philanthropy, XTX Markets, said, “The proposals for the first round of the AI for Math Fund were very strong, and therefore XTX Markets was delighted to double our initial funding. We are excited for the projects to come onstream in the year ahead and support the work of mathematicians everywhere.”
Projects to be funded from the awards announced today include:
Sketchpad (University of Edinburgh). The team will build an innovative system that will enhance the usability of AI in formal mathematics by automatically converting proofs into structured data. By introducing a new type of graph-based representation, Sketchpad will allow for the decomposition of proofs into individual statements, enabling more precise auto-formalization.
Formalizing Modern Theorems (Imperial College London). This project will create a public dataset of hundreds of formalized statements of theorems from top journals, such as the Annals of Mathematics, and in doing so will address the lack of formalization at the frontier of mathematical research. This project will also significantly expand formalized mathematics libraries and provide clear targets for AI systems on a wide range of tasks, including auto-formalizing proofs, identifying errors, and assisting humans in proof formalization.
LeanTutor (UC Berkeley). In this project, the researchers will create a tool that can reliably auto-formalize undergraduate students' proofs. The tool will also evaluate proof correctness and offer tailored guidance to undergraduates. LeanTutor's design draws on insights from education research, machine learning, and formal methods to develop a system for students and artificial intelligence agents to meaningfully work on mathematics together.
A full list of winners and their projects can be found here.
Renaissance Philanthropy convened an expert panel to review the proposals and award the grants. It is now administering the fund and providing ongoing support to grantees.
“I believe the tools these grantees will develop as a result of this work will be truly transformative,” Renaissance Philanthropy CEO Tom Kalil said. “Progress in AI for math can lead to the discovery of new fundamental theorems, strengthen hardware and software security, and improve the reasoning capabilities of AI models.”
This commitment from XTX Markets comes soon after two major philanthropic grants in the “AI for Math” space from the firm’s founder and CEO, Alex Gerko.
Gerko donated $5 million to Lean FRO, the focused research organization that is supported by Convergent Research. The project will make Lean easier to use by increasing its 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. Gerko also donated $5 million to further develop Mathlib, an open-source, community-driven online library that formalizes foundational mathematical knowledge in Lean.
About the AI for Math Fund
The AI for Math Fund seeks to advance the pace and impact of math discovery by supporting projects that are important for the field, but no one academic or industry lab has the incentive to do them. The fund will support projects that (1) are less likely to happen in a business-as-usual scenario; and (2) have the potential to advance the field as a whole. These include: developing open-source, production-quality tools; increasing the size, diversity, and quality of datasets required for training AI models; and increasing the ease-of-use of tools so that they are adopted by mathematicians.
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.
About XTX Markets
XTX Markets is a leading algorithmic trading firm that uses state-of-the-art machine learning technology to produce price forecasts for over 50,000 financial instruments across equities, fixed income, currencies, commodities, and crypto. It uses those forecasts to trade on exchanges and alternative trading venues, and to offer differentiated liquidity directly to clients worldwide. The firm trades over $250bn a day across 35 countries and has over 250 employees based in London, Singapore, New York, Paris, Bristol, Mumbai and Yerevan.
XTX Markets has an unrivalled level of computational resources in the trading industry, with a growing research cluster currently containing over 25,000 GPUs with 650 petabytes of usable storage. Teams across the firm include world-class researchers with backgrounds in pure math, programming, physics, computer science and machine learning. The firm is also constructing a large-scale data centre in Finland to future-proof its significant computational capabilities.
Since 2020, XTX Markets has committed over £250 million to charities and non-profit partners, establishing the firm as a major philanthropic donor in the UK and globally. The firm’s philanthropy focuses on advancing mathematics education and research, having committed over £50 million in grants to UK charities and education institutions, with the aim of supporting more students to progress to degrees, PhDs, and highly-skilled careers in maths, especially those from low-income backgrounds.