Spécifications, Contraintes et Preuves en Géométrie Bilan2016-2021

Objectifs/Challenges

Les objectifs de ce thèmes relèvent de la formalisation de la géométrie en vue d'usages pratiques comme la résolution de contraintes géométriques, l'aide à la preuve en géométrie dans les domaines de l'enseignement ou de la robotique ou encore la certification d'algorithmes ayant trait à la géométrie. C'est une thématique difficile où se côtoient des aspects théoriques comme le calcul algébrique formel, la théorie du calcul des constructions ou encore l'axiomatisation de la géométrie et des aspects plus pratique comme l'ingénierie de la preuve en Coq ou le guidage de méthodes numériques développées en C++.

Participants

Un professeur : Pascal Schreck
Quatre maîtres de conférences : Gabriel Braun, Nicolas Magaud (HDR), Pascal Mathis (HDR) (jusqu'au 31/08/2017), Julien Narboux
Deux doctorants : David Braun (Allocataire UNISTRA du 10/2015 au 09/2018) et Pierre Boutry (Allocataire UNISTRA du 10/2013 au 09/2016)

Résultats

Mécanisation des constructions à la règle et au compas

Cette problématique a été, dans l'équipe, essentiellement étudiée par P. Schreck et P. Mathis. Certaines résultats ont été obtenus et publiés avec Predrag Janicic et Vesna Marinkovic de l'Université de Belgrade (Serbie).

Le résultat le plus marquant réside dans la preuve algébrique en Maple des statuts de constructibilité à la règle et au compas de deux listes de problèmes de construction connues des mathématiciens américains sous le nom de liste de Wernick et liste de Connelly. Ces listes regroupent environ 270 problèmes de construction à la règle et au compas à partir de points caractéristiques, elles ont été créées de manière systématique à titre d'amusement et de challenge pour les professeurs de mathématique, principalement de lycée, et ont reçu des réponses partielles de divers mathématiciens dans le monde. L'originalité de notre travail est principalement d'avoir développer une méthode pour traiter automatiquement les deux listes et délivrer le statut, en gros constructible ou non constructible à la règle et au compas, de chaque problème. Nous avons à cette occasion mis en oeuvre ce qui fait la singularité de notre approche : nous avons mélangé du raisonnement géométrique formel, implanté sous forme d'un programme Prolog, pour guider la mise en forme et la triangularisation de systèmes algébriques sous forme de chaînes régulières, ces dernières étant traitées par Maple pour obtenir les groupes de Galois correspondant, tout cela a été implanté par un programme Maple [2-SM19].

Il convient de noter qu'il s'agit ici de tester la constructibilité et non d'exhiber, éventuellement, une construction. Les dernier résultats de notre équipe dans ce domaine résident dans une comparaison d'une méthode due à Lebesgue, et que nous avons améliorée, et une méthode due à Chou et Gao [2-Schr19]. Un challenge est de tirer parti de cette étude pour avoir une méthode praticable pour des équations de degré 8.

Fondements de la géométrie

Reprenant un travail de J. Narboux puis G. Braun, P. Boutry a consacré une grande partie de sa thèse à la formalisation en Coq du livre de Tarski sur les fondements de la géométrie. Un des tours de force de la thèse de P. Boutry a été une étude très minutieuse de plus d'une vingtaine de propositions équivalentes sous certaines conditions à l'axiome des parallèles. En examinant de très près ces conditions d'équivalence, P. Boutry a établi un graphe de dépendances (du plus fort au plus faible) de ces axiomes. L'utilisation de Coq a été ici primordiale, car les occasions de se tromper en supposant une soit disant évidence, étaient nombreuses [2-BGNS17].

Aide à la preuve en géométrie d'incidence

Ce point recouvre principalement le travail de thèse de David Braun doctorant co-encadré par N. Magaud et P. Schreck. L'objectif, très ambitieux, de cette thèse était d'identifier des pistes permettant d'aider à faire des preuves avec la géométrie comme terrain d'expérimentation. Il n'est en effet pas facile de faire des preuves en géométrie notamment à cause de la double nature de la "figure" qui sert souvent de support à la preuve : d'une part, cette figure est nécessaire, au moins pour certains mathématiciens, pour avoir l'intuition de la preuve en permettant de repérer des motifs connus et d'autre part, cette figure est une instance, souvent fausse, particulière de la spécification, elle peut donc facilement induire en erreur et conduire à des "preuves" qui ne mènent nulle part. Parce que c'est un domaine que nous connaissons bien, nous avons choisi d'étudier la géométrie projective de ce point de vue car elle est facile à axiomatiser, elle cache une redoutable complexité et l'absence de notions comme les distances ou les angles requière une grande rigueur dans le raisonnement. Les principaux résultats obtenus ont été divers et se regroupent entre les points suivants (détaillés plus bas) :

équivalence entre l'approche synthétique et une structure combinatoire, les matroïdes, très générale,
étude de technique de preuve pour prendre en compte de grosses preuves combinatoire dans le cadre des géométries finies,
conception et implantation d'un prouveur automatique à base de matroïde.

1. Équivalence entre l'approche synthétique et l'approche combinatoire via les matroïdes.
Ce travail complète une étude déjà faite par l'équipe [2-MNS12] où un sens de l'équivalence avait été établi. L'autre sens de l'équivalence (des matroïdes vers la géométrie) nécessitait un développement conséquent où les techniques "orientées objets" de Coq ont été mise en oeuvre pour bien découpler les différentes notions et différencier, notamment, les dimensions 2, 3 et au-delà de trois, i.e sans axiomes indiquant une borne supérieure pour la dimension. Ce travail a donné lieu à une publication dans une revue référencée du domaine [2-BMS19], et il a été utilisé pour justifier les travaux ultérieurs utilisant intensivement cette approche par matroïdes.

2. Géométries d'incidence finies
Cette étude de quelques structures d'incidence projectives a été l'occasion de stress test pour Coq et pour le programmeur en Coq. En effet, ces structures impliquent une explosion combinatoire au point qu'il y a de nombreuses questions ouvertes à ce sujet, comme, par exemple, l'existence d'un plan d'incidence d'ordre 12, i.e. avec 13 points par droite si on considère le cas projectif. Cela a été l'occasion de mettre au point des stratégies de développement pour arriver à ce que Coq gère les preuves sans dépassement mémoire et dans un temps raisonnable. C'est aussi au cours de cette étude qu'une comparaison entre l'approche synthétique et l'approche à base de matroïde en termes de complexité a été menée. Suivant les cas, une approche est meilleure que l'autre et inversement [4-BMS18]. Cependant, un des grands avantages de l'approche à base de matroïdes réside dans sa faculté à être automatisée et à traiter les problèmes de manière homogène au regard de la dimension de l'espace projectif.

3. Un prouveur automatique à base de matroïdes
Ce prouveur est très spécialisé et consiste à remplir une structure matroïdale représentée par une fonction rang à partir des données de l'énoncé. Il nécessite donc d'avoir éliminé tous les quantificateurs existentiels. Tout limité qu'il semble, il a permis de prouver formellement et avec un grand degré d'automatisation, divers théorèmes phares de la géométrie d'incidence en dimension 2 et 3 et notamment, le théorème de Dandelin-Gallucci [8-Brau19].