Description du sujet de thèse

Computer verification of mathematical proofs furnishes a way for mathematicians to concieve, save and transmit complex mathematical theory developments while keeping the required high level of rigour. Nevertheless, the use of these technologies is slowed by the difficulty of furnishing the large set of details needed to obtain a fully formalised proof. Several approaches have been proposed and are under active consideration.

The framework defined by the Malinca project consists, starting with a text written in natural language and containing textual reasoning in a classical way, to annotate and organize the information in successively more precise layers, to arrive at a level ready for translation into a formal proof. In this process, there are many questions that need to be resolved, for example filling into a proof the small steps that are considered as easy by the author, looking for intermediate statements that will be useful for a longer proof, or searching for the relevant definitions and lemmas in a database.

The question for the thesis will be to work on computational search for structures, strategies and information in the context of a mathematical development, in order to improve the automatisation of the process of creating formal proofs for a given mathematical topic.

Co-directed by David Alfaya (Comillas, Madrid) and co-supervised by Hugo Herbelin (INRIA, Paris).

Contexte de travail

The Malinca project (ERC Synergy, http://malinca.org), with centers in Paris, Nancy, Nice and Madrid, aims to develop a new generation of proof assistant technology capable of understanding the dynamical linguistic structures found in current high-level mathematical texts. The project includes the study of interpretation mechanisms for logical foundations, a new linguistic layer representing the intermediate steps between natural language texts and formal proof documents, and the automatisation tools for the efficient construction of definitions, theorems and proofs.

We would like to apply this to make the use of computer formalisation practical and current for mathematical research writing.

The co-direction and co-supervision of this thesis are placed in the context of the association of other centers within the project, the Comillas Pontifical University in Madrid and INRIA in Paris.

Contraintes et risques

-Registration and pursuit of the thesis within the SFA doctoral school ( https://adum.fr/script/formations.pl?site=sfa ).
-Each month the student will need to declare on timesheets a 100% implication in the ERC project.