OpenAI et Anthropic affirment avoir réfuté une conjecture d'informatique théorique vieille de 27 ans, vérifiée par preuve formelle, mais sans portée pratique.
OpenAI et Anthropic sont les deux entreprises américaines derrière, respectivement, ChatGPT et l'assistant Claude, les deux familles d'intelligence artificielle générative les plus utilisées aujourd'hui. Fin octobre 2026, à un jour d'intervalle, elles ont chacune publié un résultat qui bouscule un pan entier de l'informatique théorique. L'écho est grand dans la presse spécialisée ; la portée pour une salle de classe, elle, est pour l'instant proche de zéro, et c'est bien tout l'intérêt du sujet.
Le 26 octobre, OpenAI affirme avoir réfuté l'hypothèse du temps exponentiel (ETH), une conjecture posée en 1999, il y a vingt-sept ans, par les chercheurs Russell Impagliazzo et Ramamohan Paturi, à l'université de Californie à San Diego. Elle affirme qu'aucun algorithme ne peut résoudre le problème dit « 3-SAT » (un problème mathématique classique, utilisé depuis des décennies comme référence pour mesurer la difficulté de centaines d'autres problèmes) sans que son temps de calcul n'explose de façon exponentielle à mesure que le problème grandit. Plus de 800 articles de recherche s'appuient dessus, directement ou via des hypothèses apparentées.
Le lendemain, 27 octobre, Anthropic publie à son tour un article de 49 pages, signé « Claude », qui présente un algorithme résolvant 3-SAT légèrement plus vite que l'exponentielle prévue. Selon le mathématicien Levent Alpöge, qui travaille chez Anthropic, cet algorithme a été trouvé par un modèle Claude de recherche interne, avec 14 millions de tokens générés et sans intervention humaine dans la découverte elle-même. Les deux laboratoires font remonter leur découverte à la même date, le 16 octobre.
Précision qui change beaucoup : la portée pratique de ce résultat est nulle. L'algorithme ne bat la résolution « brute force » qu'au-delà de 10 puissance 10 000 variables, un nombre sans aucun rapport avec quoi que ce soit de calculable un jour. C'est une avancée théorique, pas un outil.
Les deux démonstrations ont été formalisées dans Lean, un logiciel qui vérifie pas à pas qu'un raisonnement mathématique ne contient aucune erreur logique, en s'assurant que chaque étape découle bien de la précédente à partir des axiomes de départ. OpenAI indique avoir terminé sa vérification le 17 octobre, puis avoir confié à Impagliazzo, Paturi et à un troisième chercheur, Ryan Williams (MIT), l'organisation d'un examen ouvert par la communauté, en précisant bien que leur participation ne vaut pas certification du résultat. Anthropic a fait contrôler la sienne par le noyau de Lean et par un vérificateur indépendant ; son annexe précise qu'aucune personne n'était connue pour l'avoir relue au moment de la publication.
Le mathématicien Lance Fortnow, qui dit ne pas avoir vérifié la preuve lui-même, a écrit le 28 octobre sur son blog que l'on peut désormais considérer l'hypothèse comme morte.
Plusieurs voix appellent à la prudence. Magnus Wahlström, de l'université de Londres, dénonce un phénomène de « mathématiques appliquées par la presse » et s'inquiète que des modèles propriétaires rendent inutiles des mois entiers de travail de recherche humaine, sans qu'on puisse vérifier comment ils y sont parvenus. Ryan Williams, qui a accepté d'organiser l'examen côté OpenAI, a par ailleurs qualifié une précédente publication de 722 articles de mathématiques générés par les modèles d'OpenAI d'« attaque par déni de service contre les mathématiciens », tout en reconnaissant que certaines parties de cette preuve-ci sont routinières et deux ou trois éléments réellement inhabituels.
Sur la cryptographie, une inquiétude légitime vu l'ampleur de la conjecture : une responsable d'OpenAI s'est dite « raisonnablement confiante » qu'aucun système cryptographique actuel n'est cassé par ce résultat. Williams nuance en notant que des raffinements futurs pourraient un jour toucher des systèmes dimensionnés sur des tailles de clés précises, mais le chiffrement RSA, par exemple, repose sur la factorisation, qui n'est pas connue pour être aussi difficile que 3-SAT. Les solveurs industriels utilisés en entreprise, de leur côté, ne sont pas concernés : ils reposent sur des approches empiriques que l'ETH n'a jamais prétendu encadrer. La question « P contre NP », elle, reste entièrement ouverte.
Rien à changer dans tes cours dès demain : aucun programme de mathématiques, de NSI ou de spécialité ne repose sur l'hypothèse du temps exponentiel, et aucun système de chiffrement que tes élèves utilisent n'est remis en cause. Ce qui est intéressant à en tirer, si tu enseignes les maths, la NSI ou que le sujet de l'IA revient en classe, c'est un exemple concret et récent de ce que ces modèles savent et ne savent pas encore faire en recherche : proposer une démonstration formalisable, vérifiable pas à pas par une machine, sur un problème resté ouvert vingt-sept ans, tout en restant incapables de dire avec certitude si leur propre raisonnement est correct sans l'aide d'un vérificateur externe et de chercheurs humains. C'est aussi un bon antidote aux deux excès symétriques qu'on entend souvent, « l'IA a résolu un problème insoluble » et « l'IA ne fait qu'inventer » : la réalité, ici, est plus mesurée, contestée par la communauté elle-même, et sans aucune conséquence pratique à ce jour. Si le sujet revient dans une discussion avec des élèves curieux, c'est un cas d'école pour expliquer pourquoi une annonce spectaculaire mérite d'être vérifiée avant d'être crue, par une IA comme par n'importe quelle source.