Résolu par ordinateur : les célèbres problèmes mathématiques que les machines ont aidé à résoudre (1976–2026)

En 1976, deux mathématiciens de l'Illinois ont annoncé avoir prouvé que quatre couleurs suffisent pour colorier n'importe quelle carte, et qu'une partie de leur démonstration ne pouvait être vérifiée que par un ordinateur. Beaucoup de mathématiciens étaient profondément mal à l'aise : est-ce vraiment une démonstration si aucun humain ne peut la lire en entier ? Cinquante ans plus tard, la question s'est inversée. En 2026, des systèmes d'IA ont trouvé les idées clés de résultats que des experts n'avaient pas trouvées pendant des décennies. Cet article raconte cette histoire dans l'ordre et, pour chaque problème célèbre, dit exactement ce que la machine a fait, car « résolu par ordinateur » peut vouloir dire des choses très différentes.

1976 : quatre couleurs, et une démonstration que personne ne pouvait lire

Tronc commun GCSE

La question est assez simple pour l'école primaire : colorier une carte de sorte que deux pays voisins n'aient jamais la même couleur. Combien de couleurs peut-il falloir ? Francis Guthrie a deviné quatre en 1852. On voit facilement qu'il peut en falloir quatre (regardez l'image ci-dessous), mais prouver que quatre suffisent toujours, pour toute carte possible, a résisté aux mathématiciens pendant 124 ans.

Kenneth Appel et Wolfgang Haken ont trouvé comment montrer que toute carte demandant cinq couleurs devrait contenir l'un de près de deux mille motifs particuliers, et que chacun de ces motifs peut être « réduit ». Les vérifier tous à la main était impossible : un ordinateur l'a fait, avec plus d'un millier d'heures de calcul. Le théorème était démontré, mais d'une manière qui a changé ce que « démonstration » voulait dire en pratique.

Comment le doute a été levé : une démonstration informatique plus courte a suivi en 1996, et en 2005 Georges Gonthier et Benjamin Werner ont vérifié tout l'argument dans l'assistant de preuve Coq. C'est aujourd'hui l'un des théorèmes les plus soigneusement vérifiés des mathématiques.

1996 : la première démonstration trouvée seule par un ordinateur

Approfondissement licence

La conjecture de Robbins demandait si trois règles courtes décrivent exactement la même algèbre que l'algèbre de Boole, la logique vrai/faux à l'intérieur de chaque puce informatique. Les meilleurs logiciens, dont Alfred Tarski, n'avaient pas réussi à la trancher en soixante ans. En 1996, le démonstrateur automatique EQP de William McCune a exploré des enchaînements de raisonnements possibles pendant environ huit jours et a trouvé une démonstration. C'était d'une autre nature qu'en 1976 : personne n'avait dit à l'ordinateur à quoi l'argument devait ressembler.

1998–2014 : les oranges de Kepler

En 1611, Johannes Kepler affirma que la façon dont les marchands empilent les oranges (chaque couche posée dans les creux de la précédente) est l'empilement le plus dense possible de sphères égales. Il remplit environ 74 % de l'espace (exactement π/√18).

Thomas Hales, avec Samuel Ferguson, a transformé la question en des milliers de problèmes d'optimisation résolus par ordinateur, et a annoncé une démonstration en 1998. Les relecteurs de la revue se sont dits « sûrs à 99 % » qu'elle était juste, sans pouvoir vérifier chaque calcul. Hales a répondu en dirigeant le projet Flyspeck pour tout revérifier dans un logiciel d'assistant de preuve ; il s'est achevé en 2014.

2016 : la démonstration de 200 téraoctets

Tronc commun GCSE

Voici un casse-tête à essayer. Coloriez chaque nombre entier en rouge ou en bleu. Pouvez-vous le faire sans qu'aucun triplet pythagoricien (trois nombres avec a² + b² = c², comme 3, 4, 5) soit d'une seule couleur ?

Ronald Graham offrait 100 dollars pour la réponse. En 2016, Marijn Heule, Oliver Kullmann et Victor Marek ont utilisé un solveur SAT (un logiciel qui résout d'énormes casse-têtes logiques vrai/faux) sur le superordinateur Stampede pendant environ deux jours. La réponse : tous les nombres de 1 à 7 824 peuvent être coloriés sans problème, mais pas de 1 à 7 825. La preuve qu'aucun coloriage de 7 825 nombres ne marche faisait 200 téraoctets, présentée par Nature comme la plus grande preuve mathématique jamais réalisée à l'époque. La même technique a tranché en 2019 la conjecture de Keller sur le pavage de l'espace par des cubes en dimension sept.

2025–2026 : l'IA commence à trouver les idées

Approfondissement master

Tout ce qui précède utilisait l'ordinateur pour vérifier, ou pour chercher dans un cadre conçu par des humains. À partir de 2025, des systèmes fondés sur de grands modèles de langage ont commencé à proposer eux-mêmes les idées mathématiques, en les associant à l'assistant de preuve Lean, afin que le résultat puisse être vérifié par machine plutôt que simplement cru.

La conjecture des distances unité (mai 2026). En 1946, Paul Erdős a demandé : si l'on place n points sur une surface plane, combien de paires peuvent être exactement à distance 1 ? Il pensait que ce nombre croît à peine plus vite que n. Un modèle interne d'OpenAI a trouvé une famille infinie d'ensembles de points qui fait mieux d'une vraie puissance de n, avec des outils profonds de théorie algébrique des nombres. Neuf mathématiciens de premier plan, dont les médaillés Fields Tim Gowers et Jacob Tsimerman, l'ont vérifiée et ont écrit un article d'accompagnement, et Will Sawin a rendu le gain explicite. Gil Kalai a comparé son importance à la démonstration des quatre couleurs de 1976.

AlphaProof Nexus (mai 2026). Google DeepMind a lancé son agent, qui associe le modèle Gemini à Lean, sur 353 problèmes ouverts de la base de problèmes d'Erdős. Il en a résolu 9, dont deux ouverts depuis 56 ans, et a démontré 44 conjectures de l'Encyclopédie en ligne des suites d'entiers (OEIS). Chaque démonstration compile dans Lean. Notez toutefois le taux de réussite : environ 2,5 %.

Astra (août 2026). OpenAI a annoncé dix résultats de son prochain modèle, non publié, dont la première construction d'un groupe non sofique (répondant à une question posée par Mikhail Gromov en 1999), trois problèmes d'Erdős et la première amélioration depuis 1978 d'une borne générale sur l'empilement de sphères. Chacun était accompagné d'un certificat Lean. Un audit humain indépendant n'a trouvé aucune erreur substantielle confirmée dans les résultats principaux, même si l'un d'eux a fait l'objet d'une demande de révision majeure par un spécialiste, et la relecture par une revue n'était pas terminée au moment de la rédaction.

Cinquante ans en une chronologie

Ce que cela signifie si vous apprenez les maths

Chaque résultat de cet article dépendait encore d'humains : quelqu'un devait énoncer le problème avec précision, décider quelle approche valait la peine d'être lancée, vérifier que le théorème prouvé par l'ordinateur était bien celui qui comptait, et expliquer pourquoi il est vrai. C'est exactement la compétence que construisent les maths à l'école quand elles demandent de montrer son raisonnement, et c'est le thème de notre article L'IA sait-elle vraiment faire des maths ?. Pour les problèmes encore ouverts, et une liste fiche par fiche de ces problèmes résolus, consultez notre centre Mystères mathématiques non résolus.