← Все новости

AI ·

OpenAI опубликовала заявленное опровержение гипотезы экспоненциального времени, полученное внутренней модельюOpenAI publishes a claimed disproof of the Exponential Time Hypothesis produced by an internal model

В репозитории openai/math появилась статья «The Exponential Time Hypothesis is False» с формализацией на Lean: алгоритм точного подсчёта решений k-CNF за субэкспоненциальное время. Если доказательство устоит — это переворот в теории сложности; проверку ведёт группа во главе с Импальяццо, Патури и Уильямсом.The openai/math repo added a paper titled "The Exponential Time Hypothesis is False" with Lean formalisations: an algorithm that exactly counts k-CNF solutions in subexponential time. If it holds, it upends complexity theory; a group led by Impagliazzo, Paturi and Williams is reviewing it.

26 октября в открытом репозитории openai/math (лицензия Apache-2.0) появились две новые рукописи. Главная — «The Exponential Time Hypothesis is False»: детерминированный алгоритм, который точно считает число выполняющих наборов для CNF фиксированной ширины за субэкспоненциальное время и полиномиальную память. Частный случай 3-SAT опровергает ETH — гипотезу, на которой держатся сотни нижних оценок сложности алгоритмов.

Вторая работа посвящена локальному сглаживанию для волнового уравнения; по заявлению авторов, из неё следуют гипотезы Какейи.

Как получены результаты

По данным репозитория, их нашла неопубликованная внутренняя модель OpenAI — примерно за 3 часа «размышлений» уровня ChatGPT Pro на результат. Всего в репозитории 721 рукопись, около 42% основных результатов формализованы в Lean.

Важные оговорки

  • Доказательство не прошло рецензирование. Его проверяет рабочая группа под руководством Рассела Импальяццо (автора ETH), Рамамохана Патури и Райана Уильямса; материалы выложены досрочно по их просьбе.
  • Нам не удалось подтвердить, формализована ли в Lean именно статья про ETH.

Если результат подтвердится, это будет и крупнейший сдвиг в теории сложности за десятилетия, и самый сильный пример ИИ, делающего настоящую научную работу.

On Oct 26 two new manuscripts appeared in the public openai/math repository (Apache-2.0). The headline one, “The Exponential Time Hypothesis is False”, presents a deterministic algorithm that exactly counts satisfying assignments of fixed-width CNF in subexponential time and polynomial space. The 3-SAT case refutes ETH — the hypothesis underpinning hundreds of algorithmic lower bounds.

The second paper concerns local smoothing for the wave equation; the authors say it implies the Kakeya conjectures.

How the results were produced

According to the repo, an unreleased internal OpenAI model found them, using roughly 3 hours of ChatGPT Pro-level thinking per result. The repo holds 721 manuscripts in total, with about 42% of top-line results formalised in Lean.

Important caveats

  • The proof has not been peer reviewed. A working group led by Russell Impagliazzo (who formulated ETH), Ramamohan Paturi and Ryan Williams is checking it; the materials were released early at their request.
  • We could not confirm whether the ETH paper itself is formalised in Lean.

If confirmed, it would be both the biggest shift in complexity theory in decades and the strongest example yet of AI doing genuine research.

Источники