Research

My research explores how large language models can learn to reason and make discoveries autonomously, spanning pre-training, post-training, and agentic systems.

Motivations

I first encountered the Lean proof assistant in 2021, through a research project in my pure mathematics curriculum. I was quickly fascinated by the potential of this tool and soon thought about combining Lean with AI systems. Inspired by AlphaGo and the work of Christian Szegedy’s team at Google, I became convinced that AI and proof assistants would play an important role in the future of mathematics, which led me to pivot toward AI.

Along the way, my interests expanded to broader questions about AI and the nature of intelligence, while mathematics remained both a personal passion and a rich testing ground for AI reasoning. Over the past four years, my work at this intersection has naturally followed developments in LLM research, moving from pre-training to post-training and, more recently, to agentic systems.

Research overview

• Pre-training: I co-developed OpenWebMath, a large pre-training dataset of mathematical web text, and Llemma, a family of open language models for mathematics.
• Post-training: I worked on Kimina-Prover, a reasoning model trained through reinforcement learning for theorem proving in Lean.
• Agentic systems: I helped build the Numina Lean Agent, which connects a general coding agent with tools for formal mathematics. At Google DeepMind, I also developed agentic systems to autonomously discover and formally verify mathematical rules describing the behaviour of Turing machines.

Future directions

Beyond using mathematics as a testbed for AI, a long-term goal is to use these systems to advance mathematics itself by investigating fundamental questions, exploring connections between theories, and deepening our understanding of the subject.