CV

Education

Cambridge Logo PhD in Computer science - University of Cambridge, Exp. 2028
PhD on automated conjecture generation and theorem proving with AI systems.
Supervisor: Prof. Mateja Jamnik, Professor of Artificial Intelligence at the University of Cambridge.

Paris Cite Logo MSc in Mathematics - Paris Cite University, Exp. 2024
Master’s degree in mathematical logic, with a thesis on automated theorem proving.
Grade: Incoming.

Sorbonne Logo MSc in Mathematics - Sorbonne University, 2023
Master’s degree in machine learning, with a thesis on automated theorem proving.
Grade: First Class Honours (16.0/20).

Experience

Numina Logo Core contributor - Project Numina, since 2024
Part of the Model and RL teams, where I build an interaction pipeline with Lean4, implement Monte Carlo tree search and train models for theorem proving in Lean4.

Cambridge Logo Research intern - University of Cambridge, 2023
Research internship on automated theorem proving with Isabelle, using Monte Carlo tree search combined with LLaMA and GPT-2.
Supervisor: Dr. Wenda Li, Research Associate at the University of Cambridge.

OpenAI Logo Research intern - OpenAI, 2022
Research internship on automated theorem proving and auto-formalisation with Lean3, using GPT-3.5 trained with expert iteration on synthetic data.
Supervisor: Stanislas Polu, Research Engineer at OpenAI.

Publications

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)
📄 Paper | 🤗 Model | 🤗 Dataset | Code

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)
📄 Paper | 🤗 Dataset | Code

Awards and honours

EleutherAI Scholarship, 2024
Awarded a $265k scholarship by EleutherAI to fully support my PhD on AI for mathematics.

École normale supérieure Data Challenge, 2023
1st place out of 107 participants at the École normale supérieure Data challenge organised by Inria. Invited to the awards ceremony at Collège de France to present my solution.

Research impact

OpenWebMath has been cited over 70 times and 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;
Kimi to train their Kimi k1.5 model;
several academic researchers to build reasoning models (e.g., Quiet-STaR by Stanford researchers).

Llemma has been cited over 280 times, and the ProofPile dataset has been used by Mistral AI researchers to evaluate the long context performance of their Mixtral of Experts model.