Research

I am primarily interested in algebraic geometry-especially the enumerative geometry and connections to number theory-the mathematics of machine learning, and formal mathematics.

Publications

Papers

Research papers and preprints

01
Journal article Nature

Olympiad-level formal mathematical reasoning with reinforcement learning

With Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z. Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, Ottavia Bertolli, Tom Zahavy, Amol Mandhane, Jessica Yung, Iuliya Beloshapka, Borja Ibarz, Vivek Veeriah, Lei Yu, Oliver Nash, Salvatore Mercuri, Calle Sönne, Bhavik Mehta, Alex Davies, Daniel Zheng, Fabian Pedregosa, Yin Li, Ingrid von Glehn, Mark Rowland, Samuel Albanie, Ameya Velingker, Simon Schmitt, Edward Lockhart, Edward Hughes, Henryk Michalewski, Nicolas Sonnerat, Demis Hassabis, Pushmeet Kohli and David Silver .
- Formal mathematics
- AI theorem proving
- Reinforcement learning
02
Conference paper ICML 2026 · ICLR 2026 VerifAI-2 Workshop

SorryDB: Can AI Provers Complete Real-World Lean Theorems?

With Austin Letson, Leopoldo Sarra, Auguste Poiroux, Oliver Dressler, Dhyan Aranha, Frederick Pu, Aaron Hill, Miguel Corredera Hidalgo, Julian Berman, George Tsoukalas and Lenny Taelman .
- Formal mathematics
- AI theorem proving
03
Research paper Preprint

Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics

With Moritz Firsching, Salvatore Mercuri, Miklós Z. Horváth, Yaël Dillies, Calle Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas and Pushmeet Kohli .
- Formal mathematics
- AI theorem proving
04
Research paper Preprint

Non-Archimedean Polydisc Spaces and Applications to Optimisation

With Anthea Monod, Yiannis Fam and Yue Ren .
- Non-Archimedean geometry
- Optimisation
05
Research paper Preprint

Tubular Neighbourhoods of Pfaffian Sets and Applications to Neural Networks

With Martin Lotz .
- Algebraic geometry
- Neural networks
06
Research paper Preprint

Tropical Expressivity of Neural Networks

With Thomas Walker, Shiv Bhatia, Yueqi Cao and Anthea Monod .
- Tropical geometry
- Neural networks

Formalisation & collaboration

Projects

Formal Conjectures

An open and evolving benchmark for verified mathematical discovery.

GitHub repository

AlphaProof

Formal mathematical reasoning work contributing to an AI system that reached silver-medal-level performance at the International Mathematical Olympiad.

Project article