AI for Math Fund
The AI for Math Fund is a new grant program supporting projects that apply AI and machine learning to mathematics, with a focus on automated theorem proving. XTX Markets is the founding donor of the AI for Math Fund.
Winning Projects
Here are the winning projects.
Challenge and Opportunity
Formal verification – so-called “automated theorem proving” – allows computers to rigorously verify the correctness of proofs, or more broadly to “prove” the correctness of any computer program. Unfortunately, few people besides formal verification researchers use these tools, because they’re highly cumbersome and labor-intensive. That’s changing with AI-based automation tools, which are increasingly making formal verification frameworks accessible to working mathematicians, enabling new forms of large-scale mathematical collaboration. Once automated, usable formal verification tools are a practical reality, we’ll have the ability to automatically generate and verify mathematically rigorous claims in general, enabling a vast expansion in mathematical knowledge, while making AIs and software more robustly trustworthy.
AI for math has seen a growing number of exciting results from industry labs and academic researchers alike. However, open-source projects that benefit the field as a whole are underfunded both by industry and by traditional academic grants. Although the National Science Foundation has a modest program at the intersection of AI and math ($6 million per year), increased support can advance both the pace and impact of math discovery.
Philanthropy can have a large counterfactual impact by supporting 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.
Strategy
An increasing number of researchers, including some of the world’s leading mathematicians, believe that the mathematics of the future will be discovered, and studied, with the help of AI tools. The AI for Math Fund is dedicated to creating AI technologies that are valuable for mathematicians and expanding their use in the global mathematical community.
Through an RFP and open call for applications, the AI for Math Fund will support projects across four tracks: Open Source Tools, Transformative Datasets, Breakthroughs, and Field Building.
Projects may be led by applicants from academic institutions, commercial organizations, or independent projects, so long as all work is open-source and shared publicly, and is separate from the business-as-usual activities of any for-profit company. Typical applicants will have strong track records of achievement in formal verification, AI, and related fields.
1. Production Grade Software Tools
The AI for Math Fund will support projects that develop open-source, production-quality software tools in the intersection of AI and mathematics, such as:
AI-based autoformalization tools for translating natural-language mathematics into the formalisms of proof assistants
AI-based auto-informalization tools for translating proof-assistant proofs into interpretable natural-language mathematics
AI-based models for suggesting tactics/steps or relevant concepts to the user of a proof assistant, or for generating entire proofs
Infrastructure to connect proof assistants with computer algebra systems, calculus, and PDEs
A large-scale, AI-enhanced distributed collaboration platform for mathematicians
2. Datasets
The AI for Math Fund will support projects to produce open-source datasets for training AI models, such as:
Datasets of formalized theorems and proofs in a proof assistant
Datasets that would advance AI for theorem proving as applied to program verification and secure code generation
Datasets of (natural-language) mathematical problems, theorems, proofs, exposition, etc.
Benchmarks and training environments associated with datasets and model tasks (autoformalization, premise selection, tactic or proof generation, etc.)
3. Field Building
The AI for Math Fund will support projects that grow the field of AI for math, such as:
Textbooks
Courses
Documentation and support for proof assistants, and interfaces/APIs to integrate with AI tools
4. Breakthrough Ideas
The AI for Math Fund will support some high-risk, high-return ideas for applying AI to fundamental mathematics and applications, such as:
Expected difficulty estimation (of sub-problems of a proof)
Novel mathematical implications of proofs formalized type-theoretically
Formalization of proof complexity in proof assistants
AI for Math Fund
Fund Details
Individual grants: up to $1M for up to 24 months of work on open-source projects and research
Open to individuals and teams worldwide
Read more in the AI for Math Fund Details Document
Application Deadlines
Web form: 11:59:59 pm PDT on January 10, 2025
Proposal: 11:59:59 pm PDT on March 10, 2025
Decisions: By June 2025
Application Process
Submit this simple application.
Selected applicants submit a full proposal.
Selected applicants may be asked to discuss their proposals.
Advisors
Click here for a list of AI for Math Fund advisors.
Eligibility
Applicants should have a strong background in formal verification, AI, proof assistants, or mathematics.
IP and Data Sharing
All code, datasets, and research outputs must be open-access, with preprints shared in public repositories.
Contact
Team
Tom Kalil, CEO, Renaissance Philanthropy
Tom Kalil is the CEO of Renaissance Philanthropy. Tom served in the White House for two presidents (Obama and Clinton) and in collaboration with his team worked with the Senate to give every federal agency the authority to support incentive prizes for up to $50 million. Tom also designed and launched dozens of White House science and technology initiatives, including the $40 billion National Nanotechnology Initiative, announced by President Clinton; The BRAIN Initiative, announced by President Obama; The Next Generation Internet initiative, announced by President Clinton and Vice President Gore; and initiatives in advanced materials, robotics, smallsats, data science, and EdTech.
Tom also served as the Chief Innovation Officer at Schmidt Futures, a philanthropic initiative of Eric and Wendy Schmidt. At Schmidt Futures, Tom supported the launch of Convergent Research, an organization that incubates and launches Focused Research Organizations, timebound non-profit organizations designed to accelerate scientific progress. Tom Kalil serves as Chair of Convergent Research. Tom also serves as a Member of the Board of Future House, a non profit focused on building AI-powered assistants for the laboratory.
Ralph Abboud, Technical Fellow
Ralph is a Technical Fellow at Renaissance Philanthropy, leading our Artificial Intelligence initiatives, including AI for math and AI for education. In this role, Ralph supports the implementation, design, and development of AI pipelines across our programs (LEVI, AI for Math Fund), and advises on selecting promising AI solutions and future technical initiatives. Before joining RenPhil, Ralph developed prototypes and evaluated AI models for education and helped design and execute the Feedback Prize competition series.
Ralph holds a D.Phil in Computer Science from the University of Oxford, specializing in graph representation learning (GRL). Before his D.Phil, Ralph completed an M.Sc in Computer Science at the University of Oxford, studying neural approaches for program synthesis, and a B.E. in Computer Engineering from the Lebanese American University.
Truman Liu, Fellow
Truman Liu is a Fellow at Renaissance Philanthropy, where he leads program strategy, grant funding, community-building, impact tracking, and program operations for initiatives including AI for Math and AI and Education.
He brings relevant experience managing education programs at Schmidt Futures, a philanthropic initiative of Eric and Wendy Schmidt. Prior to that, Truman worked in education technology across U.S. school districts (including for 500,000+ K – 12 students at Los Angeles Unified), as well as the nonprofit and philanthropic spaces in the US, Africa, and Latin America. Truman previously advised Fortune 500 companies as a consultant; he managed complex operations for a $50B+ merger across 10,000+ employees, stood up a Fortune 100 center of excellence to standardize processes, and implemented a $25M cost reduction strategy across three continents.
Truman received his MBA / MA Education from Stanford University and his BA from Georgetown University.