Lead AI Researcher: LLMs for Formal Math (BELLE)

Inria Paris recherche une personne pour diriger l'axe IA du projet BELLE, superviser le post-doctorant et les stagiaires, et coordonner les activités en interface IA, méthodes formelles et mathématiques.

Le poste implique la conception du jeu de données BELLE-Prefs, l'évaluation de la qualité du code Lean et la diffusion des artefacts, avec collaboration internationale et interaction avec Mathlib et Rocq.