Quand les machines ont piqué la matemática aux mathématiciens

Imaginez la scène : on est en 1976. Deux mathématiciens, Kenneth Appel et Wolfgang Haken, viennent de résoudre un des problèmes les plus anciens des mathématiques — le théorème des quatre couleurs. La question paraît simple : peut-on colorier n'importe quelle carte avec seulement quatre couleurs, sans que deux régions voisines partagent la même teinte ?

L'affaire semble rondement menée. Comme un truc qu'on ferait avec des crayons de couleur et un cahier de coloriage.

Sauf que ce problème embêtait le monde entier depuis plus d'un siècle.

Le twist : l'ordinateur a fait le travail

Et là, ça devient intéressant. Appel et Haken n'ont pas résolu ce puzzle à l'ancienne — avec des équations élégantes et des raisonnements brillants. Ils ont demandé à un ordinateur de tester toutes les configurations possibles. Méthodiquement. Sans relâche.

Le programme a tourné pendant 1 200 heures. Dix milliards de décisions. Dix. Milliards.

Ce n'est pas vraiment une preuve au sens traditionnel. C'est plutôt comme si vous aviez un stage très très motivé chargé de vérifier absolument toutes les cartes possibles jusqu'à trouver la réponse.

Un programmeur nommé John Koch les a aidés sur la partie algorithmique. Le système est devenu si sophistiqué qu'Appel et Haken ont eux-mêmes admis afterward que le programme "commençait à nous apprendre des choses sur la démarche que nous n'avions jamais anticipées." La machine avait, d'une certaine manière, dépassé ses créateurs.

Vous imaginez la tête du milieu.

Les mathématiciens voient rouge

Parce que les mathématiciens, soyons honnêtes, c'est une caste particulière. Ils sont fans d'élégance. De beauté pure. De ce frisson intellectuel quand une preuve vous fait dire "Ah ouais, quand même" une fois que vous la comprenez.

Et là, on leur dit qu'un ordinateur a coché des cases pour arriver à l'un des résultats les plus convoités des mathématiques ?

Disons qu'ils n'ont PAS apprécié.

Herbert Wilf, de l'université de Pennsylvanie, avait visiblement des opinions bien arrêtées sur l'ordre divin des mathématiques : "Dieu ne permettrait pas qu'on prouve un théorème par une méthode aussi terrible !"

Paul Halmos, de l'UC Santa Barbara, était tellement contrarié qu'il demandait carrément la suppression du concept : "cette preuve s'appuie en réalité sur un Oracle, et je dis : à bas les Oracles ! Ce n'est pas des mathématiques ça."

Frank Bonsall, d'Édimbourg, estimait que les preuves assistées par ordinateur "n'ont tout simplement pas leur place dans la science mathématique."

Et mon préféré, George Spencer-Brown de Cambridge : il a décrit ça comme "le cas le plus ridicule des 'Vêtements neufs de l'empereur' qui ait jamais déshonoré l'histoire des mathématiques."

Ce ne sont pas les réactions de gens qui prennent calmement connaissance d'une information nouvelle.

La skepticisme à son paroxysme

Un directeur de département de mathématiques était tellement hostile à cette preuve qu'il refusait de laisser ses doctorants rencontrer Appel et Haken. Son raisonnement ? Il prétendait que la preuve计算机 avait enlevé toute incitation à chercher une démonstration "convenable", donc qu'aucun mathématicien de premier ordre ne travaillerait jamais sur ce problème.

C'est comme refuser d'apprendre l'existence de la pénicilline parce qu'Alexander Fleming ne l'a pas découverte de la "bonne" façon.

Mais voilà ce qui me frappe le plus. Après qu'un fils Haken ait présenté la preuve (il avait aidé son père), le auditoire se serait divisé en deux groupes très révélateurs :

• Les plus de 40 ans : impossibles à convaincre que la preuve计算机 était correcte
• Les moins de 40 ans : impossibles à convaincre que 700 pages de calculs à la main pouvaient être correctes

