Anthropic опубликовала препринт «A 2^o(n) Time Algorithm for 3-SAT», автор которого указан как «Claude, Anthropic»: внутренняя исследовательская модель компании 16 октября 2026 года нашла детерминированный алгоритм, решающий 3-SAT и подсчётную задачу #3-SAT за субэкспоненциальное время 2^O(n log log n / sqrt(log n)). Если конструкция корректна, это опровергает гипотезу экспоненциального времени (ETH, Impagliazzo–Paturi). Доказательство формализовано в Lean 4 и проверено ядром Lean и независимым чекером nanoda, однако целиком его ещё не проверял ни один человек, а в файле Challenge.lean остаются два sorry.

image
image
image

Что произошло

Препринт hexagon:2610.00577v1 появился на математической платформе Hexagon 27 октября 2026 года, версия v1 подана Jelani Nelson от имени Anthropic. В нём описан детерминированный алгоритм для 3-SAT и более сложной подсчётной задачи #3-SAT, найденный внутренней исследовательской моделью Claude: ядро решения получено без человеческих подсказок в сессии объёмом около 14 миллионов выходных токенов. Формализация занимает 1050 модулей поверх Mathlib в Lean v4.33.1 и выложена в официальном репозитории anthropics/formal-math в папке eth, коммит 16a5ce4 от 27 октября 2026, 03:07 UTC; локальную корректность подтверждают ядро Lean и независимый чекер nanoda. По заявлению Anthropic, Claude Opus 5.5 способен заново вывести результат по короткому техническому наброску — это заявленная частичная воспроизводимость. OpenAI днём ранее сообщила, что её модель тоже опровергла ETH, однако опубликованного артефакта, который подкреплял бы это заявление, нет.

Контекст

Гипотеза экспоненциального времени (ETH, Impagliazzo–Paturi) утверждает, что 3-SAT нельзя решить существенно быстрее полного перебора; она и её усиление SETH служат отправными точками для сотен доказательных нижних границ в теории сложности вычислений, которые выводятся сведением из этих гипотез. Поэтому заявка с субэкспоненциальным алгоритмом бьёт по фундаменту поля, а решение вдобавок подсчётной задачи #3-SAT усиливает результат: посчитать решения сложнее, чем установить их существование. Машинная проверка в такой работе двухуровневая: ядро Lean удостоверяет каждый шаг формализации, но проверяется лишь то, что фактически формализовано, а маркер sorry означает незавершённый фрагмент доказательства. Соответственно, «машинно проверено» здесь — сильная гарантия локальной корректности построения, но она не заменяет независимой экспертизы со стороны сообщества. Отдельно важен формат публикации: препринт, код и Lean-формализация выложены одновременно и открыто, поэтому распределённый аудит может начаться сразу, а не после рецензирования.

Почему это важно для индустрии

Если конструкция устоит, ложными окажутся и ETH, и её усиление SETH, а вместе с ними потребуют перепроверки сотни работ с нижними границами, выведенными сведением из этих гипотез, — большой пласт теории сложности придётся пересматривать. Для инженеров и продуктовых команд главный актив — не сам алгоритм, а воспроизводимый рабочий процесс: длинная автономная сессия агента завершается машинной верификацией, и весь цикл «агент генерирует — формализация в Lean 4 — независимая проверка чекером» открыт в репозитории, где любая команда может разобрать его и перенести на свои домены: код, договоры, вычисления. Реалистичный сценарий на ближайшие месяцы — аудит формализации квалифицированными теоретиками и формализаторами: sorry либо закроют, либо они станут точкой провала всей конструкции, параллельно вероятны попытки извлечь человеко-читаемое доказательство. Гонка лабораторий за «автономные открытия» вышла в публичную плоскость, и обе компании явно используют её в позиционировании флагманов, что подталкивает развитие платформ для research-агентов и формальных чекеров как сервиса. Непосредственного продуктового эффекта нет: это препринт и репозиторий, а не продукт — ни API, ни цен, ни данных о задержке и пропускной способности.

Почему это важно для пользователей

Для читателя это наглядный пример того, как большие языковые модели становятся инструментом математических открытий, но прочтение требует поправок. Алгоритм не ускоряет практические SAT-солверы: результат чисто асимптотический, выигрыш над перебором появляется лишь при числе переменных порядка 10^10000, тогда как полный перебор непрактичен уже при примерно ста переменных; к решению проблемы P против NP он также не приближает, так что фраза «SAT теперь решается быстро» была бы искажением новости. Практически доступное действие сегодня одно — склонировать anthropics/formal-math по указанному коммиту и разобрать пайплайн формализации как референс: перенос схемы «агент генерирует — Lean 4 проверяет» на собственные задачи доступен уже сейчас. Ключевой навык при чтении подобных заявлений — проверять наличие машинно проверяемого артефакта, а не только текст анонса: открытая формализация позволяет каждому убедиться в локальной корректности самостоятельно. Сам препринт ничего не меняет в повседневных инструментах и сервисах, которыми вы пользуетесь.

Что пока неизвестно / ограничения

Формальное доказательство не завершено: в Challenge.lean остаются два sorry, то есть на этих местах приняты недоказанные допущения. Формализацию писали и проверяли сами ИИ-модели, и на момент публикации ни один человек не проверил её целиком; заявленная воспроизводимость через Claude Opus 5.5 опирается на модели того же семейства и пока не является независимой людской проверкой. Заявление OpenAI об аналогичном опровержении ETH не подкреплено опубликованным артефактом, поэтому считать его независимым подтверждением результата Anthropic нельзя. Наконец, это препринт версии v1, не прошедший рецензирования, так что итоговое суждение о корректности всей конструкции остаётся за математическим сообществом.

Источники

Автор

Look at AI, редакция