Description du sujet de thèse

La vérification informatique des preuves mathématiques fournit un moyen pour les mathématiciens de concevoir, sauvegarder et transmettre des développements de théories mathématiques complexes tout en gardant un niveau exigeant de rigueur. Cependant, l'utilisation de ces technologies est freinée par la difficulté de fournir l'ensemble important de détails nécessaires à une preuve entièrement formalisée. Multiples approches ont été proposées et sont sous considération.

Le cadre défini par le projet Malinca consiste, à partir d'un texte rédigé en langue naturelle, comportant des raisonnements textuels à la manière classique, d'annoter et d'organiser ces informations avec des couches successives de précisions, avant d'arriver à un niveau apte à être traduit en preuve formelles. Dans ce processus, il y a des nombreux problèmes de quête de solutions, par exemple le remplissage dans une preuve des petites étapes considérées comme évidentes par l'auteur, la recherche d'énoncés intermédiaires utiles dans une preuve plus longue, ou la recherche des définitions et de lemmes pertinents dans une base de données.

Le question pour la thèse sera de travailler sur la recherche computationelle de structures, de stratégies et d'informations dans le contexte d'un développement mathématique, afin d'améliorer le processus d'automatisation de la création de preuves formelles pour une question mathématique donnée.

Co-dirigée par David Alfaya (Comillas, Madrid) et co-encadrée par Hugo Herbelin (INRIA, Paris)

Contexte de travail

Le projet Malinca (ERC Synergy, http://malinca.org), avec des centres à Paris, Nancy, Nice et Madrid, vise le développement d'une nouvelle génération de technologies d'assistants à la preuve capable de comprendre les structures linguistiques dynamiques trouvées dans les textes mathématiques actuels de haut niveau. Le projet inclut l'étude des mécanismes d'interprétation pour les fondements logiques, une nouvelle couche linguistique représentant les pas intermédiaires entre les textes en langue naturelle et les documents de preuves formalisées, et les outils d'automatisation pour la construction efficace de définitions, théorèmes et preuves. En application nous souhaitons rendre pratique et courant l'utilisation de la formalisation informatique pour les écrits de recherche mathématique.
La co-direction et le co-encadrement de la thèse se placent dans le contexte de l'association d'autres centres à ce projet, l'Université Pontificale de Comillas à Madrid et l'INRIA à Paris.

Contraintes et risques

-Inscription et poursuite de la thèse au sein de l'école doctorale SFA ( https://adum.fr/script/formations.pl?site=sfa )
-Il faudra faire chaque mois la déclaration sur feuilles de temps d'une implication à 100% dans le projet ERC.