OpenAI et Anthropic affirment successivement que l'IA a réfuté l'« Hypothèse du Temps Exponentiel » (Frontier AI labs say their models refuted the Exponential Time Hypothesis)

OpenAI 10 26 a publié trois résultats issus de ses modèles internes en mathématiques, informatique et physique, dont la preuve que l'Hypothèse du Temps Exponentiel (ETH) de la théorie de la complexité computationnelle est fausse ; quelques heures plus tard, Anthropic a également publié une réfutation de l'ETH obtenue par son modèle de recherche Claude interne, accompagnée d'une preuve formelle en Lean 4 rédigée par l'IA. Les deux résultats sont encore en attente de validation par les pairs.

OpenAI 10 26 a publié trois résultats issus de ses modèles internes en mathématiques, informatique et physique, dont la preuve que l'Hypothèse du Temps Exponentiel (ETH) de la théorie de la complexité computationnelle est fausse ; quelques heures plus tard, Anthropic a également publié une réfutation de l'ETH obtenue par son modèle de recherche Claude interne, accompagnée d'une preuve formelle en Lean 4 rédigée par l'IA. Les deux résultats sont encore en attente de validation par les pairs.

Confiance : élevée (100) · Date de l'événement 2026-10-25

Justification

  • L'ETH affirme que le problème 3-SAT nécessite un temps exponentiel dans le pire des cas. L'article d'OpenAI présente un algorithme déterministe qui compte exactement le nombre d'assignations satisfaisantes pour toute formule k-CNF en temps sous-exponentiel ; le dépôt d'Anthropic propose également un algorithme en temps 2^o(n) pour le 3-SAT. Les deux précisent qu'il s'agit d'un résultat asymptotique, Anthropic indiquant explicitement que cela n'a rien à voir avec la vitesse réelle de résolution des formules.
  • The Decoder rapporte que des centaines d'articles en théorie des graphes, biologie computationnelle, bases de données et géométrie computationnelle reposent sur l'ETH comme hypothèse, et que si l'ETH est fausse, ces conclusions perdraient leur fondement (ce qui ne signifie pas qu'elles sont erronées). Dans une interview accordée à TechCrunch, le professeur Ryan Williams du MIT a déclaré qu'OpenAI avait vérifié qu'aucun système cryptographique ne serait compromis par cette découverte.
  • Les deux autres résultats (selon The Decoder et The Verge) : en mathématiques, la preuve de la conjecture de lissage local pour toutes les dimensions, impliquant les conjectures de Kakeya et de restriction de Stein, a été publiée directement ; en physique, la preuve de l'existence mathématique de théories quantiques des champs comme le Yang-Mills en quatre dimensions (sans « écart de masse », le problème du millénaire n'étant pas entièrement résolu), examinée par un groupe dirigé par le lauréat du prix Nobel David Gross, dont les matériaux ne sont pas encore publics.
  • Le dépôt d'Anthropic précise également que Claude Opus 5.5, dans un mode de raisonnement élevé, peut reconstruire cette réfutation à partir d'une idée clé compressée (obtenant seulement une borne plus faible, pas le résultat le plus fort de l'article).

Utilisation

  • Le PDF de l'article d'OpenAI sur l'ETH se trouve dans le répertoire preprints du dépôt GitHub openai/math ; l'article et la preuve Lean d'Anthropic se trouvent dans le répertoire eth du dépôt GitHub anthropics/formal-math, le README fournissant les étapes de vérification via lake build (officiellement environ 8 minutes, avec un processus maximal utilisant environ 7 Go de mémoire).
  • Les initiateurs originaux de l'ETH, Russell Impagliazzo, Ramamohan Paturi et Ryan Williams, ont publié une lettre ouverte sollicitant des avis de pairs, et les progrès de l'examen seront publiés progressivement (selon The Decoder).

Risques

  • Le texte original de l'annonce sur openai.com est inaccessible (403) ; la méthode de publication des trois résultats, le groupe d'examen, ainsi que le don de 500 millions de dollars d'OpenAI à la Fondation Simons pour organiser un séminaire, proviennent de rapports relayés par The Decoder et The Verge.
  • Lean ne garantit que la preuve de la proposition écrite dans Lean ; Anthropic précise également qu'aucune vérification machine n'a été effectuée pour assurer la cohérence entre l'énoncé Lean et l'article. Williams et al. soulignent que la participation à l'examen n'équivaut pas à un soutien.
  • Le mathématicien d'Anthropic, Levent Alpöge, estime que la solution d'OpenAI repose sur des travaux existants (TechCrunch) ; le groupe consultatif Mathématiques et IA AGMAI critique le fait qu'OpenAI ait montré les résultats à des experts désignés avant la publication et que la partie physique ne soit pas publique (The Verge).
  • L'annonce d'OpenAI est antérieure à la période de cette édition (10 26) ; l'inclusion dans cette édition repose sur les articles primaires lisibles sur GitHub et les nouveaux résultats d'Anthropic.

Ouvrir · Article d'OpenAI « The Exponential Time Hypothesis is False » (GitHub openai/math) · Article et preuve Lean d'Anthropic (GitHub anthropics/formal-math/eth) · The Decoder · The Verge

TechCrunch

Parcourir les dernières actualités IA