Publications

Numina Lean Agent January 2026

Preprint.
Numina Lean Agent is an open-source agentic system for theorem proving, which solved all problems from the William Lowell Putnam 2025 Competition (12/12).
Following the success of the initial version, I am now taking an active role in developing the second iteration of the agent.

Target-Based Automated Conjecturing July 2025

AI for Math Workshop at ICML 2025 (Poster).
This paper corresponds to my first PhD project. The objective is to make the reinforcement learning phase of theorem proving models fully autonomous by automatically generating the training statements.
I am leading this project, and I am currently working to scale up the approach.

Kimina Lean Server July 2025

MATH-AI Workshop at NeurIPS 2025 (Poster).
Kimina Lean Server is an open-source project designed as a high-performance Lean 4 verifier for large-scale training of theorem proving models. It is the most efficient Lean-Python interaction server, significantly faster than existing alternatives.
I was the main contributor to this project, building the initial prototype. I was then joined by Haiming Wang and Hugues de Saxcé, who helped scaling up and maintaining the system.

Kimina Prover April 2025

Preprint.
Kimina Prover is a large reasoning model trained for theorem proving in Lean 4. It was the first large reasoning model applied to theorem proving, and 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.
For this project, my main contributions were initially focused on the Lean Server, where I was the primary contributor to enable large-scale training across hundreds of CPUs. I also explored various tree search algorithms (which ultimately did not yield strong results) before shifting my focus to the reinforcement learning codebase.

Llemma October 2023

ICLR 2024 (Poster) and MATH-AI Workshop at NeurIPS 2023 (Poster).
Llemma is a family of open-source language models for mathematics, trained on OpenWebMath and other mathematical/coding datasets. It was the best open-source model in mathematics when it was released.
My contribution focused mostly on preparing the training data, specifically the OpenWebMath dataset and a dataset of formal proofs written in Isabelle.

OpenWebMath October 2023

ICLR 2024 (Poster) and MATH-AI Workshop at NeurIPS 2023 (Poster).
OpenWebMath is a large dataset of high-quality mathematical web text extracted from the web. It was built as an attempt to replicate Google’s Minerva model, which was trained on a closed dataset of every mathematical document on the web, something that wasn’t available to the academic community.
I contributed to most parts of the project, and learnt a lot from working closely with Keiran Paster, especially on the programming side.