Mathématiques et preuves formelles par Assia Mahboubi
Assia Mahboubi
INRIA
Laboratory of Digital Sciences of Nantes
Vrije Universiteit Amsterdam, Pays-Bas
" Mathématiques et preuves formelles "
La logique mathématique étudie les preuves comme des objets mathématiques : existence, forme, classification, etc. Ces preuves formelles semblent néanmoins bien éloignées des démonstrations, aussi rigoureuse soient-elles, qui constituent la littérature mathématique contemporaine. Les preuves formelles sont par contre des structures de données manipulables par des programmes informatiques, qui permettent de les construire, de les observer, de les vérifier par des procédés mécaniques. Les assistants de preuves sont des logiciels qui permettent d'effectuer ces opérations, en pratique et à grande échelle. Dans cet exposé, on s'efforcera de donner un aperçu illustré des mathématiques que l'on peut faire avec un assistant de preuve, et des bénéfices de cette activité.
Assia Mahboubi a soutenu en 2006 une thèse d'informatique portant sur la vérification formelle d'algorithmes en géométrie algébrique réelle, à l'université de Nice Sophia Antipolis, après un travail effectué à l'Inria Sophia Antipolis sous la supervision de Loïc Pottier. Elle a ensuite participé au projet de preuve formelle pour le théorème de l'ordre impair (théorème de Feit-Thompson), dans l'équipe menée par Georges Gonthier au sein du laboratoire commun Microsoft Research-Inria. Elle a été recrutée comme chargée de recherche à l'Inria en 2007, d'abord à Saclay puis à Nantes, et elle est maintenant directrice de recherche.
Assia Mahboubi étudie la formalisation des mathématiques et les interactions de la preuve formelle avec le domaine voisin du calcul formel. Elle est une autorité de référence sur la formalisation des mathématiques, en particulier avec la bibliothèque " Mathematical Components " pour le système Coq, développée initialement à l'occasion de la vérification du théorème de Feit-Thompson. Elle a co-écrit avec Enrico Tassi un livre décrivant cette bibliothèque [5] et avec de nombreux co-auteurs des articles sur l'organisation générale des formalisations de mathématiques, sur la formalisation de preuves remarquables comme le théorème de Feit-Thompson [2], la preuve d'Apéry sur l'irrationalité de \(\zeta(3)\) [4], ou le théorème d'Abel-Ruffini, [1] et sur des algorithmes pour l'automatisation de preuves concernant des égalités de formules, des procédures de décision en géométrie algébrique réelle, ou des approximations correctes en calcul intégro-différentiel [3].
Elle est membre du bureau éditorial pour " Journal of Automated Reasoning ", titulaire d'une chaire invitée à l'université libre d'Amsterdam, et d'une bourse ERC consolidateur.
[1] Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub. Un- solvability of the Quintic Formalized in Dependent Type Theory. In ITP 2021 - 12th International Conference on Interactive Theorem Proving, Rome / Virtual, France, June 2021.
[2] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A Machine-Checked Proof of the Odd Order Theorem. In Sandrine Blazy, Christine Paulin, and David Pichardie, editors, ITP 2013, 4th Conference on Interactive Theorem Proving, volume 7998 of LNCS, pages 163–179, Rennes, France, July 2013. Springer.
[3] Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. For- mally Verified Approximations of Definite Integrals. Journal of Automated Reasoning, 62(2):281–300, February 2019. 1
[4] Assia Mahboubi and Thomas Sibut-Pinote. A formal proof of the irrational- ity of ζ(3). Logical Methods in Computer Science, 17(1):1–25, February 2021.
[5] Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, January 2021.
En savoir plus sur le colloque
