Anthropic: внутренняя модель Claude опровергла Exponential Time Hypothesis
2026-10-27 Anthropic опубликовала статью и формальное доказательство результата, полученного внутренней исследовательской моделью Claude. По данным компании, найден детерминированный алгоритм для 3-SAT со временем работы 2^o(n), что опровергает Exponential Time Hypothesis. Более сильный результат касается подсчёта решений #3-SAT и заявляет оценку 2^O(n log log n / √log n). Название и характеристики использованной модели не раскрыты.
Материалы размещены в официальном репозитории Anthropic: проект включает статью, 153 191 строку формализации на Lean 4 и инструкции для проверки. Доказательство собирается на Lean 4.33.1 и Mathlib 4.33.1, а дополнительная проверка использует Comparator и независимо реализованное ядро nanoda. Код опубликован по лицензии Apache 2.0. Независимой научной оценки результата пока нет; кроме того, Anthropic отдельно предупреждает, что оценка носит асимптотический характер и не означает практического ускорения решения задач.
Для бизнеса это сигнал о росте возможностей моделей в формальной математике, проверке алгоритмов и подготовке доказуемых технических результатов. Потенциальные пользователи — исследовательские подразделения, разработчики средств верификации и компании с критичными алгоритмами. Цена доступа к внутренней модели не опубликована, поэтому оценить стоимость такой работы в USD или рублях нельзя. Основной риск — принять теоретическое достижение за готовый коммерческий инструмент; до появления доступа и внешней проверки результат следует использовать только как ориентир для пилотных исследований.
Дальше важно отслеживать независимую экспертизу статьи, воспроизводимость формализации и возможный выпуск исследовательской версии Claude. Также пока нет подтверждённых данных о стоимости вычислений, числе использованных токенов и сроках выполнения работы.