Preuves en Géométrie
Permanents – 1,5 ETPR : Pascal Schreck (PR émérite), Gabriel Braun (MC), Nicolas Magaud (MC HDR), Julien Narboux (MC)
Objectifs. Les objectifs de ce thème 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++.
Au cours des dernières années, le thème "Preuves en géométrie" a développé des bibliothèques de référence en Coq autour des fondements de la géométrie et de l’automatisation du raisonnement géométrique. L’intérêt de la communauté pour ces travaux a été démontré par plusieurs portages de nos formalisations vers d’autres assistants de preuve, de manière manuelle ou automatique. A l’avenir le thème "Preuves en géométrie" souhaite travailler dans deux directions.
– La première consiste à rendre accessible nos travaux pour d’autres assistants de preuve, comme Isabelle ou Lean, en travaillant sur l’interopérabilité entre les assistants de preuves. Pour cela nous pourrons nous appuyer sur nos travaux concernant la démonstration automatique et nos premières expériences concernant l’utilisation du machine learning pour la formalisation automatique.
– La seconde consiste à travailler en direction des applications de nos formalisations de la géométrie, pour l’enseignement de la démonstration d’une part et pour la certification des systèmes cyber-physiques d’autre part (robot, voitures autonomes).
Dans ces deux domaines d'applications, la géométrie est une composante cruciale. Un des défis clés sera d’étudier comment adapter des algorithmes 2D pour passer à la 3D et aux dimensions supérieures tout en adaptant simultanément les preuves de correction.