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.
News
- I got accepted into the Cambridge AI Safety Hub fellowship.
- Research visit at LASIGE in Lisbon, Portugal, hosted by Alcides Fonseca, working on genetic programming and dependent type theory (preprint upcoming) (LASIGE talk).
Recent work
-
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.
-
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, and also presented it at Chalmers University of Technology in Sweden.