L'ordinateur qui démontre

Le télégramme d’Urbana

Été 1976, université de l’Illinois. Le tampon de la machine à affranchir du département de mathématiques change soudain de message : Four colors suffice. Quatre couleurs suffisent. Kenneth Appel et Wolfgang Haken viennent d’annoncer la démonstration d’une conjecture vieille de cent vingt-quatre ans : toute carte de géographie peut être coloriée avec quatre couleurs seulement, sans que deux régions voisines partagent la même teinte.

Mais leur démonstration ne ressemble à rien de connu. L’idée maîtresse est humaine : ramener l’infinité des cartes possibles à une liste finie de $1\,936$ configurations, puis vérifier que chacune est « réductible ». C’est la vérification qui déraille : elle exige environ $1\,200$ heures de calcul sur les ordinateurs de l’université. Aucun être humain ne relira jamais l’intégralité de cette preuve. Aucun n’en serait capable, quand bien même il y consacrerait sa vie.

La communauté mathématique se déchire. Depuis Euclide, une démonstration est un texte qu’un cerveau humain peut parcourir et approuver, ligne à ligne. Que vaut un théorème dont la justification tient dans le silence d’une machine ? Et si le programme contenait un bug ? Et si le compilateur, le processeur, la mémoire avaient flanché une nuit de 1976 ? Certains parlent de « preuve qui n’en est pas une » ; d’autres répondent que les preuves humaines de quatre cents pages, relues par trois collègues fatigués, ne sont pas plus fiables.

Le retournement survient en 2005. Georges Gonthier, avec Benjamin Werner, reconstruit toute la démonstration dans l’assistant de preuve Coq : cette fois, ce n’est plus un programme qui teste des cas, c’est un vérificateur de logique qui contrôle chaque inférence, y compris celles des calculs. Il ne reste qu’une chose à croire : le petit noyau de Coq, quelques milliers de lignes scrutées depuis des années. L’argument s’inverse élégamment : la partie la plus sûre du théorème des quatre couleurs est désormais celle que la machine a vérifiée. Ce sont les passages « humains » des preuves classiques qui font figure de maillons faibles.

L’autre talent de la machine : réfuter

Car il existe un versant où l’ordinateur n’a jamais fait débat. Vous le connaissez : c’est le contre-exemple.

En 1919, George Pólya conjecture que jusqu’à tout rang $n \geqslant 2$, les entiers ayant un nombre impair de facteurs premiers (comptés avec répétition) restent au moins aussi nombreux que les autres. On vérifie, à la main puis à la machine : vrai sur des millions d’entiers, puis des centaines de millions. En 1958, Brian Haselgrove démontre pourtant qu’un contre-exemple existe, sans en produire aucun. En 1960, Sherman Lehman en exhibe un : $906\,180\,359$. En 1980 enfin, Minoru Tanaka isole le plus petit :

Vraie plus de neuf cents millions de fois. Fausse quand même.

La conjecture de Mertens pousse le vertige d’un cran. Elle affirmait que la fonction de Mertens $M(n)$ vérifie $|M(n)| < \sqrt{n}$ pour tout $n > 1$ ; sa vérité aurait entraîné l’hypothèse de Riemann. En 1985, Andrew Odlyzko et Herman te Riele la réfutent par un calcul massif sur les zéros de la fonction zêta… sans exhiber le moindre contre-exemple explicite. On sait qu’il en existe un ; on sait qu’il se cache au-delà de $10^{14}$ ; personne ne l’a jamais vu, et il échappe peut-être pour toujours à toute recherche exhaustive.

Vous reconnaissez la morale, c’est celle du chapitre. Le script contre_exemple(P, N) du cours et le CDC 6600 de Lander et Parkin font le même métier : balayer des cas. Si un témoin tombe, l’énoncé universel est mort, définitivement, et la preuve tient en une ligne. Mais si la machine revient bredouille après $906$ millions de succès, elle n’a rien démontré : c’est le return None du cours, à l’échelle de l’histoire des mathématiques. Un « pour tout » ne se prouve jamais en accumulant des exemples.

Et aujourd’hui ?

Les héritiers de Coq s’appellent désormais Lean et sa bibliothèque mathlib, où des milliers de théorèmes, des plus élémentaires aux plus récents, sont vérifiés ligne de logique par ligne de logique ; la question de 1976, « qu’est-ce qu’une preuve ? », est devenue un champ de recherche à part entière.

Sources

• K. Appel et W. Haken, Every planar map is four colorable, Illinois Journal of Mathematics, 1977.
• G. Gonthier, Formal Proof, The Four-Color Theorem, Notices of the AMS, 2008.
• C. B. Haselgrove, A disproof of a conjecture of Pólya, Mathematika, 1958 ; R. S. Lehman (1960) ; M. Tanaka (1980).
• A. M. Odlyzko et H. te Riele, Disproof of the Mertens conjecture, Journal für die reine und angewandte Mathematik, 1985.
• Pages Wikipédia : Four color theorem, Pólya conjecture, Mertens conjecture (consultées en juillet 2026).