Description du sujet de thèse

This PhD project lies at the intersection of proof assistants and higher education pedagogy. Mathematical formalization using proof assistants was initially developed for the purpose of formal verification in advanced research. However, it also provides a structured framework that makes explicit the logic and mechanisms of proofs, which the academic community began exploring early on for educational use. Many tools have since been developed, either from scratch with a pedagogical perspective or as educational layers built on top of existing proof assistants.

For a long time, these tools were primarily used to teach the fundamentals of computer science and logic. More recently, they have been introduced in introductory courses on mathematical proof (see \cite{tran_minh_proof_2025} for a recent state-of-the-art review). In this context, the project aims to repurpose these tools with an educational objective: providing students with a rigorous, interactive, and engaging environment to learn how to construct proofs.

This PhD will focus on undergraduate-level mathematics and computer science, without being limited to introductory proof courses. The scientific challenge is to adapt proof assistants so they can accept relatively natural proofs. In an educational context, the goal is not to automatically formalize any proof written in natural language, but rather to develop a restricted, readable, and natural language in which students can easily express the expected proofs—without needing to master the full syntax of a traditional proof assistant.

The main goal is to build a library of formalized proofs and exercises using a proof assistant (such as Coq or Lean), covering a significant portion of the curriculum in French preparatory classes and early university-level mathematics and computer science. In addition to formalizing a targeted curriculum corpus, a key aspect of the project will be adapting existing formalizations to the pedagogical needs of the intended audience. This includes building formalizations and tools that can accept student-submitted proofs similar in structure and granularity to traditional textbook proofs, as expected by instructors. Automation must be carefully calibrated—not too weak, not too strong—and adaptable to students' varying levels.

Contexte de travail

The PhD, which falls within the field of computer science, will benefit from the supportive scientific environment provided by the ANR Appam project (https://appam.icube.unistra.fr/), the Inria Liberabaci project (https://www.inria.fr/en/liberabaci), and the ERC Malinca project (https://www.inria.fr/en/erc-malinca-grant-mathematics-language-proof-assistants). These projects will foster scientific interactions with mathematics education researchers, mathematics teachers, linguists, proof assistant developers and interface designers, as well as proof theorists.

Contraintes et risques

No risks or constraints identified.