Le théorème des quatre couleurs et les preuves informatisées

Ou pourquoi prouver un théorème qui ne sert à rien ?

Le théorème des quatre couleurs est un problème mathématique qui n’a presque aucune application pratique. Son énoncé affirme que quatre couleurs différentes suffisent pour colorier n'importe quelle carte découpée en régions connexes, de sorte que deux régions limitrophes, c'est-à-dire ayant toute une frontière en commun et non simplement un point, reçoivent toujours deux couleurs distinctes.

Pourtant, la “preuve” de ce théorème réalisée par Kenneth Appel et Wolfgang Haken en 1976 a partagé la communauté scientifique, car elle se base sur une très grande disjonction de cas traités par informatique. C’est en effet la première “preuve” mathématique à avoir été réalisée à l’aide d’un ordinateur, en raison de l’ampleur des calculs à réaliser. Elle s’oppose en cela aux preuves dites “conventionnelles”, dont la production et la relecture ne nécessite que du papier et un crayon.

Un consensus semble avoir été trouvé en 2004, lorsque l’équipe de Georges Gonthier et Benjamin Werner a vérifié informatiquement la justesse d’une preuve du théorème énoncée en 1995. Cependant, l’opposition entre preuve “conventionnelle” et preuve “automatisée” persiste si bien que des mathématiciens cherchent toujours une preuve “conventionnelle” au théorème. En cela le théorème des quatre couleurs pose la question suivante :

Dans quelle mesure le développement des preuves informatiques
ouvre t-il une réflexion sur la nature de la preuve en mathématiques ?

L’histoire de ce théorème questionne la place l’informatique dans les mathématiques et plus particulièrement le fait d’utiliser un ordinateur pour prouver une conjecture par la force de calcul brute. Cependant le décalage entre le peu d’application pratique du théorème et l’acharnement démontré par les mathématiciens pour en trouver une preuve “conventionnelle” pose aussi la question de ce qui est cherché par les scientifiques au delà de la véracité de la conjecture.

Gilles COLLOMBET-GOURDON, Chloé DEPARIS, Amjad EL HAFIDI, Tom FÉVRIER & Laure-Lou TREMBLAY

Chronologie

Découverte de la conjecture

A l’Université de Cambridge, un étudiant en cartographie et mathématiques, Francis Guthrie, colorie une carte des cantons du Royaume-Uni et remarque que quatre couleurs suffisent.

Il en parle alors à son professeur Auguste De Morgan, qui comprit rapidement que le problème était plus compliqué qu’il n’y semblait. Son successeur, Arthur Cayley (du théorème de Cayley-Hamilton), publie le problème en 1878.

1852

Tentative de preuve par Kempe

Alfred Kempe résout le problème en ramenant tout à une carte composée de pentagones, s’inspirant du théorème d’Euler. En retirant les pièces dans l’ordre inverse de leur composition, la carte originelle peut être reconstruite étape par étape, en préservant la condition des quatre couleurs.

Kempe cherche à montrer que si chaque étape du développement préserve la condition, alors la condition serait conservée à l’étape suivante (quand la prochaine pièce serait retirée). Si la carte réduite respecte la condition, alors la carte arbitraire de départ respecte la condition, et alors la conjecture est vraie. La méthode qu’il développe ici s’appelle la méthode dite des “chaînes de Kempe”.

Prouver la conjecture des quatre couleurs est alors un défi, car il s'agit d'un problème difficile.

1879

Contre-exemple de Heawood

Percy John Heawood donne un contre-exemple à la démonstration de Kempe. Il apparaît que les calculs de Kempe étaient faux, mais d’une manière que personne n’arrivait à corriger. Kempe avait trouvé un “nombre inévitable de configurations” mais un de ses membres n’était pas réductible.

Ce contre-exemple fait plus que simplement contredire Kempe, il met en évidence le fait que la recherche d’un set réductible s’avère en réalité beaucoup plus complexe que ce que Kempe avait amorcé, l’ordre de grandeur avoisinant en effet les 10 000 membres de sets réductibles.

1890

Démonstration pour une carte réduite

