Claude опроверг гипотезу об экспоненциальном времени

Claude опроверг гипотезу об экспоненциальном времени (ETH). В статье Anthropic, выложенной 27 октября, описан детерминированный алгоритм, который решает 3-SAT на n переменных за время 2^o(n) и заодно считает число выполняющих наборов. На практических SAT-солверах это никак не скажется: по расчёту самой статьи, полный перебор новая оценка обгоняет только на формулах, где переменных больше 10^(10^8).

Ядро алгоритма внутренняя исследовательская модель Claude нашла 16 октября: на это ушло 14 млн выходных токенов, и человек в работе не участвовал. Исследователи Anthropic потом вместе с Claude доводили изложение, а автором статьи значится «Claude (Anthropic)». Доказательство формализовано в Lean 4, перепроверено вторым, независимо написанным ядром проверки nanoda и выложено на GitHub под лицензией Apache 2.0. Lean-разработку писали ИИ-модели, рецензировали её другие экземпляры тех же моделей, и, как сказано в статье, «на момент написания ни один человек, насколько известно, её не проверял»; константа в оценке явно не выписана. Hexagon пометил публикацию ярлыком HUMAN UNDERSTANDING: SOME PARTS.

Почему солверы этого не заметят

3-SAT спрашивает, можно ли выполнить формулу из клауз по три литерала. Перебор всех 2^n наборов работает всегда, а лучшие алгоритмы с 1980-х лишь уменьшали основание степени. Статья Anthropic называет рекордами 1,328^n для детерминированных алгоритмов и 1,308^n для рандомизированных (OpenAI в своей работе ссылается на препринт 2026 года с 1,307031578^n). ETH, которую сформулировали Impagliazzo и Paturi, утверждает, что 3-SAT нельзя решить быстрее, чем за экспоненту с некоторой фиксированной долей n в показателе. У Claude показатель растёт как n log log n/√log n (для k-SAT с множителем k²), а это медленнее, чем dn при любом d больше нуля.

Порог в 10^(10^8) переменных записывается числом примерно из ста миллионов цифр, и на всех формулах меньше его оценка ничем не лучше перебора. До P = NP отсюда тоже далеко: время по-прежнему растёт быстрее любого многочлена.

Что падает вместе с ETH

SETH, сильная версия гипотезы, влечёт ETH, поэтому опровергнута и она. По словам авторов, из прежних работ теперь следуют теоретические субэкспоненциальные алгоритмы для Independent Set, Clique, Vertex Cover и Dominating Set за O(2^(dn)) при любом d больше нуля и новая нижняя оценка схем для класса E^NP. Claude прошёлся по литературе и нашёл больше 800 статей, где хотя бы один собственный результат доказан только при ETH или более сильной гипотезе.

Гипотезу об ортогональных векторах (OV) теорема при этом не опровергает, хотя SETH её влечёт. На OV держится заметная часть мелкозернистой сложности, включая оценку Backurs и Indyk, по которой редакционное расстояние нельзя вычислить за сильно субквадратичное время. Эта оценка остаётся в силе.

Две лаборатории, один день

В статье Anthropic есть оговорка: «независимо и одновременно с этим внутренняя модель OpenAI заявляет, что доказала похожий результат». OpenAI тоже называет датой находки 16 октября. По истории коммитов OpenAI выложила препринт и Lean-доказательство в репозиторий openai/math 26 октября в 20:52 UTC, а Anthropic влила свою формализацию в main на 6 часов 15 минут позже, в 03:07 UTC 27 октября. Прогон CI на ветке пул-реквеста при этом стартовал уже в 02:46. Статья Anthropic датирована 26 октября, на Hexagon она появилась в 05:12 UTC.