N'est-ce pas fascinant ? La jeune génération voyait cette masse de calculs manuels et se disait "ouais, non, les ordinateurs semblent plus fiables que des centaines de pages d'erreurs humaines potentielles." La génération plus âgée voyait l'ordinateur et se disait "si je ne peux pas le vérifier moi-même, ça ne compte pas."

De la brocante générationnelle en maths. J'adore.

Tout le monde n'était pas furieux

Évidemment, tout le monde n'était pas prêt à brûler l'ordinateur.

Le légendaire mathématicien Bill Tutte — qui avait pourtant douté publiquement de la méthode — a fini par accepter la preuve et a célébré ça avec un poème :

Wolfgang Haken Frappa le Kraken Un ! Deux ! Trois ! Quatre ! Dit-il : "Le monstre n'est plus."

On va pas se mentir, c'est magnifique.

Heinrich Heesch, mathématicien allemand, l'a acceptée alors qu'il avait passé quarante ans à travailler sur les méthodes algorithmiques elles-mêmes qu'Appel et Haken utilisaient. Ça doit faire un peu mal — consacrer sa carrière à développer les outils qu'un autre utilise pour vous devancer.

Le drama du New York Times

Voici un petit morceau d'absurdité bureaucratique : le NYT a refusé de couvrir l'exploit au départ, craignant que ce soit un faux espoir. Quand ils ont fini par décider que c'était légitime des mois plus tard, ils ont soutenu que ce n'était plus une actualité.

Le journal de référence n'a finalement publié l'histoire que grâce à une tribune de Lipman Bers, président de la Société Mathématique Américaine — qui leur a en quelque sorte forcé la main.

Imaginez être comme : "On a résolu l'un des plus grands problèmes mathématiques !" Et eux : "Nan, on passe. Rappellez-nous dans quelques mois."

La vraie question : c'est quoi une preuve ?

Toute cette controverse touche à quelque chose de profondément philosophique. Qu'est-ce que ça veut dire prouver quelque chose en mathématiques ?

Pendant la majeure partie de l'histoire, une preuve signifiait que vous pouviez suivre le raisonnement étape par étape, comprendre chaque saut logique, et le vérifier avec votre propre cerveau. Une preuve se devait d'être lisible par un humain.

Mais la preuve du théorème des quatre couleurs ? Aucun humain ne pouvait la vérifier complètement. Trop vaste. Trop computationnelle. Il fallait faire confiance à la machine.

Le philosophe Thomas Tymoczko a soulevé ce point en 1979, arguant qu'une preuve "insurveillable" — trop grande pour qu'un humain la vérifie vraiment — n'était pas vraiment une preuve au sens traditionnel. Il ne disait pas que les maths étaient fausses ; il se demandait si "correct" et "prouvé" sont vraiment la même chose quand ce sont des machines qui font le travail.

C'est une question genuinely intéressante. Et on la reprend encore aujourd'hui quand quelqu'un utilise l'IA pour découvrir ou vérifier quelque chose de trop complexe pour des cerveaux humains.

L'héritage

Voici le truc avec le théorème des quatre couleurs : il n'a jamais été prouvé "élégamment." Le mieux qu'on ait, c'est toujours une version de cette approche计算机isée. En 1997, Neil Robertson, Daniel Sanders, Paul Seymour et Robin Thomas ont trouvé une méthode de vérification plus efficace, mais qui nécessitait toujours un ordinateur.

Peut-être que ce directeur de département avait raison sur le fait qu'aucun mathématicien de premier ordre ne travaillerait sur une preuve plus belle — parce qu'elle n'existe pas. L'ordinateur l'a vraiment résolu de la seule façon possible.

La controverse s'est largement calmée. Les preuves assistées par ordinateur sont maintenant une partie respectée (si parfois encore débattue) des mathématiques. On a des preuves qu'aucun humain ne pourrait jamais vérifier entièrement, et on a mostly fait la paix avec ça.

Mais je persiste à adorer ce moment où les professionnels les plus guindés des mathématiques ont complètement perdu leur sang-froid face à l'idée qu'une machine pouvait être meilleure qu'eux en maths.

Il s'avère que l'avenir des mathématiques, c'était un programme informatique de 1 200 heures et un poème sur le slay d'un monstre marin.