Postdoc position: Inria centre at the University of Lille

Stream: job postings

[Rémy Degenne]

I am looking for a candidate for a postdoc to formalize machine learning algorithms in Lean and eventually explore the use of AI to design algorithms and prove theoretical guarantees about them. The starting goal will be to formalize bandit algorithms.
The desired start date is January 2026 and the position is funded for 18 months. The work will take place in the Scool team at the Inria centre at the University of Lille, France, under my supervision. The funding includes money to attend conferences, and the position does not involve any teaching.

The goal of the project is to implement a type of machine learning algorithms called stochastic bandits [Lattimore, Szepesvari, 2020] in Lean, as well as the tools needed to run them on simulated environments, and prove their theoretical performance guarantees. The project should also be open to outside contributions and part of the job of the postdoc will be to manage the public project (maintain a blueprint, review PRs, etc.).
I am looking for a candidate with experience with Lean, and familiar with the mathematical concepts that can be found in the probability theory part of Mathlib, since stochastic bandits, like a large part of machine learning, models the interaction of the algorithm and its environment in a probabilistic way.
Knowledge of machine learning or even bandits would be appreciated, but is not essential.

The official offer will be open in a few weeks on Inria's dedicated job website, and the candidates will have to apply through that website. I'll update this announcement when the job offer is there.
In the meantime, please feel free to send me a message on this zulip for more information.

[Rémy Degenne]

The postdoc offer is online: please apply at https://recrutement.inria.fr/public/classic/fr/offres/2025-09199

[Rémy Degenne]

I forgot to mention the application deadline: it's in two days, September 5.

[Rémy Degenne]

This position is still open. If you are interested in formalizing machine learning theory in Lean, send me a DM.