Thèse Interopérabilité pour les Mathématiques Synthétiques dans un Assistant à la Preuve H/F - Doctorat.Gouv.Fr

Établissement : Université Paris-Saclay GS Informatique et sciences du numérique École doctorale : Sciences et Technologies de l'Information et de la Communication Laboratoire de recherche : Laboratoire Méthodes Formelles Direction de la thèse : Théo WINTERHALTER ORCID 0000000298813696 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-07-31T23:59:59 Ce projet de doctorat vise à améliorer les fondements théoriques et les capacités de l'assistant à la preuve Rocq (anciennement Coq) afin de faciliter l'interopérabilité entre différents développements mathématiques formalisés. Plus précisément, il s'intéresse aux mathématiques synthétiques, une approche qui consiste à raisonner à partir d'axiomes abstraits plutôt qu'à partir de constructions explicites.Les assistants à la preuve sont devenus des outils majeurs pour la vérification formelle de démonstrations mathématiques et de systèmes logiciels critiques. Ils ont notamment permis la vérification complète de résultats mathématiques célèbres tels que la conjecture de Kepler ou le théorème des quatre couleurs, ainsi que de logiciels industriels comme le compilateur CompCert ou des bibliothèques cryptographiques utilisées en production.Cependant, certains domaines des mathématiques et de l'informatique théorique reposent sur une grande quantité de « mathématiques invisibles » : de nombreuses étapes considérées comme évidentes sur papier doivent être explicitées en détail dans un assistant de preuve. Les approches synthétiques permettent de masquer cette complexité en introduisant des axiomes décrivant directement les propriétés recherchées, par exemple en théorie de l'homotopie, en géométrie algébrique ou en théorie de la calculabilité.Cette simplification soulève néanmoins un problème majeur : comment faire communiquer plusieurs théories synthétiques entre elles, ou relier une théorie synthétique à une formalisation plus classique ? Les axiomes employés dans différents développements peuvent être incompatibles, et les théorèmes de correction reliant les deux points de vue ne sont généralement pas disponibles directement dans l'assistant à la preuve.L'objectif principal de la thèse est de développer des mécanismes permettant de traduire automatiquement des développements synthétiques vers des développements non synthétiques tout en garantissant leur correction formelle. Cette approche repose sur une extension des fondements de la théorie des types afin d'autoriser localement certaines hypothèses supplémentaires, notamment des univers de types locaux et des égalités définitionnelles locales.Le travail débutera par plusieurs études de cas. La première concerne les types paramétriques, dont l'interprétation sera donnée par la traduction de paramétricité. La seconde portera sur la théorie des types exceptionnels, utilisant des règles de réécriture locales. Ces exemples serviront à identifier des mécanismes généraux de traduction entre cadres synthétiques et non synthétiques.Une fois ces mécanismes formalisés, ils seront démontrés corrects dans une théorie des types idéale puis intégrés dans Rocq. Le projet étudiera ensuite la transformation d'égalités définitionnelles locales en égalités propositionnelles, avec comme cas d'étude une théorie synthétique des groupes où les axiomes de groupe sont traités de manière calculatoire.À terme, cette recherche vise à fournir aux utilisateurs d'assistants à la preuve un moyen robuste de combiner des bibliothèques développées selon des approches différentes, tout en conservant les garanties de correction offertes par la vérification formelle. Elle contribuera ainsi à rendre les mathématiques synthétiques plus modulaires, réutilisables et intégrées à l'écosystème des preuves formelles modernes. Proof assistant and type theory, formalised in a proof assistant. Bridge synthetic and analytic mathematics within proof assistants.

Formation en logique et programmation fonctionnelle. Expérience avec un assistant à la preuve, avec la preuve formelle et les mathématiques synthétiques.Bon niveau en anglais pour participer à des événements internationaux et rédiger des articles en anglais.