Théorème des quatre couleurs - Définition

Introduction

Carte administrative de la Russie colorée avec quatre couleurs

Le théorème des quatre couleurs indique qu'il est possible, en n'utilisant que quatre couleurs différentes, de colorer n'importe quelle carte découpée en régions connexes, de sorte que deux régions adjacentes (ou limitrophes), c'est-à-dire ayant toute une frontière (et non simplement un point) en commun reçoivent toujours deux couleurs distinctes. L'énoncé peut varier et concerner, de manière tout à fait équivalente, la coloration des faces d'un polyèdre, ou des sommets d'un graphe planaire.

Trivialement, chacune des régions doit recevoir une couleur différente si les régions sont deux à deux adjacentes ; c'est le cas par exemple de la Belgique, du Luxembourg, de l'Allemagne et de la France dans une carte politique de l'Europe.

D'où la nécessité des quatre couleurs dans le cas général. Par ailleurs, il ne peut exister cinq régions connexes deux à deux adjacentes (c'est la partie facile du théorème de Kuratowski).

Lorsqu'on généralise le problème à un graphe quelconque, il devient NP-complet de déterminer s'il est colorable avec seulement 4 couleurs (et même 3).

Histoire

Le résultat fut conjecturé en 1852 par Francis Guthrie, intéressé par la coloration de la carte des régions d'Angleterre. La première mention publiée date toutefois de 1879. Deux premières démonstrations furent publiées, respectivement par Alfred Kempe en 1879 et Peter Guthrie Tait en 1880. Mais elles s'avérèrent erronées ; les erreurs ont été relevées seulement en 1890 par Percy Heawood et en 1891 par Julius Petersen.

Ironiquement, la fausse preuve de Kempe contient le schéma général de la vraie preuve.
La fausse preuve fournit en fait une démonstration du résultat analogue mais avec cinq couleurs au lieu de quatre, aujourd'hui connu sous le nom du théorème des cinq couleurs (dont l'unique intérêt est d'admettre une courte preuve, donnée dans la référence), comme l'a remarqué Percy Heawood en 1890.

Dans les années 1960 et 1970, Heinrich Heesch s'intéresse à la possibilité de prouver informatiquement le théorème des quatre couleurs. Finalement, en 1976, deux Américains, Kenneth Appel et Wolfgang Haken, affirment avoir démontré le théorème des quatre couleurs. Leur démonstration partage la communauté scientifique : pour la première fois, en effet, la démonstration exige l'usage de l'ordinateur pour étudier les 1478 cas critiques (plus de 1200 heures de calcul). Le problème de la validation du théorème se trouve alors déplacé vers le problème de la validation :

• d'une part de l'algorithme d'exploration,
• d'autre part de sa réalisation sous forme de programme.

Depuis 1976, l'algorithme d'Appel et Haken a été repris et simplifié par Robertson, Sanders, Seymour et Thomas. D'autres programmes informatiques, écrits de façon indépendante du premier, aboutissent au même résultat. Il existe ainsi une version entièrement formalisée, formulée avec Coq par Georges Gonthier et Benjamin Werner, qui permet à un ordinateur de complètement vérifier le théorème des quatre couleurs.

Paul Erdös pensait que le théorème des quatre couleurs était « un problème subtil et non pas un problème complexe ». D'après lui, une démonstration simple, et même très simple, devait exister. Mais pour cela, il aurait fallu peut-être « compliquer le problème », en le formulant pour un ensemble de points plus vaste qu'un graphe planaire, et incluant celui-ci. En tout cas, aucune preuve qui ne fasse pas appel à l'ordinateur n'a été découverte jusqu'ici ; cependant, de nombreux amateurs continuent à être convaincus de l'avoir démontré, et Underwood Dudley consacre un chapitre de Mathematical Cranks à ces tentatives, dont un exemple typique, et moins absurde que beaucoup d'autres, est celle de George Spencer-Brown, déposée en 1980, mais qui n'a jamais été acceptée.