Contexte historique

En juillet 1976, Kenneth Appel et Wolfgang Haken annoncent la résolution du problème des quatre couleurs, un défi ouvert depuis plus d’un siècle. Le théorème affirme qu’il suffit de quatre teintes pour colorier n’importe quelle carte plane sans que deux régions adjacentes partagent la même couleur. Leur démonstration repose sur 1 200 heures de calcul effectuées sur un ordinateur de l’époque, générant 10 milliards de décisions et aboutissant à un texte de 700 pages. Cette approche marque la première utilisation d’une machine pour accomplir la majeure partie du raisonnement mathématique.

Méthode informatique

Le processus s’appuie sur une réduction exhaustive du problème à un nombre fini de configurations critiques. L’algorithme, développé avec l’aide du programmeur John Koch, explore systématiquement chaque configuration possible, éliminant celles qui ne violent pas la contrainte de coloration. Chaque branche de l’arbre de recherche nécessite une décision binaire, d’où le compte de 10 milliards de décisions. Le calcul s’est déroulé sur un système à architecture mainframe typique des années 1970, limité par la vitesse du processeur et la capacité de mémoire, ce qui explique le temps de 1 200 heures requis.

Le résultat final, présenté sous forme de 700 pages de preuves détaillées, combine des arguments humains (déductions théoriques, lemmas) et des vérifications automatisées (tests de configurations). Cette hybridation a conduit les auteurs à déclarer que le système « avait commencé à nous enseigner des méthodes inattendues », soulignant une forme d’apprentissage émergent du logiciel.

Débats et implications

La communauté mathématique a réagi de façon contrastée. Des figures comme Herbert Wilf et Paul Halmos ont dénoncé la preuve comme une « oraculaire », arguant qu’une démonstration inobservable ne correspond pas à la pratique traditionnelle. D’autres, dont Bill Tutte, ont finalement reconnu la validité du résultat, même en composant un poème en l’honneur du succès. L’âge des mathématiciens a également influencé les opinions : les chercheurs de plus de 40 ans restaient sceptiques, tandis que les plus jeunes acceptaient plus facilement la méthode informatique.

Sur le plan philosophique, Thomas Tymoczko a souligné que le théorème était « non‑surveillable », c’est‑à‑dire qu’aucun mathématicien n’a pu vérifier chaque étape du calcul. Cette situation a déclenché un débat sur la nature même de la preuve : doit‑elle être vérifiable par l’esprit humain ou suffit‑elle à être logiquement infaillible, même si elle repose sur une machine ? Ted Swart a répliqué que la preuve assistée par ordinateur n’est qu’une extension du raisonnement à la main, rappelant que les humains sont sujets à la fatigue alors que les machines ne le sont pas.

Conséquences techniques et perspectives

Le succès de la preuve a ouvert la voie à l’utilisation systématique de la vérification formelle et des assistants de preuve (Coq, Isabelle) dans les décennies suivantes. Il a également mis en évidence les limites des architectures de calcul de l’époque, incitant les chercheurs à développer des algorithmes plus efficaces et des systèmes de preuve certifiables. Aujourd’hui, les preuves assistées par ordinateur sont courantes dans la théorie des nombres, la topologie et la vérification de logiciels critiques, montrant que le « premier choc » de 1976 a transformé la pratique mathématique sans la remplacer entièrement.