Le théorème des quatre couleurs affirme que toute carte dessinée sur un plan peut être coloriée avec au plus quatre couleurs de sorte que deux régions partageant une frontière n'aient jamais la même couleur. Deux régions qui ne se touchent qu'en un seul point peuvent partager une couleur. Le théorème s'applique à toute carte, aussi complexe soit-elle.
Regions 1, 2, 3, 4 each border multiple others. The left (4) and right (4) regions share no border, so they can share a colour. Exactly 4 colours needed here.
Francis Guthrie a conjecturé le théorème en 1852 en coloriant une carte des comtés anglais. Il remarqua que quatre couleurs semblaient toujours suffire, mais ne put le prouver. Le problème a résisté aux mathématiciens pendant 124 ans. De nombreuses preuves erronées furent publiées puis réfutées. Cinq couleurs suffisent toujours, ce qui peut être démontré à la main à l'aide de la formule d'Euler pour les graphes planaires.
The four colour theorem took 124 years from conjecture to proof. The 1976 proof was the first major theorem verified by computer.
La preuve de 1976 par Kenneth Appel et Wolfgang Haken fut le premier grand théorème démontré par ordinateur. Elle réduisit toutes les cartes possibles à 1 936 configurations et fit vérifier chacune par un ordinateur en plus de 1 200 heures de calcul. De nombreux mathématiciens étaient mal à l'aise avec une preuve impossible à vérifier à la main. Une preuve lisible par l'homme, si elle existe, reste à découvrir.
Five outer regions (an odd number) force the ring to use 3 colours: no 2-colouring of a 5-cycle exists. The centre region is adjacent to all five, touching all three ring colours, so it must be a fourth colour. This shows four is genuinely sometimes necessary.
Toute carte dessinée sur un plan peut être coloriée avec au plus quatre couleurs de sorte que deux régions partageant une frontière n'aient jamais la même couleur. Conjecturé par Francis Guthrie en 1852. Démontré par Appel et Haken en 1976 à l'aide d'un ordinateur vérifiant 1 936 configurations, ce qui en fait le premier grand théorème prouvé avec assistance informatique. Une vérification plus courte par Robertson, Sanders, Seymour et Thomas en 1997 a réduit ce nombre à 633 configurations. Le théorème ne s'applique pas sur un tore, où sept couleurs peuvent être nécessaires.