Une preuve qu’un seul esprit ne peut embrasser

1. Des applaudissements polis

Le 22 juillet 1976, deux mathématiciens de l’université de l’Illinois, Kenneth Appel et Wolfgang Haken, annoncent que quatre couleurs suffisent pour colorier une carte plane, dans les conditions habituelles du problème, sans donner la même couleur à deux régions qui ont une portion de frontière commune. Se toucher en un seul point ne compte pas. En août, à l’université de Toronto, Haken vient présenter leur démonstration au congrès d’été de l’American Mathematical Society et de la Mathematical Association of America. Il a quarante-huit ans, est né à Berlin et s’est fait un nom en topologie, dans l’étude des formes de l’espace à trois dimensions. La salle est pleine à craquer. Un problème ouvert depuis cent vingt-quatre ans vient de trouver sa solution.

Donald Albers est dans la salle. D’après son récit, il s’attend, à la fin de l’exposé, à une véritable ovation. Il n’entend que des applaudissements polis. Après la conférence, les mathématiciens lui disent les uns après les autres leur malaise. Ce qui les gêne, c’est l’allure de cette démonstration : une bonne part a été calculée par des machines, au prix de mille deux cents heures de travail, et personne ne peut la vérifier à la main d’un bout à l’autre. Ils reviennent souvent à la même idée : une erreur se cache peut-être dans les centaines de pages imprimées par l’ordinateur. Albers glisse alors sa propre question : ne seraient-ils pas en train de l’espérer ? Son reportage paraît au printemps 1981 dans une revue de mathématiques. Le titre commence par les applaudissements polis et se poursuit par une question : qu’est-ce qu’une preuve, aujourd’hui ?

Un enfant peut comprendre le problème dès qu’on le lui explique. Son origine est tout aussi simple. En 1852, un jeune homme, Francis Guthrie, colorie une carte des comtés anglais. Quatre couleurs semblent toujours suffire. Il en parle à son frère Frederick, qui interroge son professeur, De Morgan. Le 23 octobre, De Morgan transmet la question par lettre à Hamilton, à Dublin. Il commence en disant, en substance, qu’un étudiant lui a demandé ce jour-là d’expliquer un fait dont il ignorait jusque-là qu’il fût un fait, et dont il n’est toujours pas sûr. Trois jours plus tard, Hamilton répond qu’il n’a guère l’intention de s’occuper dans un avenir proche de ce quaternion de couleurs. Les quaternions, il les a inventés neuf ans auparavant. Le jour de sa découverte, il en a gravé la formule dans la pierre d’un pont devant lequel il passait. Depuis, ils occupent toute sa vie.

Francis Guthrie a vingt et un ans lorsqu’il pose la question et vient d’obtenir son diplôme de droit. Il n’y reviendra pas et n’écrira pas une ligne sur le sujet. Parti en Afrique du Sud, il sera professeur de mathématiques pendant plus de vingt ans au South African College, au Cap. Le reste de son attention ira aux bruyères du Cap, qu’il étudiera avec un botaniste jusqu’à sa mort. Un genre de plantes portera son nom.

Moins d’une minute pour énoncer le problème, cent vingt-quatre ans pour le démontrer. Quant au malaise de Toronto, il faut remonter plus loin pour le comprendre : ce problème avait déjà été démontré une première fois.

2. Une preuve qui vécut onze ans

Pendant plus de vingt ans, la question dort dans un tiroir. Le 13 juin 1878, à une séance de la London Mathematical Society, Cayley demande simplement si quelqu’un l’a résolue. L’année suivante, un ancien de ses élèves se manifeste. En juillet 1879, Alfred Kempe, avocat plaidant à Londres, annonce une démonstration dans Nature ; le texte complet paraît ensuite dans une revue mathématique américaine. Plaider est son métier. Les mathématiques, il les a apprises auprès de Cayley, à Cambridge. Sa démonstration est claire et son idée ingénieuse : lorsqu’une chaîne de régions alterne entre deux couleurs, on peut échanger ces deux couleurs sur toute la chaîne sans toucher au reste de la carte. On appellera cela une chaîne de Kempe. La preuve est acceptée. Elle le restera onze ans. Dès l’année suivante, le physicien écossais Tait en propose deux autres, riches en idées astucieuses, mais aussi en erreurs élémentaires. À cette époque, beaucoup tiennent l’affaire pour réglée.

