Hypothèse du temps exponentiel : ce que valent les réfutations d'OpenAI et d'Anthropic, vérifiées en Lean

En une phrase : OpenAI et Anthropic affirment que leurs modèles ont réfuté une conjecture centrale de l'informatique théorique, et les deux preuves passent le vérificateur Lean ; mais savoir si l'énoncé vérifié est bien la conjecture reste un travail humain, en cours, et le résultat n'a aucune portée pratique.

L'annonce a souvent été résumée ainsi : l'IA a réfuté l'hypothèse du temps exponentiel. Ce raccourci mélange trois choses qu'il faut séparer : ce que les deux entreprises revendiquent, ce qu'un logiciel de vérification a réellement contrôlé, et ce que ça change hors des laboratoires de recherche. Cet explicatif reprend les documents publiés, tels qu'ils étaient en ligne le 1er novembre 2026 au matin.

L'hypothèse du temps exponentiel, en clair

Le problème s'appelle 3-SAT. On te donne une formule logique faite de variables qui valent vrai ou faux, regroupées en petites clauses de trois au plus, et il faut dire s'il existe une façon de choisir les valeurs qui rend toutes les clauses vraies. Vérifier une solution est facile. La trouver semble difficile : avec n variables, essayer toutes les combinaisons demande 2ⁿ essais. Selon l'article d'Anthropic, les meilleurs algorithmes connus jusqu'ici ne faisaient que réduire la base de cette exponentielle, avec un record de 1,328ⁿ pour un algorithme déterministe et de 1,308ⁿ pour un algorithme qui utilise le hasard.

L'hypothèse du temps exponentiel (ETH, pour Exponential Time Hypothesis) parie que l'on ne fera jamais beaucoup mieux : il existerait une constante au-dessous de laquelle aucun algorithme ne peut descendre, si bien que 3-SAT demanderait toujours un temps exponentiel. Elle a été proposée en 1999 par Russell Impagliazzo et Ramamohan Paturi, dans le prolongement de travaux menés avec Francis Zane, rappelle l'informaticien Lance Fortnow.

Ce n'est pas la question « P = NP ? », qui demande si 3-SAT peut se résoudre en temps polynomial. L'ETH est un pari plus fort, et le réfuter ne tranche pas cette question : Anthropic l'écrit noir sur blanc dans son article.

Pourquoi les chercheurs y tiennent : l'ETH sert de point de départ à une multitude de résultats de la forme : si l'ETH est vraie, alors tel autre problème ne peut pas être résolu plus vite qu'une certaine limite. OpenAI parle de « centaines » d'articles qui s'appuient dessus, en théorie des graphes, en biologie numérique ou en bases de données. Anthropic avance plus de 800 articles, issus d'une recherche bibliographique faite par son modèle Claude, selon son article.

Ce qu'OpenAI et Anthropic revendiquent

OpenAI a fait son annonce le 26 octobre 2026, avec deux autres résultats, en mathématiques et en physique. Selon l'entreprise, son système a trouvé la réfutation le 16 octobre, puis l'a formalisée dans Lean le 17 octobre. Le manuscrit et la preuve Lean ont été déposés dans son dépôt public openai/math le 26 octobre à 21 h 52 (heure de Paris), selon l'historique du dépôt. L'algorithme compte exactement les solutions d'une formule (ce qui permet aussi de dire s'il en existe une), en un temps « sous-exponentiel » : l'exposant croît un peu moins vite que n, de l'ordre de n × log log n / √log n.

Anthropic a publié son propre article, signé « Claude », dans le dépôt anthropics/formal-math, le 27 octobre à 4 h 07 (heure de Paris), avec une preuve Lean. L'entreprise y écrit que l'algorithme central a été trouvé le 16 octobre par un modèle Claude de recherche interne, avec 14 millions de tokens de sortie et sans intervention humaine, et que des chercheurs ont ensuite retravaillé la présentation avec Claude. Le résultat a la même forme que celui d'OpenAI, obtenu, dit Anthropic, « indépendamment et en parallèle ».

Deux réfutations de la même conjecture, trouvées le même jour (le 16 octobre, selon les deux entreprises) par deux modèles concurrents : c'est ce qui a fait réagir les spécialistes. Lance Fortnow, qui n'a pas lui-même vérifié la preuve, écrit sur son blog le 28 octobre qu'on peut désormais considérer l'hypothèse comme tombée.

Ce que Lean vérifie, et ce qu'il ne vérifie pas

Lean est un assistant de preuve : un logiciel qui vérifie, étape par étape, qu'une preuve écrite dans son langage établit bien l'énoncé formel annoncé. Son « noyau » ne fait pas confiance à l'auteur, humain ou modèle de langage. C'est pour ça qu'il compte ici : un modèle peut produire un raisonnement faux mais convaincant (c'est le problème des hallucinations), alors qu'une preuve acceptée par le noyau de Lean est correcte par rapport à son énoncé, sauf défaut du vérificateur lui-même.

Un contrôle indépendant détaillé a été publié par Carlos Toledo, qui précise que rien de son travail n'a été partagé avec les deux laboratoires, ni exécuté ou relu par eux. Il a rejoué les deux preuves à partir des versions figées des dépôts, avec l'outil Comparator, le noyau de Lean et un second noyau écrit indépendamment, nanoda : les deux preuves sont acceptées et ne reposent que sur les trois axiomes standard de Lean. Il précise avoir développé ses outils avec Claude, le modèle d'Anthropic.

