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 la 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. 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 noter équipe dans ce domaine ont consisté à comparer une méthode due à Lebesgue et que nous avons améliorer et une méthode due à Chou et Gao. Un challenge est de tirer parti de cette étude pour avoir une méthode praticable pour des équations de degré 8.

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.

• équivalence entre la géométrie 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.

ce dernier à permis de prouver formellement divers théorème phares de la géométrie d'incidence, notamment en dimension 3, et notamment, le théorème de Dandelin-Gallucci.