Le problème est très simple à énoncer : combien de couleurs sont nécessaires au minimum pour colorier n’importe quelle carte géographique (sur un plan ou une sphère) de telle sorte que deux pays partageant une frontière commune aient des couleurs différentes ?
- Les pays doivent partager une frontière (un segment), pas seulement un point.
- En théorie des graphes, ce problème se traduit par le coloriage des sommets d’un graphe planaire (un graphe que l’on peut dessiner sur un plan sans que les arêtes ne se croisent).
Il est facile de voir que trois couleurs ne suffisent pas (imaginez un pays central entouré par trois autres pays qui se touchent deux à deux). La question était donc : « Est-ce que quatre couleurs suffisent toujours ? ».
Toute carte dessinée sur un plan ou une sphère peut être coloriée avec quatre couleurs au maximum, de manière à ce que deux régions adjacentes reçoivent des couleurs différentes.
Une Histoire et une Démonstration Uniques
Ce théorème est célèbre non seulement pour son énoncé simple, mais aussi pour l’histoire de sa démonstration.
- Une longue conjecture : Le problème a été posé pour la première fois en 1852 par Francis Guthrie. Il est resté une conjecture non résolue pendant plus d’un siècle, résistant aux tentatives de nombreux mathématiciens.
-
La preuve par ordinateur : En 1976, les mathématiciens Kenneth Appel et Wolfgang Haken ont finalement prouvé le théorème. Leur approche était révolutionnaire :
- Ils ont d’abord prouvé que toute carte possible devait contenir l’un des 1 936 « ensembles inévitables » (un nombre réduit plus tard).
- Ils ont ensuite montré que chacun de ces cas était « réductible », c’est-à-dire qu’il pouvait être coloré avec quatre couleurs.
- Controverse : La vérification de ces milliers de cas était humainement impossible. Appel et Haken ont utilisé un ordinateur pour effectuer les vérifications, ce qui a nécessité plus de 1 200 heures de calcul. C’était le premier grand théorème à être prouvé avec une aide aussi massive de l’informatique, ce qui a déclenché un débat philosophique sur la nature d’une preuve : peut-on faire confiance à une preuve qu’aucun humain ne peut vérifier entièrement à la main ?
Depuis, la preuve a été simplifiée, vérifiée par d’autres programmes et est aujourd’hui universellement acceptée.