“This grant gives me a foothold in a new world where AI can be used in a very concrete way,” says Leykin. “It’s an opportunity to move beyond the hype and develop tools that truly benefit mathematical research.”

With a total of $18 million in inaugural grants to 29 project teams, the AI for Math Fund backs initiatives that create open-source tools, expand high-quality datasets for AI training, and make advanced systems more accessible to mathematicians. The fund received 280 grant applications from researchers and mathematicians worldwide. 

Building bridges

Leykin’s global team includes researchers from the University of South Carolina, University of Warwick, and Cornell University. Their project, “Bridging Proof and Computation: For a Verified Lean-Macaulay2 Interface,” aims to connect two powerful systems: Lean, a platform for assisting and formalizing mathematical proofs, and Macaulay2, a computational algebra system widely used in research.

By developing a native interface — a built-in connection that allows the two systems to work together without external tools — and a Lean-based domain-specific language, the project will enable communication between these systems. This will allow Lean users to formulate tactics that involve sophisticated computation done by algorithms implemented in Macaulay2; in return, Macaulay2 users can formalize computer-assisted proofs via Lean with a little help from AI.

“This integration has the potential to transform how mathematicians work,” says Leykin. “It will not only connect Lean and Macaulay2 but also lay the groundwork for a general interface that could benefit other computer algebra systems in the future.”

His goal is to create a robust proof-assistance system where AI can help generate strategies and validate proofs, driving progress in areas that require both computational power and rigorous verification.

About the AI for Math Fund

A joint initiative developed in partnership between Renaissance Philanthropy and founding donor XTX Markets, the AI for Math Fund is one of the largest philanthropic commitments supporting the development of AI and machine learning tools to advance mathematics. Individual grants range up to $1 million for 24 months of work on open-source projects and research.