OpenAI a dévoilé le 26 octobre, en une seule fois, trois résultats de recherche produits par ses modèles d'IA, relevant de l'informatique théorique, de l'analyse harmonique et de la physique mathématique. Le plus lourd est une preuve que l'hypothèse du temps exponentiel (ETH) est fausse. L'entreprise n'a pas précisé quel modèle a été utilisé ; elle parle seulement de « modèles d'IA d'OpenAI » et indique que les trois résultats doivent encore être confirmés de façon indépendante par la communauté scientifique.
ETH : le socle de centaines d'articles
L'hypothèse du temps exponentiel porte sur la difficulté de calcul du problème de satisfaisabilité des formules booléennes (3-SAT) : en gros, elle affirme que ce type de problème ne peut pas être résolu en temps sous-exponentiel. Elle est plus forte que « P différent de NP » et aussi plus pratique. Depuis des décennies, elle sert de prémisse par défaut, et les bornes inférieures de centaines d'articles en théorie des graphes, biologie computationnelle, bases de données et géométrie algorithmique reposent sur elle.
Selon le calendrier publié par OpenAI, le modèle a généré la preuve en langage naturel le 16 octobre et achevé la formalisation en Lean le lendemain. La collaboration associait Russell Impagliazzo et Ramamohan Paturi, de l'Université de Californie à San Diego, ainsi que Ryan Williams, du Massachusetts Institute of Technology (MIT). Les deux premiers font justement partie des auteurs de l'ETH.
D'après les informations divulguées, les chercheurs ont posé deux conditions à OpenAI : rendre publiques toutes les données brutes et financer une conférence scientifique consacrée à l'impact de ce résultat sur l'informatique. OpenAI a accepté les deux. Si la preuve résiste à l'examen, les articles qui prennent l'ETH pour prémisse devront être réévalués un par un : déterminer quelles conclusions perdent seulement leur condition et lesquelles peuvent être sauvées par d'autres hypothèses représente un chantier considérable.
Conjecture de Kakeya : une piste familière aux lecteurs chinois
Le deuxième résultat est la preuve de la conjecture de lissage local en toutes dimensions, dont découlent la conjecture de Kakeya et la conjecture de restriction de Stein en toutes dimensions. Ce qui joue ici, c'est une équation aux dérivées partielles auxiliaire construite par le modèle. OpenAI dit avoir obtenu la preuve le 18 octobre et achevé la formalisation en Lean le lendemain ; la version en langage naturel comme les fichiers Lean sont publiés sur GitHub.
Cette piste n'est pas étrangère aux lecteurs chinois. La conjecture de lissage local a été formulée par Christopher Sogge en 1991 ; en 2019, Larry Guth, Hong Wang et Ruixiang Zhang ont démontré le cas de la dimension deux ; en 2025, Hong Wang et Joshua Zahl ont démontré la conjecture de Kakeya en dimension trois, alors considérée comme l'une des avancées les plus importantes de l'analyse harmonique depuis des années. Passer de la dimension trois à toutes les dimensions est un bond immense ; l'avis des mathématiciens extérieurs ne s'est pour l'instant exprimé dans aucune prise de position publique.
Yang–Mills : une simple relecture par des experts
Le troisième résultat relève de la physique mathématique. Les travaux démontrent, au sens mathématique strict, que certaines théories quantiques des champs en interaction contenant à la fois des champs de jauge et des fermions existent bien en dimension quatre, y compris la chromodynamique quantique, et traitent au passage un sous-problème de l'existence de la théorie de Yang–Mills pure. L'existence et le trou de masse de la théorie de Yang–Mills pure figurent parmi les problèmes du prix du millénaire de l'Institut Clay.
La méthode suit la voie de la théorie quantique des champs constructive de Tadeusz Balaban. Comme le modèle standard ne peut pas être extrapolé directement à des échelles de distance arbitrairement courtes, la preuve vise la plus simple des théories de grande unification contenant les champs de jauge et les fermions du modèle standard. La relecture a été menée par le prix Nobel David Gross, avec la participation de Michael Douglas, Arthur Jaffe, Igor Klebanov et Nikita Nekrasov. Ce résultat n'a pas fait l'objet d'une vérification formelle.
De mai à octobre
Si l'on met bout à bout les annonces mathématiques d'OpenAI cette année, le rythme s'accélère et les cibles changent. En mai, c'était un problème d'Erdős vieux de quatre-vingts ans ; en septembre, la question de la régularité des équations de Navier–Stokes, également accompagnée de fichiers Lean, mais sans qu'aucun mathématicien ait alors mené une vérification indépendante ; cette fois, c'est une hypothèse de complexité algorithmique dont dépendent de très nombreux travaux, et pour la première fois les auteurs mêmes de l'hypothèse figurent dans la liste des collaborateurs.
Les modes de vérification se différencient aussi : les deux résultats mathématiques fournissent des preuves Lean vérifiables par machine, tandis que le résultat physique ne peut s'appuyer que sur une relecture humaine. Lean garantit que la déduction ne comporte pas de faille, à condition que l'énoncé de la proposition n'ait pas été altéré lors de la formalisation. Cela ne pourra être confirmé qu'une fois que des équipes indépendantes auront lu les fichiers ligne par ligne.
Sources : annonce de recherche d'OpenAI, CocoLoop, ITHome ; fichiers de formalisation Lean publiés sur GitHub, utilisés pour vérifier l'objet de la preuve et le mode de vérification.