Exposé pour le marathon des sciences du 35e Festival d'Astronomie de Fleurance le 2 août 2025. Il s'agit d'une présentation succincte des théorèmes des 4/7/9... couleurs
cartes telles que la conjecture des quatre couleurs soit fausse. Ici, les cinq pays comportent tous des exclaves des quatres autres donc sont tous voisins.
Peter Guthrie Tait • 1890: Réfutation de la preuve de Kempe par Percy Heawood • 1891: Réfutation de la preuve de Peter Guthrie Tait par Julius Petersen
exclave sur une sphère peut être coloriée avec cinq couleurs. • preuve par récurrence d’une vingtaine de lignes • cela repose sur le fait qu’il existe un pays avec au plus cinq voisins
seul à croire que cette conjecture était fausse. L’intuition de Coxeter a maintenant été confirmée. En novembre 1974, William McGregor, un théoricien des graphes de Wappingers Falls, dans l’État de New York, a construit une carte de 110 régions qui ne peuvent être colorées avec moins de cinq couleurs. Le rapport technique de McGregor paraîtra en 1978 dans le Journal of Combinatorial Theory, Series B.” Six sensational discoveries that somehow or another have escaped public attention, Martin Gardner, Scientific American, avril 1975
Schématiquement, il y a une phase de réduction à certains cas puis une phase d’analyse de ces cas. • Il y a recours à l’outil informatique pour ”tester” ces cas.
l’étude des graphes planaires triangulés quasi 6-connexes • on exhibe 1476 configurations qui sont inévitables dans ces graphes • par récurrence, on enlève une configuration inévitable et on étend les coloriages du graphe privé de cette configuration au graphe de départ
un algorithme de coloriage avec 4 couleurs donc la complexité est quartique. La simplification de la preuve par Neil Robertson, Daniel P. Sanders, Paul Seymour, et Robin Thomas (1996) donne un algo- rithme quadratique!
goût d’échec : ils avaient utilisé un ordinateur pour faire la démonstration à leur place ! La controverse mathématique autour de la démonstration s’est peut-être apaisée avec la publication de leur livre et l’élégante révision de 1995 par Robertson, Saunders, Seymour et Thomas. Cependant, quelque chose clochait encore : les deux démonstrations combinaient un argument textuel, qui pouvait être raisonnablement vérifié par inspection, avec un code informatique qui ne pouvait pas l’être.” Formal Proof — The Four-Color Theorem, Georges Gonthier, Notices of the AMS, décembre 2008
goût d’échec : ils avaient utilisé un ordinateur pour faire la démonstration à leur place ! La controverse mathématique autour de la démonstration s’est peut-être apaisée avec la publication de leur livre et l’élégante révision de 1995 par Robertson, Saunders, Seymour et Thomas. Cependant, quelque chose clochait encore : les deux démonstrations combinaient un argument textuel, qui pouvait être raisonnablement vérifié par inspection, avec un code informatique qui ne pouvait pas l’être.” Formal Proof — The Four-Color Theorem, Georges Gonthier, Notices of the AMS, décembre 2008 • Preuve formelle en Rocq par Georges Gonthier et Benjamin Werner, 2005
la sphère si, et seulement si, il ne contient pas un sous-graphe dont une subdivision est K5 ou K3,3. K5 K3,3 La géométrie des pays est peu importante... mais celle de la planète?
Joseph N. Portney (1927-2012), un ingénieur en aéronautique et ancien de US Air Force, a conçu un livret et une série d’affiches éducatives ”What if the earth were...”