En 1890, Heawood, enseignant en mathématiques à Durham, met le doigt sur la faille. Pour traiter une région entourée de cinq voisines, Kempe effectue deux échanges de couleurs successifs. Il suppose qu’ils ne se gênent pas. Or les deux chaînes peuvent s’entrelacer sur la carte : le premier échange risque de détruire la condition nécessaire au second. La démonstration s’effondre.

Heawood ne se contente pas de démolir. Avec les outils rescapés de la preuve, il établit un résultat un peu plus faible : cinq couleurs suffisent toujours. L’échange des couleurs le long d’une chaîne survit lui aussi et devient un outil courant de la théorie des graphes. Qu’une démonstration ratée laisse quelque chose d’utile n’a rien d’exceptionnel dans l’histoire des mathématiques. Heawood, lui, poursuit sa carrière à Durham, d’abord comme enseignant, puis comme professeur ; il sera vice-chancelier de l’université de 1926 à 1928. Il travaillera encore près de soixante ans sur la coloration des cartes. Son dernier article sur le sujet paraît en 1949 : il a quatre-vingt-sept ou quatre-vingt-huit ans. Ses collègues gardent le souvenir d’un petit homme maigre, légèrement voûté, portant une barbe immense et souvent une cape de coupe étrange, manifestement très ancienne. Un chien a l’autorisation d’assister à ses cours.

Ce qui étonne, c’est le temps écoulé. Une démonstration parfaitement lisible est restée onze ans sous les yeux des meilleurs mathématiciens sans que personne ne voie où elle se trompait. Qu’un être humain puisse lire une preuve n’a jamais voulu dire que quelqu’un l’avait effectivement vérifiée. Une moitié du malaise de Toronto vient de là : si même les démonstrations lisibles peuvent nous échapper, sur quoi fonder notre confiance dans celles que personne ne peut lire ?

3. La salle des machines de l’Illinois

Avant Appel et Haken, l’Allemand Heinrich Heesch s’était déjà engagé dans cette voie avec l’aide d’ordinateurs. Dans les années 1960, il met au point une méthode décisive. En 1967, Haken vient le voir pour ce problème. Au cours des quatre années suivantes, Heesch se rend plusieurs fois aux États-Unis, où les machines sont plus puissantes et plus rapides ; Haken fait partie de ses collaborateurs. Au moment le plus crucial, la fondation nationale allemande pour la recherche lui retire son financement.

Au début des années 1970, Haken raconte dans une conférence les essais qu’ils ont menés sur les ordinateurs du laboratoire de Brookhaven. Des spécialistes de l’informatique, explique-t-il, lui ont assuré que la voie du calcul n’aboutirait pas. À la fin, Appel, son collègue du même département, vient le trouver : ces experts ont tort. Cela prendra du temps, mais c’est faisable. Ils commencent à travailler ensemble en 1972. Appel se charge surtout des calculs, Haken de la théorie.

Ils n’écrivent pas une démonstration ordinaire à laquelle la machine n’aurait plus qu’à ajouter quelques calculs. L’ordinateur participe à toute l’élaboration : les hommes fixent des règles, la machine les met à l’épreuve, les difficultés qu’elle rencontre conduisent les hommes à revoir les règles, puis ils recommencent. Ces allers-retours durent des années. Au bout du compte : quatre cent quatre-vingt-sept règles, environ dix mille situations locales examinées à la main et quelque deux mille configurations vérifiées une par une par ordinateur. Certaines demandent quatre-vingt-dix minutes sur la machine la plus lente, trente encore sur la plus rapide. Le total avoisine mille deux cents heures de calcul ; d’après leur propre estimation, les ordinateurs ont effectué quelque dix milliards de tests logiques. Pour la dernière étape, ils obtiennent du temps sur un gros ordinateur que l’université de l’Illinois vient d’acheter, en mars 1976, pour ses services administratifs.

