My picture

How can computers find mathematical proofs? That’s the topic of my PhD, which I’m doing under the supervision of Tim Gowers. I’m interested in all kinds of interactive and automated theorem proving, in particular for research grade mathematics. You can find out more about my research group here.

Recent Work

LLM + Lean + Reinforcement Learning

Jointly with collaborators at Numina we managed to achieve state of the art on the miniF2F benchmark twice with Kimina-Prover and Kimina-Prover Preview. This shows that LLMs can solve challenging high school competition maths problems formalized in Lean, an important stepping stone towards tackling research level mathematics. Our dataset, RL pipeline and Lean Server infrastructure have all been open sourced. I gave an invited talk about this work at AITP, together with Mantas Bakšys.

New Number Theory Result: Formalise as You Research

Together with Marco David, I presented our formalisation of a stronger version of Hilbert’s Tenth Problem at ITP. This work constitutes a new way of doing mathematical research: we develop a novel result about Diophantine Equations in parallel to formalising it in Isabelle/HOL. This is currently the largest contribution to the Isabelle Archive of Formal Proofs in terms of the number of authors; throughout the project we managed 13 student collaborators and taught them how to use Isabelle.

What Is the Future of Mathematical Proof?

Our survey paper Mathematical Proof Between Generations in the Notices of the American Mathematical Society aims at sheding light at this question. With contributions from, among others, Kevin Buzzard, Yuri Matiyasevich, Larry Paulson and Efim Zelmanov.

Publications

You can find a complete list of my publications on my Orcid page.

Lean Workshop

This section contains material for the Lean workshop at the event UK welcomes Studienstiftung.

Schedule

Material for Mini-Projects

Project A: Beyond the Natural Number Game: What’s your favourite (undergraduate-level) theorem in mathematics? The idea of this mini-project is to explore how a theorem of your choice is formalised in Lean. You can use the search bar in the Mathlib documentation and refer to search tools listed below. Probably, what you get out of this won’t make a lot of sense at first. Take a look at the book Mathematics in Lean to learn more about how to do formalisation beyond the Natural Number Game.

Project B: A New Understanding of Mathematical Proof: How does formalisation with tools like Lean change how we view mathematical proofs? Or does it not? The idea of this mini-project is to analyse how the adoption of formalisation in mathematical research can change the conception of what constitutes a proof. The material below focuses on perspectives from mathematicans and computer scientists. If you have a background in philosophy: how do various philosophers think about the concept of mathematical proof? Can you find literature on the topic and make a comparison?

Project C: Lean meets AI: Recently, Lean has played an important role in the development of AI systems for mathematics. How do these AI systems work? What are their limitations? And how does Lean come into the picture? The mini-project is to shed light on these questions by analysing the examples linked to below. Note that, recently, a lot of work has focused on solving problems from the International Mathematical Olympiad (IMO). These problems can be explained to anyone with a high-school level understanding of mathematics but are very challenging to solve, requiring multi-step reasoning.