About me
I am a tenured researcher in the Scool team at the Inria centre at the University of Lille. I work on sequential machine learning, mostly bandit theory, and I am interested in all forms of online and reinforcement learning as well as statistics and optimization. I am also passionate about formal mathematics and AI for maths and I want to transform machine learning theory by ensuring it can be written and verified in proof assistants like Lean.
I am a maintainer of the mathematical library Mathlib for the Lean theorem prover and of the Lean Machine Learning project.
If you are looking for something to contribute to Mathlib related to probability, here is a list of projects.
In 2020 I was a post-doctoral researcher at Inria Paris, in the SIERRA Team. In 2018-2019 I spent a year in the Machine Learning group at CWI Amsterdam, working with Wouter M. Koolen. From 2015 to 2019 I was a PhD student under the supervision of Vianney Perchet at the CMLA research center of Ecole Normale Supérieure Paris-Saclay and the LPSM lab at Université Paris Cité.
News
[July 2026] I am giving a tutorial at ICML 2026 on Proving Theorems with Lean and Machine Learning, with Wenda Li.
[January 2026] I organized the Lean Together 2026 online conference, the annual meeting for users, developers, and fans of the Lean programming language and theorem prover and its library Mathlib.
[December 2025] I gave talks about probability theory in Lean and the Brownian motion project at ItaLean 2025 (Bologna, Italy, December 9-12), a workshop about bridging formal mathematics and AI.
[October 2025] With Michael Rothgang, I am leading a workshop on Lean for PDEs at the Simons Laufer Mathematical Sciences Institute (SLMath), co-organized by the new Institute for Computer-Aided Reasoning in Mathematics (ICARM).
[July 2025] I am launching the FORMAL Inria exploratory action. Its goal is to formalize bandit and reinforcement learning algorithms and their theory in the Lean theorem prover. A post-doc will join the team in 2026 to work on this project.
[November 2023] I am contributing to the formalization of the polynomial Freiman-Ruzsa conjecture in Lean. This is a project led by Terence Tao, who recently proved this result with W. T. Gowers, Ben Green and Freddie Manners. See this post on Terence Tao's blog for a tour of the project.
Older news can be found on the Older News page.Publications
Last updated: January 2026. For a perhaps more up-to-date list, see my Google Scholar profile.- Formalization of Brownian motion in Lean, preprint RD, David Ledvinka, Etienne Marion, Peter Pfaffelhuber.
- Markov kernels in Mathlib's probability library, preprint RD.
- The Batch Complexity of Bandit Pure Exploration, ICML 2025 Adrienne Tuynman, RD.
- Best-Arm Identification in Unimodal Bandits, AISTATS 2025 Riccardo Poiani, Marc Jourdan, Emilie Kaufmann, RD.
- Finding good policies in average-reward Markov Decision Processes without prior knowledge, NeurIPS 2024 Adrienne Tuynman, RD, Emilie Kaufmann.
- Optimal Multi-Fidelity Best-Arm Identification, NeurIPS 2024 Riccardo Poiani, RD, Emilie Kaufmann, Alberto Maria Metelli, Marcello Restelli.
- An ε-Best-Arm Identification Algorithm for Fixed-Confidence and Beyond, NeurIPS 2023 Marc Jourdan, RD, Emilie Kaufmann.
- Non-Asymptotic Analysis of a UCB-based Top Two Algorithm, NeurIPS 2023 Marc Jourdan, RD.
- Fast Asymptotically Optimal Algorithms for Non-Parametric Stochastic Bandits, NeurIPS 2023 Dorian Baudry, Fabien Pesquerel, RD, Odalric-Ambrym Maillard.
- On the Existence of a Complexity in Fixed Budget Bandit Identification, Colt 2023. [HTML Version] RD.
- Dealing with Unknown Variances in Best-Arm Identification, ALT 2023 Marc Jourdan, RD, Emilie Kaufmann.
- A formalization of Doob's martingale convergence theorems in mathlib, CPP 2023 Kexing Ying, RD.
- Top Two Algorithms Revisited, NeurIPS 2022 Marc Jourdan, RD, Dorian Baudry, Rianne de Heide, Emilie Kaufmann.
- On Elimination Strategies for Bandit Fixed-Confidence Identification, NeurIPS 2022 Andrea Tirinzoni, RD.
- Choosing Answers in Epsilon-Best-Answer Identification for Linear Bandits, ICML 2022 Marc Jourdan, RD.
- Online Sign Identification: Minimization of the Number of Errors in Thresholding Bandits, NeurIPS 2021 Reda Ouhamma, RD, Vianney Perchet, Pierre Gaillard.
- Dealing With Misspecification In Fixed-Confidence Linear Top-m Identification, NeurIPS 2021 Clémence Reda, Andrea Tirinzoni, RD.
- Structure Adaptive Algorithms for Stochastic Bandits, ICML 2020 RD, Han Shao, Wouter M. Koolen.
- Gamification of Pure Exploration for Linear Bandits, ICML 2020 RD, Pierre Ménard, Xuedong Shang, Michal Valko.
- Non-asymptotic pure exploration by solving games, NeurIPS 2019 RD, Wouter M. Koolen, Pierre Ménard.
- Pure exploration with multiple correct answers, NeurIPS 2019 RD, Wouter M. Koolen.
- Bridging the gap between regret minimization and best arm identification, with application to A/B tests, AISTATS 2019 RD, Thomas Nedelec, Clément Calauzènes, Vianney Perchet.
- Bandits with side observations: bounded vs. logarithmic regret, UAI 2018 RD, Evrard Garcelon, Vianney Perchet.
- Combinatorial semi-bandit with known covariance, NIPS 2016 RD, Vianney Perchet.
- Anytime optimal algorithms in stochastic multi-armed bandits, ICML 2016 RD, Vianney Perchet.
Mathlib contributions
I am a contributor and a maintainer of Mathlib, the mathematics library of the Lean theorem prover. Here are some of my contributions, mostly related to probability:- A definition of Gaussian distributions in Banach spaces and Fernique's theorem. Coming soon: the Cameron-Martin theorem.
- The Kullback-Leibler divergence. Coming soon: other information divergences, notably related to the risk of statistical experiments.
- Sub-Gaussian random variables, moment generating functions and concentration inequalities.
- Independence and conditional independence.
- Probability transition kernels and their compositions. Disintegration of kernels and definitions of conditional distributions and posterior distributions. Radon-Nikodym theorem for kernels. See Markov kernels in Mathlib's probability library.
- Martingales and stopping times: Doob's martingale convergence theorems, optional stopping, optional sampling. See A formalization of Doob's martingale convergence theorems in mathlib, CPP 2023, Kexing Ying, RD.
- Conditional expectations.
- Lp spaces, the fact that they are Banach spaces and that L2 is a Hilbert space.
Teaching
Current courses- Centrale Lille, fall 2025 - Sequential learning
- ENS Paris-Saclay (Master MVA), spring 2025 - Sequential learning, with Pierre Gaillard
- ENS Paris-Saclay (Master MVA) - Sequential learning - 2021, 2022, 2023
- Centrale Lille - Sequential learning - 2022, 2023, 2024
- Université de Lille (L3 MIASHS) - Science des données 3 - 2022, 2023
- Université Paris Diderot - Practical sessions for various courses - 2016 to 2018. Courses: Analyse et algèbre 2 (L1 Physique), Raisonnement mathématique (L1 Informatique, L1 MIASHS), Probabilités (L2 Math-Info), Equation différentielles pour la biologie, Probabilités (L2 Math).
Collaborators
PhD students
- Redouane Yagouti, co-advised with Emilie Kaufmann, since October 2025.
- Adrienne Tuynman, co-advised with Emilie Kaufmann, since October 2023.
- Marc Jourdan, co-advised with Emilie Kaufmann, October 2021 - June 2024.
Post-docs
- Gaëtan Serré, starting December 2026.
- Nam Phuong Tran, since January 2026.
- Andrea Tirinzoni, 2021.
Master students
- Redouane Yagouti, co-supervised with Emilie Kaufmann, April-September 2025.
- Lorenzo Luccioli, April-September 2024.
- Adrienne Tuynman, co-supervised with Emilie Kaufmann, April-August 2023.
- Marc Jourdan, April-August 2021.