Théorème des quatre couleurs
Il en faut quatre, jamais plus. Deux régions qui partagent une frontière reçoivent des couleurs différentes, et quatre suffisent toujours, quel que soit le découpage. Trois ne suffisent pas toujours : la Belgique, le Luxembourg, l'Allemagne et la France se touchent deux à deux.
Il en faut quatre, jamais plus. Deux régions qui partagent une frontière reçoivent des couleurs différentes, et quatre suffisent toujours, quel que soit le découpage. Trois ne suffisent pas toujours : la Belgique, le Luxembourg, l'Allemagne et la France se touchent deux à deux.
Il a raisonné par l'absurde, puis par force brute. Kenneth Appel et Wolfgang Haken montrent qu'une plus petite carte exigeant cinq couleurs contiendrait forcément l'un de plus d'un millier de motifs, qu'on sait tous simplifier. L'ordinateur vérifie ces motifs un par un, en plus de mille heures de calcul, et la carte rebelle ne peut donc pas exister.
On la fait vérifier par un second logiciel, conçu pour contrôler chaque étape logique. En 2005, Georges Gonthier et Benjamin Werner ont réécrit toute la preuve dans un assistant de preuve. Il ne reste alors à croire qu'un petit noyau logiciel, et non plus les programmes écrits pour l'occasion.