Même le travail manuel ne repose pas seulement sur leurs quatre mains. La dernière version des règles est établie à la main. Pendant plusieurs mois du premier semestre de 1976, Appel, Haken et Dorothea, la fille de Haken, passent une à une les mille neuf cent trente-six configurations qui formeront la liste. Au fil de ces années, Dorothea passe du lycée à l’université ; elle deviendra elle-même chercheuse en informatique. Avant de rendre la preuve publique, les deux familles mobilisent cinq de leurs enfants : Dorothea et Armin Haken, Laurel, Peter et Andrew Appel. Page après page, ils comparent les figures de l’article avec les sorties de l’ordinateur pour repérer les erreurs de copie. Laurel, la fille d’Appel, a treize ans. Elle vérifie quelque sept cents pages. Haken racontera plus tard qu’elle y a consacré un mois entier et trouvé environ huit cents erreurs : huit cents sur sept cents pages, ce n’était pas beaucoup, à ses yeux. Elle en avait corrigé six cent cinquante toute seule. Pour les autres, cinq jours avaient suffi à Haken et Appel.

La liste ne cesse d’évoluer. La prépublication contient mille neuf cent trente-six configurations ; l’article définitif n’en garde que mille quatre cent quatre-vingt-deux ; un remaniement ultérieur ramène le total aux environs de mille quatre cent cinq. La démonstration paraît en deux parties en 1977, avec John Koch comme coauteur de la partie consacrée à la vérification. Elle s’accompagne d’environ quatre cent cinquante pages sur microfilm, pleines de figures et de relevés de contrôle. Appel et Haken ont fait le calcul : pour une seule configuration difficile, vérifier toute la sortie de la machine occuperait une personne quarante heures par semaine pendant plusieurs années. En 1989, plus de dix ans après, ils publieront de nouveau l’ensemble de la démonstration, cette fois sous la forme d’un livre.

À l’automne 1976, le département de mathématiques de l’université de l’Illinois fait modifier sa machine à affranchir. Sur chaque lettre qui en sort figure désormais cette phrase : quatre couleurs suffisent.

4. Une liste

L’ordinateur vérifie les entrées d’une liste. Pour comprendre ce qu’est cette liste et pourquoi on ne peut s’en passer, il faut revenir à Kempe : la démonstration de 1976 a la même ossature que celle de 1879. Supposons d’abord que quatre couleurs ne suffisent pas. Il existe alors un plus petit contre-exemple : parmi toutes les cartes exigeant cinq couleurs, celle qui compte le moins de régions. Il reste à établir deux choses. Premièrement, dresser une liste de configurations locales et prouver que toute carte contient nécessairement l’une d’elles. La liste est alors dite inévitable. On le montre par une méthode appelée décharge : on attribue un nombre à chaque région en fonction de son nombre de voisines, puis on fait circuler ces nombres entre régions voisines selon des règles précises. À la fin, il reste forcément quelque part une valeur positive ; à cet endroit se trouve nécessairement l’une des configurations de la liste. Deuxièmement, montrer qu’aucune configuration de la liste ne peut appartenir à un contre-exemple minimal. Si elle s’y trouvait, on pourrait la réduire pour obtenir une carte plus petite. Par hypothèse, cette petite carte se colorie avec quatre couleurs ; lorsqu’on rétablit la partie supprimée, on peut encore arranger les couleurs comme il faut. C’est ce qu’on appelle la réductibilité. Rapprochons maintenant les deux résultats : le plus petit contre-exemple doit contenir une configuration de la liste, mais ne peut en contenir aucune. Il n’existe donc pas. La méthode de décharge, Appel et Haken l’ont héritée de Heesch.

