Rémy Degenne

Rémy Degenne is a researcher at Inria in Lille who works on bandit theory and sequential machine learning, and who wants machine learning theory written and verified in proof assistants like Lean. After a PhD under Vianney Perchet from 2015 to 2019, he worked at CWI Amsterdam with Wouter Koolen and coauthored Non-Asymptotic Pure Exploration by Solving Games with Koolen and Pierre Ménard in 2019. A 2023 COLT paper of his showed that for several fixed-budget identification tasks no single algorithm attains the best possible rate everywhere, and in 2023 he also coauthored a Mathlib formalization of Doob's martingale convergence theorems with Kexing Ying. In 2025, he launched the FORMAL Inria exploratory action to formalize bandit and reinforcement learning algorithms in Lean, and he coauthored a Lean formalization of Brownian motion with David Ledvinka, Etienne Marion and Peter Pfaffelhuber. He is a tenured researcher in the Scool team at the Inria centre at the University of Lille and a Mathlib maintainer, and in January 2026 he was among the main organizers of the Lean Together 2026 meeting.

Now at: Inria
Works: 40
Citations: 291
h-index: 7
Badges: Wayfarer

Publication numbers from OpenAlex, as of 22 October 2026.

Timeline

2015–2019

PhD under Vianney Perchet

From 2015 to 2019, he is a PhD student under Vianney Perchet at the CMLA research center of École Normale Supérieure Paris-Saclay and the LPSM lab at Université Paris Cité. His PhD is in applied mathematics.
2018–2020

CWI Amsterdam and SIERRA

From 2018 to 2019, he works in the Machine Learning group at CWI Amsterdam with Wouter M. Koolen. In 2020, he is a postdoctoral researcher at Inria Paris, in the SIERRA team.
2019

Pure exploration as a game

In 2019, he coauthors Non-Asymptotic Pure Exploration by Solving Games with Wouter M. Koolen and Pierre Ménard. The paper treats the optimisation problem behind pure exploration as an unknown game and uses no-regret learners to obtain the first finite confidence guarantees adapted to the exponential family that apply to any pure exploration query and bandit structure.
2022

An ANR grant for FATE

In 2022, he is awarded ANR JCJC funding for his project FATE (Frugal and adaptive testing). The project will fund a PhD and a post-doc on bandits and sequential testing.
2023

Fixed-budget bandits and Doob in Lean

In 2023, he publishes On the Existence of a Complexity in Fixed Budget Bandit Identification at COLT, which shows that no single algorithm attains the best possible rate everywhere for several fixed-budget tasks, including Bernoulli best arm identification with two arms. With Kexing Ying, he also publishes A formalization of Doob's martingale convergence theorems in mathlib at CPP 2023. In November 2023, he contributes to the formalization of the polynomial Freiman-Ruzsa conjecture in Lean, a project led by Terence Tao.
2025

FORMAL and Brownian motion

In July 2025, he launches the FORMAL Inria exploratory action, whose goal is to formalize bandit and reinforcement learning algorithms and their theory in the Lean theorem prover. In November 2025, he, David Ledvinka, Etienne Marion and Peter Pfaffelhuber post Formalization of Brownian motion in Lean, which builds on Mathlib's measure-theoretic foundations and develops the Carathéodory and Kolmogorov extension theorems, Gaussian measures in Banach spaces, and the Kolmogorov-Chentsov theorem.
2026

Lean Together and AI talks

In January 2026, he is one of the main organizers of Lean Together 2026, the online meeting of the Lean and Mathlib community. In June 2026, he gives the talk Towards stochastic calculus in Lean in a Cambridge series on the formalisation of mathematics with interactive theorem provers, covering the Brownian motion project and its next step, formalizing stochastic integrals. In July 2026, he gives the CRIStAL seminar Proving theorems with Lean and Artificial Intelligence in Lille.
As of October 2026

Researcher and Mathlib maintainer

He is a tenured researcher in the Scool team at the Inria centre at the University of Lille, where he works on sequential machine learning, mostly bandit theory, and he is a maintainer of Mathlib and of the Lean Machine Learning project. He wants machine learning theory to be written and verified in proof assistants like Lean.