AI for Math Fund expands to $35.1m as new grants back open tools, theorem proving and AI-generated proofs

Renaissance Philanthropy and XTX Markets have added $17.1 million in funding after more than 470 applications, backing 22 projects working at the intersection of AI and mathematics

The AI for Math Fund has committed a further $17.1 million to projects spanning AI-assisted theorem proving, datasets and research tools

Renaissance Philanthropy and XTX Markets are committing a further $17.1 million to the AI for Math Fund, taking total funding pledged through the initiative to $35.1 million.

The 2026 Core Grants round was originally expected to distribute $10.5 million, but organizers expanded the pot following more than 470 applications. Twenty-two proposals representing 30 organizations have now been selected, with individual grants ranging from $100,000 to $1 million and supporting between 12 and 24 months of work.

Projects span AI-assisted theorem proving, research infrastructure, datasets, evaluation tools and new ways for mathematicians to work with and understand AI-generated mathematics.

Kumar Garg, President at Renaissance Philanthropy, wrote on LinkedIn that “the math field is undergoing a transformation in the age of AI,” describing the investments as an attempt to build an “open, vibrant, and ambitious research community.”

From AI proofs to tools mathematicians can actually use

The funded portfolio includes a new research pod at the Simons Institute focused on AI for mathematics and theoretical computer science.

Its work will center on AI-assisted theorem proving, where AI systems help researchers construct or verify mathematical arguments rather than simply producing an answer.

Another project, TorchLean, will extend an open framework that connects machine learning with Lean, a programming language used to formally check whether mathematical proofs are logically valid.

The funding will also support a visual proof environment intended to make long formal proofs easier for mathematicians to read and edit. The system will combine a browser-based Lean environment with AI assistance capable of suggesting smaller, computer-checkable steps within larger mathematical arguments.

This is becoming increasingly relevant as frontier AI systems begin producing more sophisticated mathematical work. The challenge is not only whether a model can generate a convincing answer, but whether researchers can inspect it, verify it and build on it.

Funding grows after more than 470 applications

The AI for Math Fund says almost 40 field experts contributed to a multi-stage assessment of the applications.

Its new grants fall broadly into four areas: benchmarks, evaluation and datasets; infrastructure and tooling; foundational research and more experimental projects; and wider efforts to build the AI-for-mathematics research community.

Simon Coyle, Head of Philanthropy at XTX Markets, says the fund is helping support “the open development of tools, training and community to accelerate AI-powered discovery in mathematics.”

Alongside its support for the AI for Math Fund, XTX Markets and its founder Alex Gerko have committed more than $35 million to other formal mathematics initiatives including Mathlib, the Formal Frontier autoformalization project and the Lean Focused Research Organization.

Tom Kalil, CEO of Renaissance Philanthropy, says: “XTX Markets’ investments have transformed formal mathematics and created a roadmap for other disciplines and funders to follow.”

Building an open AI-for-math ecosystem

The AI for Math Fund is focused on work that could benefit the wider field but may be difficult for a single university or commercial AI laboratory to justify funding independently.

That includes open-source software, larger and more varied mathematical datasets, tools for evaluating AI systems and infrastructure intended to make emerging AI capabilities usable by working mathematicians.

Renaissance Philanthropy says the aim is not simply to fund individual mathematical results, but to build shared resources that can support researchers across institutions.

XTX Markets has also become a substantial backer of mathematics education and research more broadly. The company says it has committed more than £90 million to UK charities and education institutions working in mathematics, as part of more than £400 million in philanthropic commitments since 2020.