Inria Sophia : le génie mathématique à l'heure de l'informatique
"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 linformatique 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 sest 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 lesprit 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 lartisanat, où chaque argument est un tribut à lingéniosité du mathématicien qui la ciselé, à une forme dingénierie, où les preuves sont construites à laide de techniques plus systématiques. On substitue ainsi des interfaces rigoureuses aux conventions dusage malléables, et des algorithmes précis à lapprentissage de méthodes par des exercices. Parvenir à codifier ainsi une part de létat de lart 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 |