OpenAI a annoncé le 26 octobre 2026 que son système avait produit un résultat qui, selon l’entreprise, réfute l’Exponential Time Hypothesis (ETH), une conjecture sur la complexité de 3-SAT. OpenAI situe la découverte en langage naturel au 16 octobre et sa formalisation dans Lean au 17 octobre. La documentation Lean décrit un théorème de comptage exact pour des formules k-CNF, tandis qu’elle attribue au manuscrit des bornes de temps plus serrées.
Ce qu’OpenAI affirme au sujet de l’ETH
L’ETH suppose que, dans le pire cas, 3-SAT ne peut pas être résolu en temps sous-exponentiel. OpenAI affirme que son système a trouvé un résultat qui contredirait cette conjecture. L’annonce présente cette conclusion comme une affirmation à examiner, pas comme un verdict scientifique indépendant.
Le 26 octobre, OpenAI a annoncé qu’un groupe dirigé par Russell Impagliazzo, Ramamohan Paturi et Ryan Williams examinerait et expliquerait le résultat. OpenAI associe Impagliazzo et Paturi à UC San Diego, et Williams au MIT.
Ce que la formalisation Lean couvre
La documentation de portée de Lean décrit, pour un entier k fixé avec k ≥ 2, une machine déterministe qui compte exactement les affectations satisfaisantes d’une formule k-CNF encodée canoniquement. Le comptage exact donne le nombre de configurations qui satisfont la formule, au lieu de répondre seulement à la question de savoir s’il en existe une.
Pour n variables et un encodage de longueur L bits, la borne de temps donnée pour ce théorème est (L+1)^{O_k(1)} 2^{O_k(n(log log n)^2/√log n)}. La documentation indique aussi que la machine visite au plus (L+1)^{O_k(1)} cellules de bande au total.
Les bornes attribuées au manuscrit sont distinctes
La même documentation attribue au manuscrit daté du 25 octobre une borne de temps plus serrée : (n+m)^{O_k(1)} 2^{O_k(n log log n/√log n)}, où m désigne le nombre de clauses. Pour le cas où m ≤ Dn, avec D > 0 fixé, elle donne (n+m)^{O_{k,D}(1)} 2^{O_{k,D}(n/√log n)}.
Ces expressions sont présentées comme des bornes du manuscrit, distinctes de celle du théorème formalisé dans Lean. La page de portée les attribue au manuscrit; elle ne les présente pas comme la borne exacte de la formalisation.
De l’enjeu théorique aux performances pratiques
L’ETH sert de base à des résultats conditionnels de difficulté dans des centaines d’articles, selon OpenAI, notamment en théorie des graphes, en biologie computationnelle, dans les bases de données et en géométrie computationnelle. L’annonce ne prétend pas résoudre P = NP. OpenAI précise que transformer une avancée théorique en amélioration pratique nécessitera encore d’importantes recherches : la borne annoncée ne signifie donc pas que les ordinateurs ou les solveurs SAT deviennent immédiatement plus rapides.
Dans sa mise à jour du 28 octobre 2026, ExplainX indiquait qu’aucune confirmation indépendante du résultat n’avait été signalée à cette date.
Pour visualiser l’ETH et la différence entre une borne asymptotique et un gain pratique, Adem B10 propose une explication en anglais. Le puzzle à interrupteurs qu’il utilise est une illustration simplifiée, pas l’algorithme d’OpenAI.
