"Le génie mathématique, du théorème de quatre couleurs à la classification des groupes" est le thème au menu du prochain Colloquium Jacques Morgenstern de l'INRIA Sophia Antipolis – Méditerranée, colloque qui aura lieu jeudi 18 novembre, 11 heures, à l'Amphithéâtre Morgenstern et qui sera animé par Georges Gonthier (Microsoft Research). Accès libre et gratuit
En résumé. Voilà plus de trente ans que l’informatique et les ordinateurs ont fait irruption dans les mathématiques, avec la célèbre preuve du théorème des quatre couleurs par Appel et Haken. Leur rôle s’est amplifié récemment, car ils permettent maintenant de maîtriser non plus seulement des calculs, mais aussi des raisonnements dont la complexité dépasse les capacités de l’esprit humain (ou du moins, de la plupart), comme la preuve de la conjecture de Kepler ou la classification des groupes simples finis.
Cependant, ces preuves "machine" exigent un changement profond de la pratique des mathématiques : un passage de l’artisanat, où chaque argument est un tribut à l’ingéniosité du mathématicien qui l’a ciselé, à une forme d’ingénierie, où les preuves sont construites à l’aide de techniques plus systématiques. On substitue ainsi des interfaces rigoureuses aux conventions d’usage malléables, et des algorithmes précis à l’apprentissage de méthodes par des exercices. Parvenir à codifier ainsi une part de l’état de l’art mathématique assez importante pour permettre de coder des preuves intéressantes, représente un défi considérable ; nous montrerons comment nous avons commencé à le relever.
+d'infos |
Inria Sophia : le génie mathématique à l'heure de l'informatique
Jean-Pierre Largillet2 min de lecture