Est-il possible de colorier n’importe quelle carte géographique avec 4 couleurs seulement ? La réponse (positive) à cette question a été conjecturée en 1852 par Morgan (l’homme des quaternions) et F. Guthrie. Après un siècle de tentatives (dont une preuve erronée, de Kempe en 1890, qui a été pensée correcte 11 ans !), ce théorème a été « prouvé » par Appel et Haken en 1976. Néanmoins, cette preuve posait un problème de statut, puisqu’elle reposait sur l’étude d’un nombre important de cas particuliers, qu’un ordinateur était seul capable d’étudier en temps plausible. Il faut en effet savoir que le programme initial contenait bon nombre d’erreurs, patiemment recensées au fil des années…
En 1995, Robertson, Sanders, Seymour, et Thomas ont réécrit la « preuve » d’Appel et Hanken en langage C ( la preuve initiale était écrite en assembleur pour IBM 370…). Ce travail a rendu la validité du théorème plus plausible.
Un pas important vient d’être franchi par deux chercheurs, Georges Gonthier (Microsoft) et Benjamin Werner (Inria) qui ont mis au point un programme de vérification formelle de la « preuve » de 1995, fondée sur un outil dédié à ce genre de travail (le « Coq Proof System »). Ce système a vérifié qu’aucun cas n’échappait à la sagacité des programmeurs, et que chaque vérification était correcte. Aussi, leur travail conforte-t-il le statut probant du travail d’Appel et Haken.
Reste que ce type de preuve est quand même plutôt frustrant, et qu’une preuve humainement lisible est toujours recherchée, si tant est qu’elle existe !
Une conférence sur l’historique de ce théorème aura lieu le mercredi 25 mai à 15 heures à l’Institut Henri Poincaré, 11 rue Pierre et Marie Curie, 75005 Paris (salle 201 /2°étage). Le conférencier en sera Olivier Hudry, de l’Ecole Nationale Supérieure des Télécommunications ; l’intitulé en est «Histoire et épistémologie du problème des quatre couleurs».
Voilà a publié une dépêche de vulgarisation
http://actu.voila.fr/Depeche/ext–francais–ftmms–informatique/050426153836.6crkxzs0.html
La page personnelle de G. Gonthier permet le téléchargement d’un texte expliquant la méthode employée.
http://research.microsoft.com/~gonthier/
L’IUFM de Poitou-Charente a mis en ligne un passionnant ensemble de pages de théorie des graphes dont tout un chapitre relatif au théorème des 4 couleurs, et à son historique.
A noter aussi sur ce site (bien que cela n’ait rien à voir), tout un cours de probabilités et statistiques d’accompagnement de l’enseignement de ces notions au lycée.
http://www.univ-lr.fr/formations/idea/duCultureMath/graphes/index.htm
http://www.univ-lr.fr/formations/idea/duCultureMath/graphes/chapitre04/cours/chapitre04_1.htm
http://www.univ-lr.fr/formations/idea/duCultureMath/statistiques/index.htm
– A la Une : Des progrès dans la preuve du théorème des 4 couleurs
