Sciences · Mathématiques
Le théorème des quatre couleurs
Le théorème des quatre couleurs affirme que toute carte plane peut être coloriée avec quatre couleurs seulement, sans que deux régions voisines partagent la même couleur. Il a été démontré en 1976.
Mis à jour le 4 min de lecture
L’énoncé tient en une phrase et un enfant peut le comprendre ; sa démonstration a pourtant résisté pendant près de 125 ans et a nécessité, pour la première fois dans l’histoire des grands théorèmes, l’aide d’un ordinateur. Le théorème des quatre couleurs est devenu le symbole d’une question philosophique : une preuve que personne ne peut vérifier à la main est-elle une vraie preuve ?
Ce que dit (et ne dit pas) le théorème
- Deux régions qui ne se touchent qu’en un point (comme les cases d’un échiquier en diagonale) peuvent avoir la même couleur.
- Chaque région doit être connexe : un pays formé de plusieurs morceaux séparés (avec une enclave, par exemple) n’entre pas dans le cadre du théorème si l’on exige que tous ses morceaux aient la même couleur.
- Le théorème ne dit pas qu’il faut toujours quatre couleurs : certaines cartes se colorient avec deux ou trois.
- Il est faux que trois couleurs suffisent toujours : quatre régions qui se touchent deux à deux en exigent quatre.
La traduction en graphe
On place un point dans chaque région et on relie deux points si les régions ont une frontière commune. On obtient un graphe planaire (dessinable sans croisement d’arêtes). Le théorème devient : le nombre chromatique de tout graphe planaire est au plus 4. Voir la théorie des graphes.
Une longue histoire
| Date | Étape |
|---|---|
| 1852 | Francis Guthrie, en coloriant la carte des comtés d’Angleterre, conjecture que quatre couleurs suffisent ; la question est transmise à Augustus De Morgan |
| 1878 | Arthur Cayley présente le problème à la London Mathematical Society |
| 1879 | Alfred Kempe publie une démonstration, acceptée pendant onze ans |
| 1890 | Percy Heawood trouve l’erreur de Kempe et prouve que cinq couleurs suffisent |
| 1913-1960 | Progrès partiels ; la notion de configuration « réductible » se développe (Birkhoff, Heesch) |
| 1976 | Kenneth Appel et Wolfgang Haken, à l’université de l’Illinois, achèvent une preuve assistée par ordinateur |
| 1996 | Robertson, Sanders, Seymour et Thomas publient une preuve simplifiée, toujours informatique |
| 2005 | Georges Gonthier et Benjamin Werner vérifient la preuve avec l’assistant de preuve Coq |
L’erreur de Kempe est restée inaperçue pendant onze ans, mais sa méthode (les « chaînes de Kempe ») a été reprise par tous ses successeurs.
Le principe de la preuve
La démonstration procède par l’absurde :
- On suppose qu’il existe une carte nécessitant cinq couleurs, et on en prend une minimale (avec le moins de régions possible).
- On montre que toute carte contient forcément au moins une configuration d’une liste finie de configurations, dite inévitable.
- On montre que chacune de ces configurations est réductible : si une carte la contient, on peut la simplifier, colorier la carte simplifiée avec quatre couleurs, puis étendre la coloration.
- Une carte minimale ne peut donc pas exister.
Appel et Haken ont dû vérifier 1 936 configurations (ramenées ensuite à environ 1 476), un travail impossible à la main. Le calcul a demandé plus de mille heures de calcul machine. Robertson et ses coauteurs ont réduit la liste à 633 configurations.
Une preuve controversée
En 1976, de nombreux mathématiciens se sont montrés réticents : une démonstration doit pouvoir être relue et comprise. Que se passe-t-il si le programme ou la machine contient une erreur ? Cette controverse a ouvert la voie aux preuves formelles, vérifiées par des logiciels spécialisés dont le noyau est lui-même très petit et contrôlé. La vérification de 2005 a dissipé l’essentiel des doutes. Voir la démonstration mathématique.
Au-delà du plan
| Surface | Nombre de couleurs nécessaires |
|---|---|
| Plan ou sphère | 4 |
| Tore (donut) | 7 |
| Ruban de Möbius | 6 |
| Bouteille de Klein | 6 |
Le cas du tore, prouvé par Heawood, montre que le problème dépend de la topologie de la surface. Paradoxalement, la formule générale de Heawood pour les surfaces plus complexes (démontrée en 1968 par Ringel et Youngs) a été établie avant le cas du plan.
Questions fréquentes
Pourquoi quatre couleurs suffisent-elles pour une carte ?
Parce que toute carte plane contient au moins une zone d’un type simplifiable, ce qui permet de raisonner sur des cartes de plus en plus petites. La vérification de tous les types nécessite un ordinateur.
Qui a démontré le théorème des quatre couleurs ?
Kenneth Appel et Wolfgang Haken en 1976, avec l’aide d’un ordinateur. La conjecture avait été formulée en 1852 par Francis Guthrie.
Les cartographes utilisent-ils quatre couleurs ?
Rarement. Les cartes réelles utilisent souvent plus de couleurs pour la lisibilité, et doivent gérer des pays en plusieurs morceaux et les étendues d’eau, qui sortent du cadre du théorème.
Combien de couleurs faut-il sur un donut ?
Sept : sur un tore, on peut dessiner sept régions toutes voisines deux à deux.