Imperial mathematician receives grant to formalise theorems with AI
The goal is to create a robust resource for future research
Professor Kevin Buzzard of Imperial’s Department of Mathematics has been awarded a two-year grant from the AI for Math Fund. This will allow him to establish a research group focused on formalising advanced mathematics.
The fund was launched by Renaissance Philanthropy and XTX Markets with an initial commitment of $9 million to support work at the convergence of mathematics and artificial intelligence. Buzzard’s project will create a public dataset by encoding research level theorems into formal languages such as Lean. Four postgraduate researchers will join the group.
Buzzard noted that current AI systems are tested mainly on International Mathematical Olympiad problems or undergraduate material. “These are problems which humans already know how to solve,” he said. “If we want to make machines which can help humans and accelerate mathematics, we definitely need them to be able to understand what’s going on at the boundary of modern research.”
A central aim of the project is to address the problem of AI “hallucinations,” where models generate plausible but incorrect arguments. “Within the context of mathematics Lean is a potential solution,” Buzzard explained. “Our work will create a super-hard dataset of challenges of this nature; if a machine can translate the proofs into Lean given only the statements, then we have digitised the paper, we have checked it for errors, and we are on the way to developing a tool which can help humans referee maths papers.”
The group will focus on turning recent theorems into Lean, with humans defining hard mathematical objects and machines tasked with producing the proofs. The team aims to compile a database of at least 100 recent theorems, as well as the definitions they depend on - integrated into Lean’s mathematics library.
Buzzard pointed that the project focuses on strengthening foundations rather than producing new discoveries. “This is about creating a resource that future tools can build on,” he said.
