This is a postdoctoral position in the Scool team, which specializes in machine learning applied to sequential decision making. The position is funded by the Inria exploratory action FORMAL.
The goal of the postdoc is to formalize machine learning algorithms in the Lean theorem prover 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.
Lean is a programming language and theorem proving assistant.
We can write programs in Lean, but also write theorems and proofs about those programs or any mathematical objects. Mathlib is the mathematical library of Lean. It contains most of the content of a Masters degree in mathematics, in particular many results of probability theory and analysis.
The obvious advantage of formal proofs is correctness: if the system accepts a proof, it is correct.
The real gain is however in what the certainty allows.
Since the computer checks the proofs, many people can work on a project without needing to trust each other.
Furthermore, once an algorithm and its proof are described in a formal language it becomes easier for a machine learning algorithm to interact with it, for example by generating new algorithms or proofs and getting feedback from Lean about their correctness.
Lean is therefore at the center of the recent efforts to use AI to assist in mathematical proofs.
