AI for Math Winners (www.renaissancephilanthropy.org)

The AI for Math Fund announced its inaugural portfolio of 29 grants for 2025, seeding projects that aim to accelerate mathematical discovery by building tools, datasets, and interfaces unlikely to be funded in normal academic or industry pipelines. The awards prioritize open-source, production-quality software, larger and more diverse formal datasets, and usability improvements so working mathematicians will actually adopt AI-assisted workflows. By deliberately targeting gaps—ranging from core infrastructure to high-ambition “moonshots”—the fund is positioning the community to make broad, reusable progress rather than isolated wins. Technically, the funded work spans dataset construction (modern formalized theorem statements, Mathbench, structured motivated-proof databases), proof automation and search (principled proof search methods, GNN-SMT, scalable theorem proving via mathematical databases), interaction layers (Copilots for Isabelle, LeanAide, LeanTutor, structured tactic representations), and autoformalization (document-level autoformalization, BRIDGE). Several projects explicitly explore how to constrain or augment LLMs for robust theorem proving and bridge symbolic computation with proof assistants, while others build benchmarks and tooling to grow the ecosystem (Polymath Plus, Vellum). Together these efforts target reproducibility, composability, and human-in-the-loop workflows that could materially improve automated theorem proving, make formalization more tractable, and speed the discovery cycle in pure and applied mathematics.