Dear proof assistant users,
I would like to advertise an open position at ENS Lyon on the translation between formal mathematics libraries using machine learning techniques.
The purpose of this postdoc is to experiment with both open-weight and closed-weight models to evaluate how LLMs can help bridge gaps between mathematical libraries of different proof assistants, and is a part of larger project of using LLMs to assist proving and programming at Inria.
The expected challenges are: build datasets, embeddings, and and AI agents, perform trainings, finetunings or RAG, but also find tactics/proof patterns that are suitable for AI translations and possibly bridge gaps between proof assistants available tactics.
Best wishes