AI for Math Fund: 2025 Winners

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 supports projects that are less likely to happen in a business-as-usual scenario, and 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.

The Fund’s first 29 grant awards will go to researchers at universities and organizations to support their efforts to develop systems that help advance mathematical discovery and research across several key tasks.

The inaugural AI For Math Fund portfolio comprises of researchers and universities and organizations developing systems that help advance mathematical discovery and covers a breadth of key topics and bottlenecks in AI for Math research, including:

  • Key dataset development

  • Improved prover - mathematician interaction

  • Core functionality and coverage improvements

  • Promising field-building initiatives

  • High-ambition moonshots

2025 Winners

  • An AI-Focused Tactic for Language Learning

  • A Dataset of Modern Formalized Theorem Statements

  • A Principled Approach to Proof Search with Applications to Siderenko’s Conjecture

  • A Structured Representation of Tactics for Machine-Assisted Theorem Proving

  • Bridging AI, Proof Assistants, and Mathematical Data (BRIDGE)

  • Bridging Complexity and Automation to Advance Automatic Theorem Proving

  • Bridging Proof and Computation

  • Constraining LLMs for Theorem Proving

  • Crowdsourcing and Reinventing the Next Generation of Dynamic and Scalable Math Benchmarks

  • Databases of Structured Motivated Proofs

  • Document-Level Autoformalization

  • Domain Specific Documentation for Mathlib

  • Large Language Models for Lattice-Theoretic Reasoning of Reactive Programs

  • Learning to do Math with Vampires and Spiders

  • New Categorical and Topological Foundations For AI and Machine Learning

  • Scalable Theorem Proving via Mathematical Databases

  • Towards Automated Mathematical Discovery