CV
Education
PhD in Computer science - University of Cambridge October 2024 - Present
Doctor of Philosophy in AI for formal mathematics.
Supervisors: Prof. Mateja Jamnik and Prof. Timothy Gowers.
MSc in Mathematics - Paris Cite University October 2023 - September 2024
Master’s degree in mathematical logic, with a thesis on automated theorem proving.
Grade: Incoming.
MSc in Mathematics - Sorbonne University October 2022 - September 2023
Master’s degree in machine learning, with a thesis on automated theorem proving.
Grade: First Class Honours (16.0/20).
Experience
Student Researcher - Google DeepMind August 2025 - Present
Research at the intersection of AI, mathematics, computation and creativity using AlphaProof.
Supervisor: Tom Zahavy, Staff Research Scientist at Google DeepMind.
Research Intern - University of Cambridge April 2023 - August 2023
Research internship on neural theorem proving in Isabelle, implementing a Monte Carlo tree search using large language models as policy and value models.
Supervisor: Wenda Li, Research Associate at the University of Cambridge.
Research Intern - OpenAI April 2022 - June 2022
Research internship on neural theorem proving and auto-formalisation in Lean 3, formalising olympiad problems and monitoring the reinforcement learning training of GPT-3.5.
Supervisor: Stanislas Polu, Research Engineer at OpenAI.
Selected Publications
Target-Based Automated Conjecturing for Neural Theorem Proving
Marco Dos Santos, Albert Q. Jiang, Wenda Li, Mateja Jamnik
AI for Math Workshop at ICML 2025 (Poster).
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
Project Numina & Kimi Team. Core contributor.
Preprint.
Llemma: An Open Language Model For Mathematics
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, Sean Welleck
ICLR 2024 (poster) and MATH-AI Workshop at NeurIPS 2023 (poster).
OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text
Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, Jimmy Ba
ICLR 2024 (poster) and MATH-AI Workshop at NeurIPS 2023 (oral & poster).
Research impact
Kimina-Prover was the first large reasoning model applied to theorem proving. It pushed the state-of-the-art on miniF2F (from 71% to 81% for the Preview version, and from 89% to 92% for the final version) and PutnamBench. The model has been used by:
- DeepSeek as the main baseline to compare their DeepSeek-Prover-V2 model;
- ByteDance Seed as a baseline and inspiration for their Seed-Prover model.
Llemma has been cited over 300 times. It was the best open-source model in mathematics when it was released, and it has been downloaded more than 300k times on Hugging Face. The model and its training dataset have been used by:
- Mistral AI to evaluate the long context performance of their Mixtral of Experts model on the Proof-Pile-2 dataset;
- DeepSeek as a baseline to compare their DeepSeekMath model;
- The Qwen team from Alibaba Group as an inspiration to train their Qwen2.5-Math models;
- Several academic researchers as a baseline and inspiration for their models (e.g., MetaMath and TinyLlama).
OpenWebMath has been cited over 70 times. It was the #1 trending dataset on Hugging Face when it was released. The dataset has been used by:
- DeepSeek to build the continued pre-training dataset for DeepSeekMath and DeepSeek-Prover models;
- Microsoft to continuously pre-train their Rho-1 model;
- The Kimi team from Moonshot AI to train their Kimi k1.5 model;
- Several academic researchers to build reasoning models (e.g., Quiet-STaR by Stanford researchers).
Awards and honours
EleutherAI Scholarship July 2024
Awarded a £168,000 scholarship by EleutherAI to fully support my PhD on AI for mathematics.
École normale supérieure Data Challenge March 2023
1st place out of 107 participants at the École normale supérieure Data Challenge organised by Inria. Invited to the awards ceremony at the Collège de France to present my solution.