La liste de Kempe était très courte. Il commençait par montrer que toute carte possède une région ayant au plus cinq voisines. Jusqu’à quatre voisines, ses échanges de couleurs fonctionnaient. Avec cinq, on arrivait précisément à la faille découverte par Heawood.

La suite du travail a consisté à décomposer ce cas des cinq voisines en configurations plus grandes et plus précises, dont chacune pourrait être démontrée réductible séparément. Seulement, plus on affine, plus la liste s’allonge et plus chaque vérification pèse lourd. Autour d’une configuration se trouve une couronne de régions : il faut essayer toutes les dispositions des quatre couleurs sur cette couronne pour savoir si les échanges permettent de s’en sortir. Avec quatorze régions autour, il y a près de deux cent mille dispositions à considérer ; avec dix-huit, plus de seize millions.

Voilà pourquoi Appel et Haken ne pouvaient se passer des machines. Ce n’était pas une simple envie d’en utiliser. L’ossature était en place depuis Kempe : trouver une liste courte, ou vérifier une liste longue jusqu’à la dernière entrée. En un siècle, personne n’avait trouvé la liste courte.

5. Trois raisons de douter

Le malaise de Toronto s’est ensuite précisé en trois objections. Elles ne disent pas la même chose.

La première dit : ce n’est pas une démonstration. Le philosophe Thomas Tymoczko en donne la formulation la plus célèbre en 1979. Il ne prétend pas que le théorème des quatre couleurs soit probablement faux. Il rappelle qu’une preuve remplit deux fonctions : convaincre de la vérité du résultat, et permettre de parcourir tout le raisonnement pour en comprendre le pourquoi. Il désigne cette seconde qualité par un mot qui signifie qu’on peut embrasser la preuve d’un seul regard, depuis un même point de vue. La démonstration de 1976 accomplit la première tâche et abandonne la seconde. Dès lors qu’un calcul impossible à embrasser ainsi entre dans la catégorie des preuves, c’est le sens du mot preuve que l’on a élargi.

La deuxième objection dit : c’est une démonstration, mais elle n’est pas belle. Elle ne fait pas comprendre pourquoi quatre couleurs, précisément, doivent suffire. À Toronto, bien des gens espèrent qu’un jour on trouvera une preuve courte, qui donne à voir la raison du résultat.

La troisième est la plus pratique : peut-être est-ce une démonstration, mais comment vérifier qu’elle est vraiment sans erreur ? Le programme est-il correct ? La liste complète ? Parmi les milliers de sorties, n’y en a-t-il pas une qui a été mal traitée ? Les données imprimées ont-elles été transmises sans décalage ? En 1979, DeMillo, Lipton et Perlis publient un article où ils rappellent que la solidité d’une preuve ne vient pas seulement de ses déductions formelles. Elle vient aussi de toute la vie qu’elle mène dans la communauté mathématique, lorsqu’on la critique, la simplifie, la réemploie, l’enseigne. Par où ce travail peut-il commencer quand personne n’est en mesure de tout revérifier ?