Mais une machine ne vérifie que ce qu'on lui demande de vérifier. Reste une question de lecture : l'énoncé formel dit-il vraiment « l'ETH est fausse » ? Carlos Toledo conclut que son travail « ne certifie pas que l'ETH est fausse », parce que deux points restent de la lecture humaine : que le modèle de machine et le codage des formules choisis par chaque entreprise correspondent à ceux des manuels, et que sa propre définition de l'ETH en Lean est la bonne. Anthropic dit la même chose dans l'annexe de son article : la preuve Lean a été écrite par des modèles d'IA et relue par d'autres instances des mêmes modèles, et, au moment de la rédaction, aucune personne n'était connue pour l'avoir vérifiée.

Deux écarts sont visibles dans les documents eux-mêmes :

• Chez OpenAI, la preuve Lean ne couvre pas le résultat principal de l'article. La note de portée du dépôt indique que Lean établit un exposant de l'ordre de n × (log log n)² / √log n, alors que l'article annonce n × log log n / √log n. Le résultat le plus fort ne repose que sur la preuve rédigée en langage courant. Les deux bornes suffisent à réfuter l'ETH.
• Chez OpenAI toujours, les fichiers Lean ne définissent pas l'ETH. C'est Carlos Toledo qui a écrit une définition « de manuel » et prouvé en Lean que l'énoncé d'OpenAI la contredit, dans le modèle de machine d'OpenAI. Anthropic, lui, définit l'ETH dans son fichier d'énoncés et en prouve la négation.

OpenAI a confié l'examen de son résultat à un groupe mené par Russell Impagliazzo et Ramamohan Paturi (université de Californie à San Diego) et Ryan Williams (MIT). Dans leur lettre d'ouverture publiée sur le blog d'examen le 26 octobre, ils préviennent que leur participation « ne doit pas être prise comme une certification » du résultat (traduction Le Latent). Le dernier billet du blog, daté du 30 octobre, ouvre un fil pour recenser les personnes qui ont recompilé les preuves Lean de leur côté.

Ce que ça change pour toi : rien en pratique

C'est le point que les reprises ont le moins mis en avant, et ce sont les auteurs eux-mêmes qui le disent. Dans son article, Anthropic qualifie son résultat de « purement asymptotique » : il décrit ce qui se passe quand le nombre de variables tend vers l'infini.

Les seuils donnés par Anthropic, et leur traduction :

• Formules avec cinq clauses par variable : la borne prouvée ne fait pas mieux que l'essai de toutes les combinaisons tant que n ne dépasse pas 10 puissance 10 000, selon Anthropic. Autrement dit, il faudrait un nombre de variables qui s'écrit avec plus de 10 000 chiffres.
• Formules quelconques : le seuil passe à 10 puissance 100 millions, d'après le même article, soit un nombre de variables qui s'écrit avec plus de 100 millions de chiffres.
• Même en optimisant : l'approche ne semble pas pouvoir apporter de gain avant n supérieur à 10 millions, alors que l'essai de toutes les combinaisons est déjà hors de portée à 100 variables, écrit Anthropic, qui conclut que son résultat « ne dit rien » de la résolution de formules en pratique.

OpenAI reste plus général dans son annonce : transformer ces avancées théoriques en améliorations pratiques demandera « beaucoup de recherche » supplémentaire, selon l'entreprise.

L'effet ne s'étend pas non plus à tous les problèmes difficiles. Lance Fortnow note que l'algorithme ne donne rien de nouveau pour le problème du voyageur de commerce ou celui de la somme de sous-ensembles, car les traductions de ces problèmes en 3-SAT font exploser le nombre de variables. Il rappelle aussi que la chute de l'ETH ne rend pas fausses les conséquences qu'on en tirait : elles perdent seulement leur justification.

Si tu développes, que tu utilises des solveurs pour de la planification ou que tu étudies l'informatique, rien ne change dans tes outils. Ce qui change, c'est la recherche : des résultats de difficulté appuyés sur l'ETH sont à revoir, et les théoriciens cherchent maintenant jusqu'où on peut aller.

Comment lire la prochaine annonce « l'IA a démontré »

Cette affaire donne une grille utile pour les annonces à venir. OpenAI rappelle dans son annonce qu'il avait déjà publié d'autres résultats produits par ses modèles le 6 octobre 2026, et Anthropic suit le même chemin :

1. La preuve est-elle publique et formalisée ? Ici oui, dans les dépôts openai/math et anthropics/formal-math, avec les commandes pour la recompiler.
2. L'énoncé formel est-il celui annoncé ? Chez OpenAI, il est plus faible que le titre de l'article, et c'est écrit dans la note de portée.
3. Des humains indépendants ont-ils lu l'énoncé ? Pour l'instant, des volontaires et des blogueurs spécialisés, pas encore les examinateurs désignés.
4. Les auteurs revendiquent-ils une portée pratique ? Ici non, et Anthropic chiffre lui-même l'écart.

Un modèle de raisonnement peut désormais produire des preuves que Lean accepte. La vérification par la machine règle la question des erreurs de logique ; elle laisse entière celle du sens de l'énoncé, qui reste, pour l'ETH, entre les mains des chercheurs qui l'ont inventée. Pour situer ces annonces dans le reste de l'actualité de l'IA, la rubrique Comprendre rassemble nos explications de fond.