Sites Inria

English version

Colloquium Jacques Morgenstern

Le génie mathématique, du théorème de quatre couleurs à la classification des groupes

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.

  • Date : 18/11/2010
  • Lieu : Inria Sophia Antipolis
  • Intervenant(s) : Georges Gonthier, Microsoft Research
  • Organisateur(s) : Inria - UNS - I3S - Polytech Nice Sophia

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.

lire la suite

Mots-clés : Mathématiques Théorème 4 couleurs Colloquium J. Morgenstern Inria Sophia Antipolis - Méditerranée

Haut de page

Suivez Inria