La suite de l’histoire n’a véritablement répondu qu’à la troisième objection. Dans les années 1990, Robertson, Sanders, Seymour et Thomas entreprennent de contrôler la preuve d’Appel et Haken. Ils renoncent très vite. Ils expliqueront ensuite, en substance, qu’une partie était informatisée et ne pouvait être vérifiée à la main, tandis que la partie réputée vérifiable à la main était d’une complexité et d’une minutie extraordinaires. La simple saisie des descriptions de plus d’un millier de configurations constituait déjà un chantier. Ils décident donc de tout reprendre. En 1996, ils aboutissent à une nouvelle démonstration : six cent trente-trois configurations, trente-deux règles de décharge au lieu de plusieurs centaines. Ils rendent les programmes et les données publics ; chacun peut relancer les calculs. Selon eux, vérifier la partie consacrée au caractère inévitable de la liste prendrait plusieurs mois à la main, une vingtaine de minutes par ordinateur. La machine est toujours là, mais, pour la première fois, le volet informatique devient un objet que d’autres peuvent contrôler indépendamment. En 2005, Gonthier inscrit toute cette démonstration moderne dans un système formel, à l’aide d’un logiciel appelé assistant de preuve. Un très petit noyau de programme en vérifie chaque étape. C’est la voie de 1996 qu’il contrôle, non les programmes exécutés par Appel et Haken en 1976 : à ce jour, personne n’a établi de cette façon que ces anciens programmes étaient exempts d’erreurs. La confiance ne porte plus dès lors sur des milliers de cas et un long programme spécialisé, mais sur le petit noyau, sur les définitions formelles et sur la traduction de l’énoncé initial dans ce langage. Elle n’a pas disparu. Elle s’est resserrée, concentrée en quelques endroits où d’autres peuvent venir refaire le contrôle.

La deuxième objection reste sans réponse. En mars 2026, six auteurs proposent dans une prépublication une nouvelle démonstration et une méthode de coloration beaucoup plus rapide. Ils utilisent 8 202 configurations réductibles, dont deux cas simples. Au 1er octobre 2026, il convient de parler d’une nouvelle preuve proposée par ses auteurs. Elle n’a pas encore derrière elle une longue période de vérifications indépendantes ayant fait émerger un consensus ; cette prudence ne revient pas pour autant à la déclarer fausse. Thomassen, l’un des participants, dit que ce qu’il veut, lui, c’est une démonstration sans ordinateur. Il n’a jamais cessé d’y penser.

6. Un théorème trop grand pour un livre

Le deuxième exemple est plus vaste encore. Trop vaste pour tenir dans un livre.

Dans l’épisode précédent, nous avons rencontré cette ossature : on peut composer les éléments deux à deux, il en existe un qui ne fait rien, et chacun peut être annulé par un autre. Les mathématiciens appellent cela un groupe. On le décompose à l’aide de sous-groupes normaux et des groupes quotients correspondants. Un groupe simple n’a pas de sous-groupe normal propre non trivial ; cela ne signifie pas qu’il n’a aucun sous-groupe non trivial. Les groupes simples jouent un peu le rôle des nombres premiers : tout entier s’obtient par multiplication de nombres premiers, et tout groupe fini possède une suite de composition dont les facteurs sont des groupes simples. Mais ces facteurs ne suffisent pas à déterminer de façon unique comment le groupe d’origine est assemblé. Quels sont donc tous les groupes simples finis ?

Les plus petits sont très sobres : des cycles comptant un nombre premier d’éléments. Faites tourner un pentagone régulier d’un cinquième de tour à chaque fois. Après cinq de ces rotations, il revient à sa position initiale ; les cinq rotations distinctes ainsi obtenues forment un groupe simple. Le premier groupe simple où l’ordre des opérations compte possède soixante éléments : toutes les rotations d’un icosaèdre régulier. Dans le dixième épisode, l’équation du cinquième degré résistait à toute formule générale de résolution. Au fond de l’obstacle se trouvait précisément ce groupe simple de soixante éléments.

La réponse prend la forme d’une liste : quelques familles infinies dont les membres se succèdent selon des règles, puis vingt-six exceptions isolées qui n’appartiennent à aucune de ces familles. La plus grande sera baptisée le Monstre. Le nombre de ses éléments s’écrit avec cinquante-quatre chiffres. Fischer et Griess prédisent son existence vers 1973. Le 14 janvier 1980, à Ann Arbor, Griess annonce qu’il l’a construit : il a obtenu toutes les symétries d’un objet à cent quatre-vingt-seize mille huit cent quatre-vingt-trois dimensions. Lors de la publication, en 1982, il l’appelle le Géant amical.

