Three research projects in the Department of Applied Mathematics and Theoretical Physics (DAMTP) are among 22 winners worldwide of grants from the AI for Math Fund, run by Renaissance Philanthropy and funded by XTX Markets.
The AI for Math Fund seeks to accelerate the pace and impact of mathematical discovery by supporting projects that have the potential to advance the field as a whole.
The successful projects have each been awarded a share of a total of $17.1 million in funding across all 22 grants. The funding round was expanded beyond its originally announced $10.5 million in response to the exceptional strength of applications. More than 470 submissions were received.
At a time when AI in research mathematics is making headlines – producing new results while also reinforcing the importance of human input and community in making discovery meaningful – the three grant-winning projects in DAMTP span an exciting range of investigations and approaches.
"It's like we've been handed an alien tool. It's incredibly powerful, but we're all still figuring out how to use it," says Miles Cranmer, Assistant Professor in Data Intensive Science in DAMTP and the Institute of Astronomy, who leads or co-leads the DAMTP projects. "AI can now write mathematical proofs that a computer can check are correct, but, as written, these proofs might teach us nothing and be hard to understand. And throughout the history of mathematics, solving a hard problem has usually meant coming up with a new idea."
Translating the alien manual
One project, led by Matthew Colbrook, Associate Professor in DAMTP, and Miles Cranmer, develops open-source software that helps mathematicians read, edit, and learn from formal proofs (written in Lean, a language that lets a computer check every step) – particularly the long ones, written by people or AI, that are increasingly common.
"Taking a computer-generated part of a proof and trying to extract new ideas from it is a pretty unusual way of doing maths. We also want to explore the interaction between humans and AI in mathematics, taking the best of both worlds," says Matthew Colbrook. "It is crucial that AI-generated mathematics increases the understanding of the user through this interaction. We think AI is so powerful that we really have to try new things to get the most out of it. This is a high-risk, high-reward project."
"In astrophysics, for example, much of the work is already computerised, and there are specialised tools to help you understand computer outputs," adds Cranmer. "A simulation might generate huge amounts of raw data, and you need visualisation and analysis tools to actually learn anything from it. We think that AI-generated mathematical proofs need analogous sorts of tools."
Another of the grant-winning projects, led by Alessandro Favero, Physics-AI Fellow in DAMTP, and Cranmer, studies how mathematical information is represented, composed, and used inside language models and AI systems built to prove theorems. How do language models do mathematics? When an AI system proves a theorem, is it recognising the structure of the problem or matching patterns? And when it writes out its reasoning, do the steps reflect the computation happening inside? The aim is to build on this understanding to release open tools, datasets, and benchmarks to help mathematicians trust, debug, and learn from AI-generated proofs.
"AI's mathematical abilities have advanced faster than our understanding of how these systems work," says Favero. "By performing experiments on the models' internals, we aim to uncover the mechanisms behind those abilities, so that when a model fails, we can diagnose why, and when it succeeds, we can see what it has to teach us."
Better questions and building community
The third grant-funded project in DAMTP is also led by Cranmer. AI systems are becoming increasingly capable of proving and formalising mathematics, but they still need better tools for generating useful conjectures: statements that mathematicians suspect are true but have not yet proved.
This project focuses on developing an open-source 'conjecture engine', alongside building the developer and community infrastructure to support it. The project builds on PySR, an open-source symbolic regression tool, which uses machine learning to find mathematical relationships. "AI is good at finding answers. With PySR, we want to make AI better at asking questions too, by having it discover interesting relationships that can point mathematics in new directions," explains Cranmer.
Alongside the funding awarded to these three projects, the Isaac Newton Institute for Mathematical Sciences, DAMTP's neighbour in Cambridge, has won a grant for a residential programme on AI for Maths. The programme aims to bring together the world's leading mathematicians who use – or want to use – AI tools alongside researchers advancing AI methodology. In addition to the potential for catalysing ideas and new advances, the programme aims to support and build community consensus on standards for research transformed by AI, and for the evaluation of AI-assisted work.