L’essentiel
- OpenAI affirme que son modèle GPT-5.6 Sol Ultra a démontré seul une conjecture de théorie des graphes restée ouverte depuis les années 1970.
- Le mathématicien Thomas Bloom, de l’université de Manchester, salue une preuve « courte et élémentaire », qui aurait pu être trouvée dès les années 1980.
- Il reproche au papier de ne mentionner aucun travail antérieur, notamment un article de 1983 dont la démonstration semble largement s’inspirer.
En moins d’une heure, un modèle d’OpenAI a bouclé une démonstration restée hors de portée des mathématiciens pendant près d’un demi-siècle. L’exploit tient d’abord au chronomètre : une machine qui règle en quelques dizaines de minutes ce qui avait résisté à des générations de chercheurs.
Le plus troublant se trouve pourtant ailleurs. Cette preuve, aussi élégante soit-elle, ne cite aucune source : pas une référence, pas une filiation. Pour une démonstration mathématique, l’oubli n’a rien d’anodin.
Un blocage d’un demi-siècle, levé sans effort apparent
La conjecture en question relève de la théorie des graphes, cette branche qui étudie les réseaux de sommets reliés par des arêtes. La question était simple à énoncer : peut-on toujours trouver, dans n’importe quel réseau, un ensemble de cycles qui parcourt chaque arête exactement deux fois ? Formulé indépendamment par plusieurs mathématiciens dans les années 1970, le problème avait résisté à toutes les preuves générales, malgré une longue série de résultats partiels.
Selon OpenAI, la démonstration provient entièrement de GPT-5.6 Sol Ultra, le papier lui-même ayant été rédigé par le modèle GPT-5.6 Sol. Thomas Bloom, mathématicien à l’université de Manchester, y voit « une très jolie preuve », qu’il décrit comme « courte, élémentaire, et qui aurait pu être découverte dans les années 1980 ». Aucune théorie nouvelle n’est requise : le modèle combine astucieusement des outils déjà connus. Son évaluation reste à ce jour l’analyse publique la plus détaillée ; une vérification complète par la communauté scientifique est encore en cours.
Pourquoi, alors, aucun humain n’y était parvenu ? Bloom avance une hypothèse presque psychologique. L’étape clé reposerait sur un détour contre-intuitif dans le raisonnement. Un mathématicien humain aurait essayé l’approche évidente, l’aurait vue échouer, et serait passé à autre chose en se disant que le problème résistait. La machine, elle, ne se décourage pas : elle enchaîne les petites variations jusqu’à ce que l’une fonctionne.
Une preuve élégante, mais amnésique
L’éloge s’arrête pourtant là. Bloom fait remarquer que les idées mathématiques au cœur de cette preuve remontent au moins à un article de 1983, signé Bermond, Jackson et Jaeger. Or le papier d’OpenAI n’en dit pas un mot. Si bien qu’à lire cette seule démonstration, on pourrait croire que le modèle a inventé de toutes pièces la stratégie sous-jacente.
« Je suppose que ces travaux antérieurs ont fortement influencé la preuve d’OpenAI, et il est dommage qu’elle ne les mentionne pas du tout », écrit le chercheur. Pour lui, ce n’est pas un accident isolé : « C’est un problème fréquent avec les preuves et articles générés par IA : ils utilisent des idées et des stratégies tirées de la littérature sans les citer correctement. » Bloom doute même que le système ait trouvé la solution par lui-même, « étant donné que son premier réflexe face à un problème consiste généralement à chercher et lire tous les papiers qui s’y rapportent ».
La nuance est décisive. Un modèle qui commence par ingérer la littérature existante, puis en recombine les pièces, ne produit pas exactement du neuf. Il fait remonter du connu, oublié ou dispersé, sans en garder la trace. La rapidité impressionne ; l’effacement de la généalogie intellectuelle, lui, inquiète.
Création ou réassemblage, le doute que cette preuve ravive
Le débat n’est pas nouveau, et il dépasse largement les mathématiques. Les modèles de raisonnement se contentent-ils de retrouver un savoir existant pour le réassembler, ou fabriquent-ils quelque chose d’authentiquement inédit par un travail créatif ? Sur cette preuve précise, Bloom penche clairement pour la première hypothèse.
Il rapproche d’ailleurs ce résultat d’une autre conjecture, celle des distances unités, qu’OpenAI a également résolue récemment. Deux grands problèmes ouverts « qui se sont révélés bien plus faciles que prévu : aucune grande théorie nouvelle n’était nécessaire ». Sa lecture est lucide : l’IA excelle sur les conjectures « dont la solution ne demande que de la théorie existante, bien développée, plus beaucoup de patience et de conviction ». Mais il ajoute aussitôt que cela ne concerne « probablement qu’une petite partie des problèmes ouverts, et nous ne savons pas d’avance lesquels ».
Autrement dit, la machine démontre ici moins sa supériorité que la marge d’inachevé laissée par l’impatience humaine. Elle exhume des preuves qui étaient à notre portée depuis des décennies, faute d’avoir insisté.
Sans traçabilité, une preuve reste invérifiable
Le problème déborde vite du champ des mathématiques. Une démonstration sans citations n’est pas seulement discourtoise envers ses prédécesseurs : elle est plus difficile à vérifier. Impossible de la rattacher à un corpus, de comparer l’approche, de tracer d’où vient chaque brique du raisonnement. On se retrouve face à un bloc opaque qu’il faut auditer intégralement, plutôt qu’à un maillon inscrit dans une chaîne connue. L’alternative existe pourtant : le système AlphaProof de Google DeepMind rédige ses démonstrations en Lean, un langage formel où chaque étape est validée par la machine, ce qui rend la vérification automatique plutôt que manuelle.
Transposez cela au code généré, aux synthèses documentaires, aux rapports produits par vos agents. Un système qui puise dans un savoir existant sans jamais indiquer sa provenance vous prive de l’outil de contrôle le plus élémentaire : la vérification par recoupement des sources. La vitesse d’exécution ne compense pas cette perte, elle l’aggrave, en multipliant les productions qu’on ne peut plus remonter à leur origine.
La performance de GPT-5.6 Sol Ultra est réelle et mérite d’être saluée. Mais l’histoire retiendra peut-être moins l’heure gagnée sur cinquante ans de blocage que cette question laissée en suspens : à quoi bon une preuve si l’on ne peut pas dire d’où elle vient ?
Mon avis
Une citation, en mathématiques, fait bien plus qu’honorer les prédécesseurs : c’est le mécanisme de contrôle qui rend une preuve auditable. En le supprimant, ces modèles transforment chaque résultat en boîte noire qu’il faut valider à la main, ce qui annule une partie du temps qu’ils prétendent nous faire gagner. Je ne crois pas au récit d’une IA « créative » qui inventerait ces démonstrations : elle fait remonter, très vite, un savoir déjà écrit. Le chantier des prochains mois n’est pas de prouver davantage de conjectures : il est d’exiger que ces systèmes montrent leur généalogie, ligne par ligne. Sans quoi nous accumulerons des vérités que plus personne ne saura vérifier.
