Théorème des quatre couleurs

Coloriage en quatre couleurs de cinq pays d'Europe (autour du Luxembourg) avec leur structure de graphe.

Le théorème des quatre couleurs indique qu'il est possible, en n'utilisant que quatre couleurs différentes, de colorier 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 celle des sommets d'un graphe planaire, en remplaçant la carte par un graphe dont les sommets sont les régions et les arêtes sont les frontières entre régions.

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).

Même si l'énoncé de ce théorème est élémentaire, on n'en connaît pas de preuve simple. Les démonstrations connues décomposent le problème en un nombre de sous-cas tellement important qu'elles nécessitent l'assistance d'un ordinateur pour être vérifiées.

Le théorème se généralise à certaines classes de graphes non planaires. Cependant, lorsqu'on généralise le problème à un graphe quelconque, il devient NP-complet de déterminer s'il est coloriable avec seulement quatre couleurs (ou même trois).

Histoire

Le résultat fut conjecturé en 1840 par Ferdinand Möbius^[1], puis en 1852 par Francis Guthrie, intéressé par la coloration de la carte des régions d'Angleterre^[2]. La première mention publiée date toutefois de 1879^[3]. Deux premières démonstrations furent publiées, respectivement par Alfred Kempe en 1879 et Peter Guthrie Tait en 1880. Mais elles se révélèrent erronées ; les erreurs ont été relevées seulement en 1890 par Percy Heawood et en 1891 par Julius Petersen.

Si la preuve de Kempe s'est révélée fausse, elle fournit cependant une démonstration d'un problème analogue, avec cinq couleurs au lieu de quatre, aujourd'hui connu sous le nom du théorème des cinq couleurs^[4].

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^[5]. Leur démonstration divise la communauté scientifique : pour la première fois, en effet, la démonstration exige l'usage de l'ordinateur pour étudier les 1 478 cas critiques (plus de 1 200 heures de calcul). Le problème de la démonstration 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 (en), Seymour et Thomas^[6]. D'autres programmes informatiques, écrits de façon indépendante du premier, aboutissent au même résultat. Il existe ainsi depuis 2005 une version entièrement formalisée^[7], 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. La preuve de Gonthier introduit de nouveaux formalismes (les hypermaps) qui permettent de réduire la quantité de cas à considérer.

Paul Erdős suggère^{[réf. souhaitée]} que le théorème des quatre couleurs est « 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, devrait exister. Mais pour cela, il conviendrait peut-être de « compliquer le problème », en le formulant pour un ensemble de points plus vaste qu'un graphe planaire, et incluant celui-ci.

En 2020, aucune preuve qui puisse se passer de l'ordinateur n'a été découverte ; cependant, de nombreux amateurs continuent à être convaincus avoir démontré sans ordinateur le théorème des quatre couleurs , et Underwood Dudley consacre un chapitre de Mathematical Cranks à ces tentatives.

Généralisations du théorème des quatre couleurs

Classes de graphes plus générales que les graphes planaires

