Doctorant (H/F) dans le projet Mathematicae Lingua Franca (Malinca)

CNRS; Provence-Alpes-Côte d'Azur; Sur place; EUR 40 000 - 60 000; Plein temps

Résumé du poste

Le CNRS recrute pour une thèse en mathématiques dans le projet Mathematicae Lingua Franca à Nice. Le doctorant doit développer des méthodes d'automatisation pour la création de preuves formelles à partir de raisonnements en langue naturelle, tout en travaillant dans un environnement collaboratif avec des institutions renommées.

Qualifications

• Recherche computationnelle de structures et stratégies dans un développement mathématique.
• Inscriptions et poursuite de la thèse dans l'école doctorale SFA requises.

Responsabilités

• Automatiser le processus de création de preuves formelles pour un domaine mathématique spécifique.
• Travailler sur l'annotation et l'organisation d'informations issues de textes mathématiques.

Formation

Doctorat en Mathématiques ou domaines connexes

Description du poste

Doctorant (H/F) dans le projet Mathematicae Lingua Franca (Malinca), Nice

Informations générales

Intitulé de l'offre : Doctorant (H/F) dans le projet Mathematicae Lingua Franca (Malinca)
Référence : UMR7351-CARSIM-003
Nombre de Postes : 1
Lieu de travail : NICE
Date de publication : mardi 10 juin 2025
Type de contrat : CDD Doctorant
Durée du contrat : 36 mois
Date de début de la thèse : 1 septembre 2025
Quotité de travail : Complet
Rémunération : La rémunération est d'un minimum de 2200,00 € mensuel
Section(s) CN : 41 - Mathématiques et interactions des mathématiques

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://, 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:///script/?site=sfa )
-Il faudra faire chaque mois la déclaration sur feuilles de temps d'une implication à 100% dans le projet ERC.