Imperial is unlocking the potential of artificial intelligence to power modern mathematics research thanks to support from Renaissance Philanthropy.
A generous grant from Renaissance Philanthropy has launched a pioneering two-year research project, led by Professor Kevin Buzzard in the Department of Mathematics. This support marks the first gift from Renaissance Philanthropy to Imperial and is part of the AI for Math Fund – managed by Renaissance Philanthropy in partnership with founding donor XTX Markets to support projects that maximise the use of AI.
The project aims to accelerate modern mathematics research by creating a substantial public dataset of formalised statements from recent journal publications. Translating mathematical concepts into a formal language with strict syntax not only reduces ambiguity for humans, but also allows computers to interact with mathematics in new ways.
While digital tools such as proof assistants and AI have shown promise in generating basic mathematical proofs autonomously, current technologies are limited to school-level mathematics, which are far from the scope of research that scientists are engaging in today. Professor Buzzard's team will push these boundaries by formalising the statements of hundreds of complex research-level theorems across many areas of mathematics, both increasing the vocabulary of modern theorem provers and providing an extensive and challenging autoformalisation dataset for AI systems.
Empowering world-class talent
Accelerating the formalisation of mathematics is a necessary part of accelerating mathematics itself. Professor Kevin Buzzard Professor of Pure Mathematics
With this funding, Professor Buzzard will recruit four postgraduate researchers to undertake research and help build the dataset. They will work with Lean, a programming language widely regarded as the best tool for formalising mathematics. Imperial's Department of Mathematics is home to many Lean experts, making it the ideal environment for the postgraduate researchers to grow and thrive in the next two years.
Professor Kevin Buzzard, Professor of Pure Mathematics, said: "Accelerating the formalisation of mathematics is a necessary part of accelerating mathematics itself. To speed up this process, we need tools that can do the complex work of formalising, or tools that can support humans doing this work. We have seen how AI supports groundbreaking discoveries in fields such as medicine and engineering, and I believe it has an untapped potential for mathematics.
"Philanthropic support from Renaissance Philanthropy is enabling us to change the landscape of modern mathematics, helping mathematicians solve challenges that we encounter today and those we will encounter in the future. We are grateful for this opportunity and are excited to embark on this journey to achieve what was previously thought impossible."
Researchers have long aspired to build systems capable of autonomously solving deep open mathematical problems. However, at present, AI systems operating at this level typically use human language and are thus open to hallucinations – a phenomenon where AI generates responses that are misleading, incorrect or entirely fabricated. The team's dataset will be pivotal in bridging this gap, providing the training data AI systems need to better understand and eventually assist with formalising more complex mathematical statements and, ultimately, proofs.
Demonstrating how AI can accelerate progress in mathematics research will encourage more mathematicians to adopt AI in their work, contributing to nurturing and attracting talent in this field which is vital in growing the area of mathematical formalisation.
Tom Kalil, CEO of Renaissance Philanthropy said: "We are excited by the convergence of AI and mathematics, where the collaboration of mathematicians and computer scientists could lead to the discovery of new mathematical theorems, improve the reasoning capabilities of AI models, and strengthen hardware and software security. We are excited to partner with Imperial to formalize cutting-edge mathematics research and are looking forward to the transformational opportunity that Professor Buzzard's project brings to the field."
