Description du sujet de thèse

Ce projet de thèse s’inscrit à l’interface entre les assistants de preuve et la didactique de l’enseignement supérieur.
La formalisation mathématique par assistants de preuve a principalement été développée à des fins de vérification formelle en recherche avancée. Cependant, elle offre également un cadre structurant qui explicite la logique et les mécanismes des démonstrations que la communauté a assez tôt essayé d'utiliser dans un cadre d'enseignement. De nombreux outils, construits de zéro dans une perspective didactique ou comme des surcouches des assistants de preuve pour l'enseignement ont été développés. Pendant longtemps, ces outils ont principalement été utilisés pour enseigner les fondements de l'informatique et la logique. Plus récemment, ces outils ont été utilisés dans des cours d'initiation à la démonstration (voir \cite{tran_minh_proof_2025} pour un état de l'art récent).

Dans ce contexte, le projet ambitionne de transposer ces outils dans un objectif pédagogique: il s’agit de fournir aux étudiants un environnement rigoureux, interactif et motivant pour les initier à la démonstration. Cette thèse se focalisera sur les mathématiques et l'informatique de premier cycle sans se limiter à l'initiation à la démonstration.

Le défi scientifique est de pouvoir adapter l'assistant de preuve pour qu'il accepte des démonstrations relativement naturelle. Dans ce contexte d'enseignement, on n'aura pas comme objectif de formaliser automatiquement toute démonstration écrite en langue naturelle mais l'objectif plus modeste d'avoir un langage restreint lisible et naturel dans lequel il est facile pour un étudiant d'exprimer les démonstrations attendues sans acquérir la syntaxe d'un assistant de preuve traditionnel.

L'objectif principal est d'obtenir une bibliothèque de preuves/exercices formalisés à l’aide d’un assistant de preuve (tel que Coq, ou Lean) couvrant une partie significative du programme de classes préparatoires et de début d'université en mathématiques et informatique.
Outre la formalisation d’un corpus ciblé du programme, un aspect essentiel du projet consistera à adapter les formalisations existantes aux besoins pédagogiques du public cible. Il s'agira en particulier de construire une formalisation et des outils permettant d'accepter les démonstrations attendues par les enseignants de manière similaire à des preuves traditionnelles en termes de granularité et de besoins de justifications. L'automatisation devra être ni trop faible ni trop forte, et adaptable au niveau des étudiants.

Contexte de travail

La thèse qui se situe dans le domaine de l'informatique bénéficiera du contexte scientifique favorable des projets ANR Appam (https://appam.icube.unistra.fr/), Inria Liberabaci (https://www.inria.fr/fr/liberabaci) et ERC Malinca (https://www.inria.fr/fr/bourse-erc-malinca-langue-mathematiques-assistants-preuve) qui permettront des interactions scientifiques avec des didacticiens des mathématiques, des enseignants de mathématiques, des linguistes, des développeurs des assistants de preuves et de leurs interfaces, et les théoriciens de la preuve.

Contraintes et risques

Pas de risques ni contraintes identifiés.