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

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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 ?