Le nombre chromatique d'un graphe planaire est inférieur ou égal à 4.

L'histoire du théorème des quatre couleurs remonte au moins au XIXè siècle.
En 1852 Francis Guthrie, mathématicien et botaniste anglais, remarque qu'il lui suffit de quatre couleurs pour colorier la carte des cantons d'Angleterre,
sans donner la même couleur à deux cantons qui ont une frontière commune.
En 1879, Kempe publie une première "preuve'' de la conjecture, qui est malheureusement fausse.
La première démonstration date de 1976, par Appel et Haken. Leur preuve consiste à se ramener à un nombre fini, mais très grand,
de configurations. Ensuite, pour chaque configuration, il faut vérifier que 4 couleurs suffisent.
Ces nombreuses vérifications ont été faites par ordinateur. Ceci produisit alors une tempête incroyable chez les mathématiciens. C'était la première preuve
produite grâce à l'outil informatique. En particulier, on ne pouvait la vérifier humainement!
Encore maintenant, on ne connait pas de preuves n'utilisant pas l'ordinateur. En revanche, de nombreuses autres conjectures célèbres
ont été démontrées à l'aide de l'informatique, comme la conjecture de Képler.
Consulter aussi...