Science

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.”

Professor Kevin Buzzard Thomas Angus for Imperial College London

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.

Feature image: Professor Kevin Buzzard Thomas Angus for Imperial College London

Tagged in:

From Issue 1876

3 Oct 2025

Discover stories from this section and more in the list of contents

Explore the edition

Read more

University Challenge: Imperial dominates SOAS in qualifying round

News

University Challenge: Imperial dominates SOAS in qualifying round

Imperial College’s University Challenge team qualified for the second round of the hit quiz competition with a resounding victory of 220-115 against the School of Oriental and African Studies (SOAS). The team had “a hell of a performance” according to host Amol Rajan, as they now proceed further into

By Mohammad Majlisi
Speaking to the students behind the Zero Index

Environment

Speaking to the students behind the Zero Index

Imperial uses its Zero Index to assess which fossil fuel companies it should maintain research partnerships with. In the most recent round of assessments, the University approved BP, Equinor, ExxonMobil, Petronas, Shell, TotalEnergies, and Woodside Energy. Felix has been reaching out to the staff and students who worked on the

By Oscar Mitcham