Les articles avaient commencé à grandir bien avant. En 1963, Feit et Thompson démontrent que tout groupe fini d’ordre impair est résoluble ; tout groupe simple fini non commutatif est donc nécessairement d’ordre pair. Leur article compte deux cent cinquante-cinq pages et occupe à lui seul un numéro entier d’une revue. Plus tard, Gonthier et une équipe reprendront toute cette démonstration dans un assistant de preuve. Leur travail sera publié en 2013.

Montrer que la liste est complète, c’est établir le théorème de classification des groupes simples finis. La démonstration ne tient ni dans un article ni dans un livre. Elle s’étend sur des centaines d’articles, dus à une centaine d’auteurs principaux, pour un total d’environ dix mille pages. Avec les résultats préalables indispensables, l’estimation courante atteint quinze mille pages. Ces chiffres ne se calculent pas tous de la même façon : on ne sait même pas très bien où tracer les limites de cette unique démonstration.

Au début des années 1980, Daniel Gorenstein publie un livre dont le titre signifie Groupes simples finis : introduction à leur classification. Il y rassemble plus de vingt ans de travaux comme on fait le bilan d’un ensemble achevé. Pendant toutes ces années, c’est lui qui a gardé une vue d’ensemble et indiqué les directions à suivre. Plus tard, Aschbacher, l’un des acteurs les plus engagés de l’entreprise, écrira que, dans l’esprit de la communauté mathématique, la classification était généralement considérée comme terminée aux alentours de 1980.

Cet achèvement ne se réduit pas à une phrase prononcée un jour à une tribune. Un programme de recherche est devenu peu à peu un résultat reconnu. On estimait que toutes les grandes branches avaient été couvertes ; quant aux parties restantes, les spécialistes concernés savaient comment s’y prendre.

Que les experts sachent comment finir et qu’il existe déjà une démonstration complète, publiée, dont chaque étape puisse être citée, ce sont deux affirmations différentes. Le problème se loge entre les deux.

7. La pièce manquante

Dans l’arbre de la classification, une branche entière porte le nom de groupes quasi-minces. Dans le programme de première génération, elle a été confiée à Geoff Mason. En 1980, Mason annonce la classification de ces groupes. En 1981, il laisse un manuscrit d’environ huit cents pages, qui ne sera pas publié. On comprendra seulement plus tard qu’il est incomplet et présente de graves lacunes.

Cette faille n’a pas de date de découverte. Rien de comparable à Heawood désignant, en 1890, l’étape fautive de Kempe. Le constat s’impose progressivement. De la fin des années 1980 aux années 1990, à mesure que l’on réorganise les démonstrations de la classification, il devient de plus en plus difficile de traiter cette partie comme un dossier clos. Un travail que tout le monde croyait fini depuis longtemps ne l’était pas réellement.

Aschbacher et Stephen Smith comblent la lacune. En 2004, ils publient les deux volumes de La Classification des groupes quasi-minces, environ mille deux cent vingt pages au total. Il ne s’agit pas d’ajouter une page d’errata. Il faut un nouveau livre. Quelques omissions moins importantes seront encore découvertes par la suite, puis corrigées à leur tour.

Trois faits peuvent donc être affirmés. Dès le début des années 1980, la communauté mathématique a accepté la liste comme correcte. Une partie considérable demeurait pourtant inachevée dans les textes publics de la première génération de démonstrations. Les deux volumes de 2004 en ont fourni un traitement complet et publiable.

Gorenstein a compris très tôt que, même correcte, la première démonstration ne constituait pas une forme finale satisfaisante. Avec Richard Lyons et Ronald Solomon, il lance un programme de deuxième génération : réécrire les preuves dispersées dans des centaines d’articles sous la forme d’une série de monographies ordonnées, aussi autonomes que possible, où les dépendances entre les résultats seraient explicites. Gorenstein meurt en août 1992. Le premier volume ne paraît qu’en 1994. L’éditeur présente comme objectif une démonstration soigneuse et largement autosuffisante. Le dixième volume paraît en 2023 ; la réécriture se poursuit depuis, et le nombre exact de volumes comme le total des pages doivent être actualisés à partir des parutions effectives. Lyons et Solomon travaillent sur les dernières parties de la démonstration principale ; en Allemagne, Stroth a lui aussi un volumineux manuscrit consacré au dernier tronçon. L’estimation initiale de douze volumes et cinq mille pages paraît désormais très serrée.

