L’ETH est une conjecture sur la difficulté intrinsèque des problèmes de satisfaisabilité : en gros, elle pose que k-SAT (pour k ≥ 3) ne peut pas être résolu en temps 2o(n), où n désigne le nombre de variables — autrement dit, qu’aucun algorithme ne résout toutes les instances en temps sous-exponentiel par rapport à n. En pratique, l’ETH sert de référence pour évaluer la difficulté : de nombreuses bornes inférieures conditionnelles portant sur les problèmes de graphes, les requêtes de bases de données et les réductions en biologie computationnelle s’appuient sur elle pour soutenir qu’il serait surprenant de dépasser certains temps d’exécution. Lorsqu’un problème est qualifié de difficile au sens de l’ETH, cela signifie que toute amélioration majeure impliquerait une avancée remettant en cause cette référence.

L’affirmation d’OpenAI porte sur SAT à largeur fixe : des instances SAT contraintes par la structure des clauses ou les interactions entre variables. Si quelqu’un construit un algorithme qui résout toutes les instances de SAT à largeur fixe en temps 2o(n) — c’est-à-dire sous-exponentiel par rapport à n —, cela contredit l’affirmation générale de l’ETH selon laquelle les familles de problèmes k-SAT exigent un temps exponentiel. Une telle réfutation invaliderait de nombreux résultats conditionnels de difficulté reposant explicitement sur l’ETH. Point crucial : réfuter l’ETH ne revient pas à prouver P = NP. L’ETH est une conjecture plus forte et plus précise sur la dépendance exponentielle exacte des temps d’exécution. P = NP signifierait la disparition de l’écart entre le temps polynomial et le temps polynomial non déterministe ; un algorithme sous-exponentiel pour une famille particulière de problèmes SAT établit de meilleures performances asymptotiques pour cette famille, sans affirmer que tous les problèmes NP peuvent être résolus en temps polynomial.

Formaliser une preuve dans Lean est une étape importante : cela impose des définitions précises, comble de nombreuses lacunes informelles et produit un artefact vérifiable par machine, qui protège contre certaines catégories d’erreurs humaines. L’équipe d’OpenAI indique que la formalisation dans Lean a suivi la réfutation en langage naturel en moins de 24 heures. Cela dit, la vérification formelle établit la correction syntaxique relativement aux axiomes et aux définitions formels ; elle ne remplace pas l’interprétation collective par la communauté des hypothèses du modèle, des constantes cachées dans les analyses asymptotiques, des régimes de paramètres ni de la portée générale de l’algorithme, par opposition à une solution adaptée à des familles d’instances pathologiques.

OpenAI a invité un groupe d’experts dirigé par Russell Impagliazzo et Ramamohan Paturi — deux des auteurs originels de l’ETH — ainsi que par Ryan Williams, du MIT. Ce trio réunit le contexte historique et l’autorité technique nécessaires : Impagliazzo et Paturi peuvent déterminer si la réfutation proposée contredit réellement la formulation initiale de l’ETH, tandis que Williams peut évaluer les implications pour les bornes inférieures algorithmiques et les résultats conditionnels connexes. Leur pilotage devrait contribuer à un examen transparent et mené par des experts, tout en mettant en avant un modèle constructif de collaboration entre les entreprises d’IA et le monde universitaire.

Cet épisode illustre une nouvelle méthode de recherche : les modèles génératifs peuvent proposer des conjectures et même produire des preuves vérifiables par machine, raccourcissant ainsi le délai entre une idée et un artefact formel. Pour les parties prenantes — équipes de recherche, bailleurs de fonds et responsables produit —, la priorité immédiate devrait être d’investir dans des infrastructures de vérification, des dépôts ouverts d’artefacts et des audits financés par la communauté. Des risques persistent : les modèles peuvent inventer des lemmes erronés qui passent malgré tout la vérification des types, mal appliquer des définitions ou tirer parti d’hypothèses trop étroites sur les instances. La bonne réponse n’est ni l’enthousiasme aveugle ni le rejet systématique, mais une validation structurée et transparente menée par des experts du domaine.