0 00 6 min 2 semaines 43

Le 27 octobre, Anthropic a diffusé une prépublication proposant un algorithme en temps sous-exponentiel pour 3-SAT. Un résultat potentiellement majeur, encore soumis à l’examen de chercheurs indépendants.

Une course scientifique inattendue semble se dessiner entre deux grands laboratoires d’intelligence artificielle. Le 27 octobre 2026, Anthropic a présenté une prépublication attribuant à un modèle Claude la découverte d’un algorithme remettant en cause l’Exponential Time Hypothesis, ou ETH. Le résultat apparaît au lendemain d’une annonce comparable d’OpenAI.

Ce que dit le document scientifique

La prépublication, intitulée A 2^{o(n)} Time Algorithm for 3-SAT, annonce un algorithme déterministe en temps sous-exponentiel pour le problème 3-SAT, exprimé en fonction du nombre de variables. Elle affirme également traiter #3-SAT, problème plus complexe consistant à compter les affectations satisfaisantes plutôt qu’à seulement déterminer si elles existent.

Le document est publié sur Hexagon, avec la mention que son contenu est principalement généré par IA et que certaines parties seulement ont été comprises ou examinées par des humains. Ce marquage constitue lui-même un élément intéressant pour évaluer le statut de la publication.

Une découverte initiale attribuée à Claude

Anthropic indique que le cœur de l’algorithme aurait été trouvé le 16 octobre par un modèle de recherche Claude, sans intervention humaine durant cette étape. Le processus aurait mobilisé environ 14 millions de tokens de sortie. Des chercheurs de l’entreprise auraient ensuite collaboré avec le système pour améliorer la présentation du résultat.

Il s’agit d’une déclaration de provenance émise par le laboratoire. Les conditions exactes de conception, d’entraînement et de supervision du modèle ne peuvent pas être déduites de cette seule indication.

Pourquoi ETH compte

L’hypothèse ETH affirme, très schématiquement, que certains problèmes de satisfaisabilité ne disposent pas d’algorithmes suffisamment rapides pour éviter une croissance exponentielle du temps de calcul dans le pire des cas.

Elle ne se confond pas avec la question P contre NP. Une éventuelle réfutation d’ETH modifierait le paysage de la complexité algorithmique, mais ne signifierait pas que tous les problèmes difficiles deviennent immédiatement faciles à résoudre.

La preuve assistée par Lean 4

Anthropic déclare avoir formalisé le résultat dans Lean 4. Le code est présenté comme vérifiable par des systèmes logiciels capables de contrôler des raisonnements mathématiques formels. Cette démarche renforce la possibilité d’un audit reproductible, mais elle ne résout pas automatiquement les questions de correspondance entre l’énoncé théorique et le code, d’interprétation du résultat ni de validation externe.

Il faut également éviter un raccourci : une preuve asymptotique ne garantit pas une amélioration pratique des performances pour des problèmes de taille courante. Les constantes cachées, la mémoire requise et les conditions d’application jouent un rôle déterminant.

Deux découvertes indépendantes ?

OpenAI affirme avoir également obtenu une réfutation le 16 octobre et avoir finalisé sa formalisation le 17 octobre. Anthropic parle de travaux indépendants et concomitants. Pour l’instant, cette indépendance doit être appréciée à partir des éléments rendus publics et de l’analyse scientifique des méthodes employées.

Analyse PRODPRESS

Cette actualité pose des enjeux qui dépassent la compétition commerciale entre laboratoires. Elle concerne les critères permettant d’admettre une découverte scientifique assistée ou produite par IA : accès aux données, traçabilité des calculs, formalisation, documentation, revue par les pairs et reproductibilité.

La question critique est moins « quelle IA a gagné ? » que « comment vérifier collectivement une preuve dont aucun humain n’a encore maîtrisé toutes les étapes ? »

Glossaire et état de vérification

3-SAT : problème consistant à déterminer si une formule logique à clauses de trois littéraux est satisfaisable. #3-SAT : problème de comptage des solutions. Temps sous-exponentiel : catégorie théorique de croissance algorithmique. Lean 4 : environnement de formalisation et de vérification des preuves.

Au 28 octobre 2026 : prépublication et dépôt accessibles ; revendication de découverte attribuée à Claude documentée ; validation indépendante complète et conséquences théoriques à confirmer.

Sources et documentation


Christophe Martin-Landré — Journaliste d’investigation, fondateur et directeur de publication de PRODPRESS®

© 2026 PRODPRESS MEDIA GROUP LLC — Tous droits réservés.

Authentique. Impertinent. Libre.

Note éditoriale : synthèse rédigée à partir de documents identifiés et de déclarations publiques. Les recherches en cours et les résultats scientifiques revendiqués restent distingués des faits établis.