Missions

Le projet a pour objectif de participer au développement d’une nouvelle génération d’assistants à la preuve, qui intègrent dans leurs noyaux une couche linguistique et des outils d'assistance automatisée pour guider le scientifique et faciliter la construction de documents mathématiques certifiés, depuis le choix des concepts et des définitions, jusqu’à l'élaboration des théorèmes et des démonstrations.

Activités

• Conception, implémentation et expérimentation d’une couche linguistique dans un assistant à la preuve,
• Développement d’outils d’extraction de paramètres (feature extraction) de larges corpus de mathématiques formalisées
• Gestion incrémentale de ces larges corpus de mathématiques formalisées
• Développement d'un environnement de type Gym pour permettre à l’IA d’interagir avec l’assistant à la preuve
• Intégration d'un éditeur de code et d’une interface graphique pour permettre à un utilisateur humain d’interagir avec l’assistant à la preuve et l’IA

Compétences

• Expert en programmation OCaml et Python
• Bonne connaissance d’un assistant de preuve tel que Agda, Isabelle, Lean ou Rocq sur les aspects formalisation et implémentation interne
• Expérience de développement d’interface utilisateur, notamment avec les éditeurs de code moderne tels que VSCode et Jupyter
• Bonne connaissance de l’apprentissage machine, idéalement appliqué à la preuve formelle
• Bonne connaissance des systèmes de build de OCaml et Rocq
• Maîtrise de la gestion de gros corpus de données

• Anglais : B2 (Cadre européen de référence)
• Capacité de conceptualisation
• Sens critique
• Sens de l'organisation
• Aptitude au travail en équipe

Contexte de travail

Travail au sein de l'unité mixte de recherche 8243 IRIF

Contraintes et risques

Pas de risque