Le père de l'algèbre moderne, George D. Birkhoff, formule la notion de configuration réductible et démontre la conjecture pour toutes les cartes comportant moins de 26 régions à colorier. Cette borne est améliorée au cours du XXème siècle.

1913

Travaux de Heesch

Heinrich Heesch résout le problème du “carrelage régulier” : il donne une liste de toutes les formes d’une pièce régulière qui peut être utilisée pour carreler le plan et prouve que cette liste est exhaustive. Il développe le principe dit de la C-réductibilité, qui consiste à remplacer une configuration donnée par un sous graphe lui correspondant.

1935

Première utilisation de l'informatique

Dans la continuité de Heinrich Heesch, Karl Dürre écrit un programme pour déterminer la D-réductibilité dans le langage de programmation ALGOL 60. Le programme lui permet aussi de vérifier des configurations de Kempe plus complexes.

1965

Première tentative de preuve informatique

En expérimentant avec des sets de configurations, Yoshio Shimamoto découvre la configuration du “fer à cheval”, montrant que la D-réductibilité est incompatible avec l’existence d’une carte de cinq couleurs, et donc prouverait la conjecture du théorème des quatre couleurs. Cependant, le programme de Dürre montra que cette configuration n’était pas D-réductible. La démonstration de Shimamoto échoue finalement.

1971

Un problème qui intrigue de plus en plus

Martin Gardner publie dans Scientific American une carte qu’il présente comme contre-exemple de la conjecture du théorème des quatre couleurs. Même si cet exemple est en réalité un “poisson d’avril”, cela montre l’intérêt que suscite la conjecture dans la communauté des mathématiciens.

1975

La naissance de la controverse

Haken, Appel et Koch présentent leur preuve : ils étudient sur papier 10 000 cartes, en extraient 1500 configurations et testent 1 000 000 000 de coloriages avec un programme IBM, afin d'en prouver la C-réductibilité. Cette preuve met en oeuvre une interaction humain/machine : la construction de sets est inévitablement réalisée à la main, de même que la vérification de la bonne implémentation des configurations.

Une étude de 140 pages est publiée, décrivant la stratégie de la démonstration. La deuxième partie liste le set de configurations inévitables et décrit le programme vérifiant que chaque set est réductible. Au délà du théorème des quatre couleurs, il s'agit de montrer que l'informatique peut être un outil au service des mathématiques.

En savoir plus sur la controverse

1976

Un débat qui se poursuit

Frank Allaire apporte une nouvelle preuve de la conjecture avec un set différent de configurations inévitables et des preuves plus convaincantes de réductibilité. Son travail s’inscrit dans la lignée de la démonstration de 1976 et vise à répondre aux critiques suscitées.

1977

Réduction du nombre de configurations

Neil Robertson et Daniel Sanders réalisent informatiquement la procédure de “décharge” que Appel et Haken avaient effectué manuellement. Il s’agit donc de rechercher des configurations de sets inévitables. Ils réduisent le nombre de configurations à 633. Ils font cependant face à une réaction toujours hostile devant l’usage de l’ordinateur.

1993

Un premier consensus

Robertson, Saunders, Seymour et Thomas présentent une amélioration de la preuve de Appel, Haken et Koch : ils optimisent l’analyse et remarquent que l’étude des 633 configurations mises en évidence en 1993 suffit. De plus l’étude des 10 000 cartes et des 1 000 000 000 de coloriages peut se faire avec des programmes en langage C. Ceux-ci sont beaucoup plus compréhensibles et rapides : en trois heures la tâche est effectuée alors qu’il avait fallu deux mois et demi à Appel et Haken pour aboutir au même résultat.

Ils publient finalement un article de 35 pages compréhensible et lisible qui établit une forme de consensus au sein de la communauté scientifique. Il y a alors une volonté de rendre la preuve accessible à l'ensemble des mathématiciens.

1995

La fin de la controverse ?

Georges Gonthier et Benjamin Werner convertissent la preuve précédente sur le logiciel Coq, en remplaçant les programmes C par un script de preuve. Cela leur permet de démontrer la validité de la preuve de 1995. L'enjeu est ici de faire un coup d'éclat, afin d'appuyer la démocratisation des assistants de preuve comme Coq. De fait, la controverse semble fermée.

Est-ce vraiment le cas ?

2004