Théorème des quatre couleurs

Vitrail coloré avec quatre couleurs

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 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 coloriable avec seulement quatre couleurs (ou même trois).

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 [1]. 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  (en) [2].

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 [3]. 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 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 [4]. 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, 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 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 2015, aucune preuve qui ne fasse pas appel à l'ordinateur n'a été découverte ; cependant, de nombreux amateurs continuent à être convaincus de l'avoir démontré, et Underwood Dudley consacre un chapitre de Mathematical Cranks à ces tentatives.

Other Languages
azərbaycanca: Dörd boya problemi
日本語: 四色定理
한국어: 4색정리
norsk nynorsk: Firfargeproblemet
Simple English: Four color theorem
slovenščina: Izrek štirih barv
Tiếng Việt: Định lý bốn màu
中文: 四色定理