🎛️ Colorie cette carte avec 4 couleurs
Clique sur une région, puis sur une couleur. Règle : deux régions voisines ne peuvent pas avoir la même couleur. Le théorème dit que c'est toujours faisable avec 4 couleurs maximum.
Région sélectionnée
—
Régions coloriées
0 / 12
Statut
En cours
Sélectionne une région en cliquant dessus, puis choisis une couleur. Évite les conflits avec les voisins.
🎓 1852 : un étudiant trace une carte
Francis Guthrie, étudiant à Londres, colorie une carte des comtés d'Angleterre. Il remarque qu'il y arrive toujours avec seulement 4 couleurs sans que deux régions voisines n'aient la même. Intrigué, il en parle à son frère Frederick, qui en parle à son professeur, le célèbre Augustus De Morgan.
De Morgan écrit à William Rowan Hamilton (le concepteur des quaternions) le 23 octobre 1852. L'énoncé est cristallin :
« Toute carte plane peut être coloriée avec 4 couleurs ou moins de telle sorte que deux régions partageant une frontière commune (pas un simple point) reçoivent des couleurs différentes. »
⏳ 1852-1976 : 124 ans de tentatives infructueuses
- 1879 — Alfred Kempe publie une « preuve » dans American Journal of Mathematics. Elle est célébrée pendant 11 ans.
- 1890 — Percy Heawood trouve une erreur fatale dans la preuve de Kempe. Heawood sauve néanmoins une partie : le théorème des 5 couleurs (toute carte plane se colorie avec 5 couleurs).
- 1900-1960 — Des centaines de mathématiciens s'attaquent au problème. Aucune preuve. Aucune carte demandant 5 couleurs trouvée.
- 1969 — Heinrich Heesch propose une méthode de « décharge » : on liste toutes les configurations « inévitables » dans une carte, et on montre qu'elles sont toutes « réductibles ». Mais il y en a trop pour la main.
💻 1976 : Appel et Haken cassent le mur
Kenneth Appel et Wolfgang Haken, à l'université de l'Illinois, avec l'aide du programmeur John Koch, formalisent l'approche d'Heesch et la mettent en œuvre informatiquement.
Leur stratégie : trouver un ensemble de 1 936 configurations inévitables, et prouver pour chacune qu'elle est réductible. Total : 1 200 heures de calcul sur un IBM 360 (∼50 jours).
Juillet 1976, l'annonce tombe : le théorème des 4 couleurs est démontré. L'université de l'Illinois fait apposer sur tout son courrier le tampon : « Four colors suffice ».
🤔 La crise philosophique : qu'est-ce qu'une preuve ?
Avant 1976, une preuve mathématique était un raisonnement vérifiable par un humain en temps fini. Les preuves d'Euclide, Pythagore, Gauss, Cauchy — toutes lisibles par un mathématicien expert.
Avec Appel-Haken, on a une preuve impossible à vérifier humainement. On doit faire confiance :
- aux algorithmes implémentés,
- au compilateur Fortran qui les a traduits,
- au matériel IBM qui les a exécutés,
- au programmeur qui les a écrits.
Certains, comme le philosophe Thomas Tymoczko, défendent que cela change la nature même des mathématiques : elles deviennent empiriques au sens des sciences expérimentales. D'autres, comme Donald Knuth, refusent : « Une preuve par ordinateur n'est pas une preuve mathématique. »
✅ 1995 : Robertson-Sanders-Seymour-Thomas simplifient
Neil Robertson, Daniel Sanders, Paul Seymour et Robin Thomas reprennent le problème et trouvent une preuve plus simple : seulement 633 configurations au lieu de 1 936. Toujours non vérifiable à la main, mais plus claire.
En 2005, Georges Gonthier (Microsoft Research) formalise complètement la preuve avec l'assistant de démonstration Coq. Cette fois, chaque étape est vérifiée par un noyau logique de quelques milliers de lignes — bien plus sûr qu'un compilateur. La preuve est désormais totalement formelle.
🌍 Pourquoi seulement 4 ?
Pourquoi pas 3 ? Voici un contre-exemple simple :
Une carte avec 4 pays mutuellement voisins (genre K₄)
requiert 4 couleurs. Exemple : France-Allemagne-Suisse-Italie
(les 4 partagent des frontières 2 à 2).
Pourquoi pas 5 ? C'est précisément l'objet du théorème : aucune carte plane ne requiert 5 couleurs. La planarité est essentielle : sur un tore (donut), il faut 7 couleurs (Heawood, 1890). Sur une bande de Möbius, 6. Le « bon » nombre dépend de la topologie de la surface.
📊 Le passage aux graphes
Le théorème des 4 couleurs est en fait un théorème de théorie des graphes : toute carte se traduit en graphe (un sommet par pays, une arête par frontière commune). Et le graphe ainsi obtenu est planaire (peut être dessiné sans croisement).
Tout graphe planaire est 4-coloriable.
🚀 Applications modernes de la coloration
- Allocation de fréquences radio : antennes proches ne doivent pas émettre sur la même fréquence (interférences). C'est un problème de coloration de graphes — voisins = même couleur interdite.
- Compilateurs : allocation de registres CPU. Chaque variable « vivante » en même temps qu'une autre ne peut pas occuper le même registre. Coloration du graphe d'interférence.
- Planification : examens à programmer (matières en commun = pas même créneau), horaires de cours, plannings d'infirmières.
- Réseau cellulaire : allocation des canaux GSM, 4G, 5G.
- Test logiciel : génération de cas de test couvrant tous les chemins d'un programme.
- Sudoku : c'est un cas particulier de coloration de graphes (9 couleurs, 81 sommets, contraintes de lignes/colonnes/blocs).
- Graphisme : tessellation de surfaces, génération procédurale de motifs (jeux vidéo, animations).
- Bioinformatique : repliement de protéines, alignement de génomes.
🏆 L'héritage : preuves assistées par ordinateur
Depuis Appel-Haken, plusieurs autres grands théorèmes ont été prouvés par ordinateur :
- Conjecture de Kepler (Hales 1998, formalisée 2014) : l'empilement le plus dense de sphères en 3D est l'empilement « cannonball ». Preuve : 3 gigaoctets de code.
- Boolean Pythagorean Triples (Heule-Kullmann-Marek 2016) : peut-on colorier ℕ avec 2 couleurs sans triplet pythagoricien monochrome ? Non. 200 téraoctets de preuve, la plus grande de l'histoire.
- Conjecture de Robbins (William McCune 1996) : prouvée par l'IA EQP en 8 jours. Aucun humain n'y était parvenu en 60 ans.
- 2024 — DeepMind AlphaProof : résout 4 problèmes sur 6 des Olympiades internationales de maths, médaille d'argent. Les preuves automatiques entrent dans une nouvelle ère.
📐 Le lien avec ton programme
- Théorie des graphes : pas au programme BAC SM marocain, mais accessible en TPE/option info. Les notions de sommets, arêtes, planarité sont intuitives.
- Récurrence : la plupart des preuves « manuelles » de cas particuliers se font par récurrence sur le nombre de régions.
- Formule d'Euler V − E + F = 2 (vue dans le concept Königsberg) : c'est l'outil principal pour prouver le théorème des 5 couleurs (résultat plus faible mais élégant et accessible).
- Algorithmique : la coloration optimale d'un graphe est NP-difficile en général. Mais pour les graphes planaires, le théorème des 4 couleurs donne une borne constructive.
- Logique et informatique : la formalisation en Coq introduit aux assistants de preuve. Outil de plus en plus utilisé en recherche (cryptographie, sécurité critique).