Un deuxième laboratoire de pointe affirme que son IA a fait tomber l'un des postulats de travail de la théorie de la complexité. Le 27 octobre, Anthropic a intégré à son dépôt public formal-math, sur GitHub, un dossier réunissant un article attribué à Claude et un développement Lean 4 censé démontrer que l'hypothèse du temps exponentiel (ETH) est fausse. Cette publication est intervenue quelques heures après celle d'OpenAI, qui revendique sa propre réfutation de la même conjecture, et les deux équipes se présentent comme indépendantes.
Énoncée par Russell Impagliazzo et Ramamohan Paturi en 1999, l'ETH postule que 3-SAT, c'est-à-dire savoir si une formule booléenne à clauses de trois littéraux admet une solution, demande un temps exponentiel en nombre de variables pour une certaine constante fixe. L'article d'Anthropic décrit un algorithme déterministe qui ne se contente pas de trancher : il compte les affectations satisfaisantes, en temps 2 puissance O(n log log n divisé par la racine carrée de log n). Cet exposant croissant moins vite que tout multiple constant de n, il en découle que 3-SAT se résout en temps 2^o(n).
Le récit de la découverte sort de l'ordinaire. Selon la note de provenance figurant sur la fiche de l'article dans Hexagon, un modèle de recherche interne de Claude a trouvé le cœur de l'algorithme le 16 octobre, en produisant environ 14 millions de tokens sans aucune intervention humaine ; les chercheurs d'Anthropic ont ensuite travaillé avec lui à la rédaction. La fiche indique d'ailleurs que le texte est principalement généré par IA. Le README du dépôt ajoute que Claude Opus 5.5, réglé sur un effort élevé, sait reconstruire la version décisionnelle de la réfutation à partir d'un indice condensé reproduit sur place.
Le volet formel est conçu pour être contrôlé de l'extérieur. Un fichier court, MainResults.lean, énonce deux théorèmes sur le modèle de machines de Turing de Mathlib : la fausseté de l'ETH et la borne de comptage principale de l'article. D'après le README, tous deux ne reposent que sur les trois axiomes standard de Lean, la compilation prend environ huit minutes sur 24 processeurs virtuels, et l'intégration continue du dépôt s'appuie sur l'outil Comparator pour revérifier les preuves avec un second noyau, écrit séparément, baptisé nanoda. Le code est publié sous licence Apache 2.0.
Anthropic dit clairement ce que la vérification mécanique ne garantit pas. Lean atteste que les preuves découlent des définitions posées, mais aucun logiciel ne confirme que MainResults.lean traduit fidèlement l'article, et une analyse de SXZ.io cite le texte lui-même pour souligner que personne, à sa connaissance, n'a relu le code Lean écrit par l'IA. Cette analyse relève aussi que le théorème affirme seulement l'existence d'une constante et que, selon les calculs de l'article, la borne ne bat la recherche exhaustive que pour des formules de plus de 10^10 000 variables, dans le cas de cinq clauses par variable.
La comparaison avec les travaux d'OpenAI a déjà commencé. SXZ.io note que l'énoncé Lean d'Anthropic couvre la borne complète de l'article et pose directement la fausseté de l'ETH, alors que le théorème formel d'OpenAI porte sur un exposant plus faible que celui de son manuscrit ; la configuration d'Anthropic active en outre le second noyau, que celle d'OpenAI laisse désactivé. TechCrunch, qui a couvert les deux annonces, cite Ryan Williams, du MIT : si ces affirmations tiennent, de nombreux articles fondés sur l'ETH devront être revus, et la communauté devrait accorder un peu plus de crédit à l'éventualité P = NP.
L'examen par les pairs ne fait que commencer. Williams, Impagliazzo et Paturi organisent la réponse de la communauté informatique à la revendication d'OpenAI et ont écrit que leur implication ne valait pas certification ; aucun examen équivalent de l'article d'Anthropic n'a été annoncé. Les retombées pratiques restent minces pour l'instant. Anthropic insiste sur le caractère purement asymptotique du résultat, qui ne permet pas de résoudre plus vite des formules réelles : l'enjeu est théorique, et tient à ce qu'il révèle de systèmes d'IA capables de produire des mathématiques vérifiables.