Quelqu’un a-t-il lu ligne à ligne, du début à la fin, toute la démonstration de première génération, avec l’ensemble des résultats dont elle dépend ? On ne trouve personne qui l’affirme. Aschbacher, Lyons, Solomon ont une maîtrise extraordinaire de l’architecture générale, et chaque région a ses spécialistes. Mais connaître cette architecture et contrôler page après page plusieurs centaines d’articles ne sont pas des travaux du même ordre de grandeur.

Dans la pratique, les mathématiciens ne cherchent pas un lecteur surhumain. Les spécialistes de chaque domaine répondent de leur partie. Les articles font continuellement appel les uns aux autres ; ces réemplois sont autant d’occasions de vérifier à nouveau, sans pour autant garantir que chaque citation s’accompagne d’une relecture ligne à ligne. Lorsqu’une lacune importante apparaît, on réécrit. Les synthèses et les monographies de deuxième génération servent enfin à remplacer, autant que possible, la question de savoir qui fait confiance à qui par celle de savoir quel résultat dépend de quel autre. Qu’un théorème soit connu n’implique pas qu’une personne en connaisse tous les détails.

8. Trois façons d’en avoir fini

Il reste un troisième exemple. En 1611, Kepler offre à son protecteur, pour le Nouvel An, un petit livre sur les flocons de neige hexagonaux. Il y glisse une conjecture : les oranges empilées en pyramide, couche après couche, sur l’étal du marchand de fruits occupent l’espace aussi densément qu’il est possible. À l’origine, il s’agit de boulets de canon. Walter Raleigh a demandé à son assistant Harriot de trouver un moyen d’en compter un tas ; Harriot correspond avec Kepler à partir de 1606. En 1900, Hilbert fait entrer la question dans le dix-huitième problème de sa célèbre liste. En 1998, Thomas Hales annonce l’avoir démontrée. Sa preuve repose pour moitié sur des raisonnements traditionnels, pour moitié sur la vérification d’une masse d’inégalités, la programmation linéaire et des énumérations finies. Son étudiant Samuel Ferguson a apporté une contribution majeure à une partie décisive.

Les Annals of Mathematics réunissent une douzaine de rapporteurs, qui travaillent pendant environ quatre ans. En 2003, Fejes Tóth, leur coordinateur, déclare qu’ils sont certains à 99 % de la correction de la preuve, mais ne peuvent certifier l’ensemble des calculs. Le chiffre sera repris à l’infini. Il met un nombre sur une réalité que l’évaluation par les pairs laisse d’ordinaire tacite : relire un article n’a jamais été actionner un interrupteur à deux positions, vrai ou faux. En 2005, les Annals publient l’argumentation principale, des pages 1065 à 1185, soit cent vingt et une pages. Les ressources de calcul et les articles relatifs aux calculs sont mis à disposition ou publiés séparément.

Hales ne s’arrête pas là. Il lance un projet visant à transcrire la preuve entière dans un système formel, pour que le petit noyau d’une machine la contrôle et qu’aucun rapporteur n’ait plus à faire confiance aux calculs. Le 10 août 2014, le projet annonce qu’il est arrivé au bout, à l’aide de deux assistants de preuve. La démonstration formelle paraît en 2017, signée par vingt-deux auteurs.

Un même théorème, trois dates, trois sens du mot terminé. En 1998, l’auteur estime avoir fini. En 2005, la revue juge le résultat assez fiable pour le publier. En 2014, un noyau formel a achevé la vérification.

