Mission : 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