18 nov. 2010
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 interface 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.
Georges Gonthier (Microsoft Research)
Vidéo de la conférence indisponible
Vidéo des questions :