C’est la quatrième fois que cette série rencontre ce genre de question. Dans le troisième épisode, nous demandions si ce livre marquait le début de l’axiomatisation ; dans le cinquième, si ces commentaires étaient des démonstrations ; dans le neuvième, si ces séries relevaient déjà du calcul infinitésimal. Les trois premières fois, il s’agissait de savoir quel nom donner à quelque chose, et c’étaient les générations suivantes qui posaient la question rétrospectivement. Ici, l’objet est présent et son nom ne fait aucun doute. La question est de savoir s’il peut être tenu pour connu. Et ceux qui la posent sont ses contemporains : à la sortie de la conférence de Toronto, en 1976, les mathématiciens expriment déjà leur malaise. Trois ans plus tard, Tymoczko lui donne la forme d’un problème.

L’autre voix n’a jamais manqué non plus. En 1980, Krakowski répond à Tymoczko que toute preuve formelle de longueur finie peut, en principe, être embrassée dans son ensemble : les humains n’ont qu’à apprendre à vivre un peu plus longtemps. C’est une ironie, mais elle porte un argument solide. Les mathématiques n’ont jamais exigé que tous les préalables d’une démonstration tiennent simultanément dans une seule tête. Un article de vingt pages peut faire appel à des théorèmes disséminés dans des milliers de pages de livres ; personne n’en conclut que ces vingt pages ne sont pas une preuve. En 1994, Thurston écrit que les mathématiciens cherchent des moyens de faire comprendre les mathématiques, de permettre qu’on les pense. Vue ainsi, une démonstration doit non seulement garantir la vérité du résultat, mais aussi mettre quelque chose entre les mains de ceux qui la reçoivent. Le problème des grandes preuves n’est pas que personne ne possède le tout : dans les mathématiques ordinaires non plus, personne ne possède le tout. C’est que la chaîne de confiance s’allonge beaucoup. Une bonne réponse consiste à rendre chaque maillon aussi petit que possible, pour que le contrôle puisse plus facilement passer d’une personne à une autre.

Ce qui a réellement changé depuis 1976 n’est donc pas que les mathématiques seraient passées des hommes aux machines. Pour la première fois à grande échelle, trois choses auparavant liées se sont séparées : la validité d’un raisonnement, ce qu’il donne à comprendre et la possibilité effective de le vérifier. Les quatre couleurs ont porté les calculs au-delà du champ de vision d’une personne ; la classification a fait de même avec les textes et les savoirs spécialisés. La formalisation tente de rassembler tout cela dans un objet qu’une machine puisse contrôler pas à pas. Elle répond à une grande part de la question de la confiance. L’autre part demeure : lorsqu’une communauté mathématique sait de façon fiable qu’une chose est vraie, a-t-elle pour autant compris pourquoi elle l’est ?

Ce qu’une personne ne peut saisir tout entier peut se partager en parties dont chacune sera à la portée de quelqu’un.

En 1977, trois jeunes chercheurs du MIT rendent publique une méthode de chiffrement fondée sur une difficulté mathématique : multiplier deux grands nombres premiers est facile ; retrouver ces nombres à partir du produit est difficile. Cinq ans plus tard, cette méthode a son entreprise. La sixième année, elle a son brevet.

On continue de compter. Ce qui compte comme mathématiques, en revanche, n’a jamais été définitivement tranché.

Sources et lectures complémentaires

Les références ci-dessous éclairent les détails historiques et les divergences d’interprétation évoqués dans le texte. Les notices de collections, les textes anciens et les reconstitutions modernes ne constituent pas des preuves de même nature.

• Prépublication de 2026 sur les quatre couleurs et la coloration en temps quasi linéaire
• Robertson, Sanders, Seymour et Thomas : annonce de la nouvelle preuve en 1996
• Gonthier : la preuve formelle du théorème des quatre couleurs
• Une preuve du théorème de l’ordre impair vérifiée par machine
• La Classification des groupes quasi-minces
• Hales : la preuve de la conjecture de Kepler publiée dans les Annals
• Une preuve formelle de la conjecture de Kepler, 2017