UNE IA RÉSOUT UNE ÉNIGME DE COLORIAGE

Prenez un réseau de points reliés par des traits — ce que les mathématiciens appellent un graphe. Coloriez maintenant les points de façon que deux points reliés par un trait n’aient jamais la même couleur. Le plus petit nombre de couleurs qui marche est le nombre chromatique du graphe. Un cas célèbre est le théorème des quatre couleurs, démontré en 1977, dont le titre dit tout : « Every planar map is four colorable » (toute carte plane se colorie avec quatre couleurs).

Le pari de Hadwiger en 1943

En 1943, Hadwiger a proposé une règle valable pour tous les graphes. Réduisez un graphe en supprimant des points ou des traits, et en fusionnant deux points reliés en un seul. Le résultat s’appelle un mineur. Hadwiger regardait le plus grand graphe complet — un amas où chaque point est relié à tous les autres — que l’on peut obtenir ainsi, et conjecturait que le nombre de couleurs nécessaires ne dépasse jamais la taille de cet amas.

L’article la présente comme « parmi les problèmes les plus anciens et les plus fondamentaux de la théorie des graphes ». Elle n’est démontrée que pour les petits cas : jusqu’à des amas de cinq points, où elle équivaut au théorème des quatre couleurs ou s’y ramène. À partir de six, elle reste ouverte.

S’approcher, un logarithme à la fois

Faute de pouvoir démontrer l’énoncé exact, les chercheurs ont tenté de borner le nombre de couleurs par une fonction de la taille de l’amas, qui croisse le plus lentement possible. L’article retrace les progrès. Pendant des décennies, la meilleure borne croissait un peu plus vite que proportionnellement — d’un facteur faisant intervenir la racine carrée d’un logarithme. Il y a quelques années, Norin, Postle et Song ont franchi cette barrière. Delcourt et Postle l’ont encore améliorée et, surtout, ont montré qu’il suffit de traiter des graphes assez petits. Liu et Luo ont ramené le facteur supplémentaire à un triple logarithme.

L’aboutissement naturel est la conjecture de Hadwiger linéaire : un multiple fixe de la taille de l’amas suffit toujours. C’est ce que Sergey Norin, de l’université McGill à Montréal, et Raphael Steiner, de l’ETH Zurich, affirment désormais démontrer.

Le rôle de la machine

Les auteurs sont explicites : la preuve a été trouvée par GPT-6 Astra, un modèle d’OpenAI, en suivant leurs directions. Ils lui ont d’abord demandé de traiter le cas des graphes très denses, qu’ils pensaient être la pièce manquante. Il a réussi, écrivent-ils, « après seulement quelques heures et quelques encouragements ». Prié de rendre explicite une dépendance, il a couvert les graphes jusqu’à une certaine taille — sans atteindre tout à fait la plage nécessaire. Ils lui ont alors demandé une idée originale pour combler l’écart, ce qui a donné l’étape de « bootstrap » de la preuve finale. Presque aucune de leurs propres idées de preuve n’a survécu, disent-ils, à part une suggestion sur les contractions.

La rédaction est humaine. Un autre modèle d’OpenAI a aidé à la relecture et à la bibliographie. Les auteurs indiquent que Codex, d’OpenAI, a produit une version formelle, vérifiable par ordinateur, de toute la preuve dans l’assistant de preuve Lean, publiée en ligne avec un premier brouillon écrit par l’IA. Ils assument l’entière responsabilité des mathématiques.

Dans la preuve

L’argument a deux moitiés :

1. Petits graphes, peu de couleurs. Pour les graphes à peine plus grands que la limite de l’amas, les auteurs montrent qu’environ quatre fois la taille de l’amas suffit. Le point de départ est un résultat de Reed et Seymour de 1998 : une forme assouplie, « fractionnaire », du coloriage obéit déjà à la règle linéaire avec un facteur deux. Le nouveau travail transforme des coloriages fractionnaires en vrais coloriages, en ajoutant quelques traits au graphe et en trouvant d’immenses appariements dans une structure auxiliaire.
2. Un bootstrap. Un second argument étend la plage de tailles de graphes couverte d’un facteur quatre tiers dans l’exposant à chaque étape, au prix d’une constante plus grande. Dix étapes font passer la plage d’un tiers à environ 5,92, au-delà du seuil de 5 exigé par la réduction de Delcourt et Postle. Cette moitié utilise une vieille astuce due à Gyárfás, qui n’avait jamais été appliquée à ce problème selon les auteurs.

Les auteurs décrivent une preuve faite d’outils connus — « contenue dans l’enveloppe convexe des résultats existants », mais pas sur un bord évident de celle-ci.

Ce qui reste ouvert

La constante est gigantesque : une estimation grossière donne environ 10¹⁰⁰. Les auteurs voient de la marge pour descendre sous 10¹⁰, mais pensent qu’atteindre, disons, 100 demanderait des idées nouvelles. La conjecture exacte de Hadwiger n’est pas touchée : « Nous sommes indécis », écrivent-ils. L’article est une prépublication ; 41 pages de mathématiques nouvelles vont maintenant passer au crible d’autres spécialistes.