Quatre couleurs sont suffisantes pour colorier une carte, tout en satisfaisant le critere des frontieres, la seule condition imposée sur la carte étant que les pays doivent être connexes (en un seul morceau), sinon en découpant un pays en 4 morceau à l'intérieur d'un autre pays on aboutit à une contradiction manifeste.

Ce résultat est connu en mathématiques sous le nom de "Théorème des quatre couleurs", après être resté au stade de conjecture pendant des décennies il fut prouvé en 1976 par Appel et Haken. La démonstration fait appel à des procédés combinatoires complexes et repose au final sur un calcul d'ordinateur. Une preuve en Coq (langage qui permet la description formelle d'une preuve dans le but de sa vérification automatique par un ordinateur) a été récemment (préciser ?) publiée par Georges Gonthier.

On peut par contre prouver un "Théroème des cinq couleurs" (plus faible, donc) par récurrence en s'appuyant sur la formule d'Euler-Poincaré.

attachment:1.jpg