Autoformalising Habiro rings
As of November 2026, I have been awarded a UKRI Future Leaders Fellowship that will support my research over the next four years. The project will use AI to formalise and explore ongoing research on Habiro rings, algebraic K-theory, their connections to the Langlands programme, and algebraic number theory more broadly.
Projects such as Tau Ceti are rapidly expanding formal libraries of mathematics, which will open up new ways to do research. The fellowship aims to develop tools to help mathematicians and AI systems extract new insights from these libraries and tackle major open problems in new ways.
My goals include: autoformalising current research and using Lean to produce stronger results, find new proofs and stating new conjectures. Moreover, we will be developing retrieval-augmented generation (RAG) systems that help AI draw on relevant mathematical knowledge to create mini-AI experts in certain areas of mathematics and perhaps even fine-tuning small-ish open-source language models, to take this one step further. The ultimate goal is to help humans understand the complex mathematics produced by mathematicians and AI systems.
As part of the project, I will recruit two postdoctoral researchers, each on a three-year contract, and a PhD student. The team will have access to frontier AI models and travel funds to support independent research in algebraic number theory. We will also work in partnership with Kevin Buzzard’s Langlands Lab at Imperial College London, with regular visits, meetings and collaboration towards our shared goals.