| Gilles Dowek | Directeur de recherche, INRIA Paris-Saclay | Rapporteur |
| Jacques Fleuriot | Professeur, Université d'Edimbourg | Rapporteur |
| Dominique Michelucci | Professeur, Université de Bourgogne | Rapporteur |
| Cédric Bastoul | Professeur, Université de Strasbourg, directeur scientifique chez Huawei France | Examinateur |
| Catherine Dubois | Professeur, ENSIIE Evry | Examinateur |
| Pascal Schreck | Professeur, Université de Strasbourg | Garant d'habilitation |
L’utilisation des assistants de preuve comme Coq prend de plus en plus d’ampleur. De tels outils permettent de démontrer formellement aussi bien des résultats mathématiques que des propriétés de correction d’algorithmes et de programmes informatiques. La géométrie est un domaine d’application riche et bien adapté pour mettre à l’épreuve ces systèmes d’aide à la preuve. Dans nos travaux, nous nous intéressons à trois domaines spécifiques de la géométrie : la formalisation d’algorithmes géométriques, l’automatisation au moins partielle des démonstrations dans le cadre de la géométrie projective et enfin la modélisation des nombres réels dans un formalisme bien adapté à la géométrie discrète.
Nos premiers travaux en géométrie ont permis de démontrer dans Coq la correction de deux variantes de l’algorithme incrémental de calcul de l’enveloppe convexe d’un ensemble de points du plan en utilisant une approche topologique avec les cartes combinatoires. Ces travaux ont mis en évidence le besoin de disposer d’outils pour automatiser au moins partiellement les démonstrations en géométrie. Nous avons alors étudié cette question dans le cadre simple de la géométrie projective en utilisant une approche combinatoire et la notion de rang d’un ensemble de points. L’outil proposé permet de démontrer automatiquement de nombreux théorèmes emblématiques de la géométrie projective et de produire une trace sous la forme d’un script de preuve vérifiable par Coq. Enfin, faire des preuves en géométrie, qu’elles soient automatisées ou non, ne peut se faire sans disposer d’un modèle informatique des nombres réels. Nous avons formalisé dans Coq la droite d’Harthong-Reeb qui est un modèle du continu ainsi que son implantation informatique avec les entiers de Laugwitz-Schmieden. Ce modèle est bien adapté au contexte de la géométrie discrète et permet notamment de représenter facilement des objets continus de manière discrète en utilisant un schéma d’arithmétisation.
Nos travaux ont un double objectif. Il s’agit d’une part de confronter notre expertise en preuves formelles à des problèmes issus de nouveaux domaines et de démontrer que les outils dont nous disposons sont bien adaptés à la réalisation de preuves formelles, notamment en géométrie. D’autre part, de tels travaux permettent de mettre en évidence les points d’amélioration des outils existants et éventuellement d’en accroître la fiabilité, l’efficacité et la facilité d’utilisation.