On voit que l'énoncé classique du théorème des quatre couleurs n'est bien sûr pas une caractérisation des graphes dont le nombre chromatique est inférieur ou égal à quatre puisque le graphe ${\displaystyle K_{3,3}}$ n'est pas planaire mais est biparti. D'autre part, pour des raisons de complexité algorithmique, il ne peut exister de caractérisation simple des graphes k-colorables pour k fixé supérieur ou égal à trois. Le théorème des quatre couleurs se généralise aux graphes sans mineur ${\displaystyle K_{5}}$, puisque le nombre chromatique de ces graphes vaut au plus quatre (et c'est une des motivations de la conjecture de Hadwiger). Une généralisation plus forte encore a été donnée récemment par Guenin :

• les graphes sans mineur impair ${\displaystyle K_{5}}$ sont colorables avec seulement quatre couleurs.

(Un mineur est dit impair si les opérations de contractions des arêtes s'effectuent uniquement sur une coupe du graphe. Un graphe contient un mineur impair ${\displaystyle K_{5}}$ s'il contient un ${\displaystyle K_{5}}$ dont on a remplacé les dix arêtes par dix chemins de longueur impaire.)

Ces résultats plus forts sont basés sur des preuves utilisant le théorème des quatre couleurs lui-même, par conséquent ils n'en apportent pas de nouvelle démonstration.

Surfaces plus générales que le plan

En collant les bords marqués de flèches doubles pour former un cylindre, puis les bords marqués de flèches simples, on obtient un tore avec sept régions se touchant six à six ; ainsi, sept couleurs sont nécessaires

Résultat du collage précédent.

On peut aussi considérer le problème du coloriage de cartes tracées sur des surfaces autres que le plan. Sur la sphère, le problème est le même (pour le voir, il suffit de retirer un point de la sphère intérieur à l'une des régions, et d'effectuer une projection stéréographique).

En 1890, Heawood démontra que pour une surface « fermée » (c'est-à-dire compacte, connexe et sans bord) non homéomorphe à la sphère, le nombre de couleurs nécessaires est toujours majoré, en fonction de la caractéristique d'Euler χ de la surface, par

${\displaystyle p:=\left\lfloor {\frac {7+{\sqrt {49-24\chi }}}{2}}\right\rfloor }$

(où les crochets extérieurs désignent la fonction partie entière) et conjectura que ce majorant était optimal.

(Le théorème des quatre couleurs est l'extension à la sphère de sa majoration, puisqu'alors, χ = 2 donc p = 4.)

Par exemple, le tore a une caractéristique d'Euler χ = 0 donc p = 7 ; 7 couleurs suffisent donc pour colorier n'importe quelle carte sur le tore, et l'exemple de la figure montre que cela peut être nécessaire.

En 1934, Philip Franklin réfuta la conjecture de Heawood en montrant que pour la bouteille de Klein, 6 couleurs suffisent toujours, alors que, comme pour le tore, χ = 0 donc p = 7 (il exhiba de plus une carte pour laquelle 6 couleurs sont nécessaires). Mais en 1968, Ringel et John William Theodore Youngs montrèrent que la conjecture est vraie pour toute autre surface fermée, c'est-à-dire qu'il existe une carte tracée sur cette surface pour laquelle p couleurs sont nécessaires.

Il n'y a pas de généralisation dans l'espace car n boudins assez longs peuvent toujours être disposés de telle façon que chacun touche tous les autres — ce qui rend supérieur à n le nombre de couleurs nécessaires — et n peut être choisi aussi grand qu'on veut.

Conséquences

Algorithmiques

Coloriage des États des États-Unis en quatre couleurs.

Déterminer si un graphe peut être ou non coloré en deux couleurs est très facile : techniquement, il suffit de colorier arbitrairement un sommet de chaque composante connexe avec une couleur et ensuite de propager cette décision en colorant les sommets voisins avec l'autre couleur, et ainsi de suite. Si l'on rencontre un sommet encore non coloré et voisin de deux sommets de couleur différente, alors le graphe ne peut être biparti. C'est un problème soluble en temps polynomial.

En revanche, déterminer si un graphe peut être ou non coloré en k couleurs pour k > 2 est un problème NP-complet. La preuve de Appel et Haken donne un algorithme pour colorier tout graphe planaire avec quatre couleurs en temps quadratique (la 3-coloration des graphes planaires étant NP-complet).

Cas du coloriage de cartes

S'agissant du coloriage des cartes de géographie, le théorème a, en fait, un intérêt limité. Par exemple, si on souhaite colorier une carte géographique du monde en attribuant des couleurs différentes aux pays limitrophes :

• D'une part, on sera gêné par la présence de la mer. Soit il faut lui attribuer une couleur comme si c'était un pays — mais ce serait trompeur — soit il faut lui réserver une couleur supplémentaire.
• D'autre part, le théorème traite de régions connexes, or les pays ne sont pas forcément connexes, car leur territoire peut inclure des îles ou des exclaves.

Bibliographie

• Georges Gonthier (enseignant à Polytechnique), Le théorème des quatre couleurs (lire en ligne)
• George Gonthier A computer-checked proof of the Four Colour Theorem
• Howard Levi, « An algebraic reformulation of the four color theorem », publié à titre posthume par Don Coppersmith, Melvin Fitting et Paul Meyer.

Notes et références

1. (en) S. M. De Backer, « The Four-Colour Problem », Nature, vol. 153,‎ 10 juin 1944 (lire en ligne)
2. Kenneth Appel et Wolfgang Haken, Les progrès des mathématiques, éd. Belin, 1981, 8-19 p. (ISBN 2902918143), « La solution du problème des quatre couleurs ».
3. (en) Arthur Cayley, « On the colourings of maps », Proc. Royal Geographical Society, vol. 1, 1879, p. 259-261.
4. Gonthier 2000.
5. (en) Kenneth Appel et Wolfgang Haken, « Every planar map is four colorable, Part I: Discharging », Illinois J. Math., vol. 21,‎ 1977, p. 429-490 (lire en ligne).
6. On trouvera un rappel de l'historique du théorème et une version détaillée de leur algorithme (présentée sous forme d'un travail informatique guidé) dans Gonthier 2000.
7. (en) Georges Gonthier, « Formal Proof—The Four-Color Theorem », Notices of the AMS,‎ 2008, p. 12 (lire en ligne [PDF])

Liens externes

• (en) Eric W. Weisstein, « Heawood Conjecture », sur MathWorld
• (en) Eric W. Weisstein, « Map Coloring », sur MathWorld