OpenAI et Anthropic affirment que leurs IA ont réfuté une hypothèse clé de l'informatique

Le 26 octobre, OpenAI met en ligne un document au titre sans nuance : « The Exponential Time Hypothesis is False » (l'hypothèse du temps exponentiel est fausse). Le 27 octobre, Anthropic publie à son tour un article signé « Claude (Anthropic) » qui affirme la même chose. Les deux entreprises disent que leur modèle interne, non commercialisé, a trouvé l'idée centrale le 16 octobre.

Chaque texte est accompagné d'une preuve formalisée dans Lean, un logiciel qui vérifie mécaniquement chaque étape d'un raisonnement mathématique. Aucun n'a encore été validé par la communauté scientifique.

Une hypothèse sur laquelle reposent des centaines de travaux

Formulée à la fin des années 1990 par Russell Impagliazzo et Ramamohan Paturi, avec Francis Zane, l'hypothèse du temps exponentiel (ETH) porte sur un problème logique célèbre, 3-SAT : peut-on donner à des variables la valeur « vrai » ou « faux » de façon à satisfaire une liste de contraintes portant chacune sur trois d'entre elles ? L'hypothèse affirme qu'aucun algorithme ne peut y parvenir sans un temps qui se multiplie par un facteur fixe à chaque variable ajoutée.

Les chercheurs s'en servent pour démontrer que des problèmes de graphes, de biologie ou de bases de données ne peuvent pas être résolus rapidement. Selon l'article d'Anthropic, plus de 800 travaux en dépendent, directement ou par une hypothèse voisine. Les deux laboratoires décrivent un algorithme qui résout 3-SAT, et compte même ses solutions, en un temps dit « sous-exponentiel ». Jelani Nelson, informaticien de Berkeley en congé de l'université pour travailler chez Anthropic, a déposé l'article de l'entreprise sur la plateforme Hexagon et en a relu la preuve avant publication. Selon lui, les deux démonstrations aboutissent à peu près à la même borne.

Qui vérifie ces preuves ?

OpenAI a confié son résultat à trois spécialistes : Russell Impagliazzo et Ramamohan Paturi, les auteurs de l'hypothèse, de l'université de Californie à San Diego, et Ryan Williams, du MIT. Dans une lettre ouverte, ils préviennent que leur participation « ne doit pas être considérée comme une certification ». Selon The Next Web, Ryan Williams précise qu'ils n'ont signé aucun accord de confidentialité et ne seront pas payés. OpenAI dit ne réclamer aucun crédit académique et a versé 5 millions de dollars à la Fondation Simons pour des ateliers sur les résultats produits par l'IA.

Côté Anthropic, l'avertissement figure dans le dépôt de code lui-même : la formalisation Lean « a été écrite par des modèles d'IA », et aucune machine ne vérifie que son énoncé dit bien ce que dit l'article ; ce contrôle revient à un lecteur humain. Une annexe de l'article précise que cette formalisation n'a été relue que par d'autres instances des mêmes modèles et qu'au moment de la rédaction, aucune personne n'est connue pour l'avoir vérifiée.

OpenAI revendique aussi deux autres résultats, en analyse et en physique théorique. Le second touche à l'un des « problèmes du millénaire » de l'institut Clay, mais ses documents ne sont pas publics : le groupe de physiciens mené par le prix Nobel David Gross a choisi de rédiger lui-même ses conclusions.

Rien ne change pour les logiciels ni pour le chiffrement

« Si l'affirmation est correcte, elle changera une partie importante de l'informatique théorique », écrivent les trois relecteurs d'OpenAI. La pratique, elle, ne bouge pas. Le dépôt d'Anthropic le dit sans détour : le résultat « ne dit rien de la résolution de formules en pratique ». Selon l'article, pour une formule comptant cinq fois plus de contraintes que de variables, l'algorithme ne bat la recherche exhaustive qu'au-delà de 10^10 000 variables. La question « P = NP ? » reste ouverte. Le chiffrement n'est pas menacé : la factorisation, sur laquelle repose RSA, se fait déjà en temps sous-exponentiel depuis des décennies, et la taille des clés en tient compte.

Reste la coïncidence : deux modèles concurrents, la même découverte, le même jour. Jelani Nelson l'a constaté sur X. Ce n'est pas la première incursion des deux laboratoires sur ce terrain : ils financent déjà la vérification de preuves écrites par l'IA. Les relecteurs d'OpenAI s'inquiètent que le crédit aille à qui publie le premier ou dispose des outils les plus puissants, plutôt qu'à ceux qui vérifient et expliquent ; en juin, des mathématiciens posaient déjà la question de l'attribution dans la « déclaration de Leiden ». Les ateliers à venir diront si la démonstration résiste à l'examen humain.