ИИ опроверг гипотезу экспоненциального времени — дважды, в один день

16 октября две лаборатории, каждая у себя, получили от внутренних моделей один и тот же вывод: гипотеза экспоненциального времени, ETH, ложна. Через несколько дней обе выложили статьи и доказательства на языке Lean. Репозиторий Anthropic честно предупреждает: это исследовательский артефакт, он не поддерживается и правок не принимает. Звучит как табличка «стройка закрыта» на месте, где только что что-то рухнуло.

Что за гипотеза и что именно нашли

ETH считалась почти аксиомой теории сложности. Она утверждает, что часть задач, например выполнимость булевых формул, нельзя решить быстрее экспоненциального времени. Её описывают как более сильного родственника вопроса P против NP. На ETH опираются сотни работ: они выводят условные оценки сложности в теории графов, вычислительной биологии, базах данных и вычислительной геометрии. Если фундамент поплыл, под вопросом все эти «быстрее нельзя».

Anthropic опубликовала статью «A 2^{o(n)} Time Algorithm for 3-SAT». Автором указан Claude, результат получен внутренней исследовательской моделью. Детерминированный алгоритм решает 3-SAT на n переменных за время 2^{o(n)}, то есть заметно быстрее экспоненты. Более трудную задачу #3-SAT, подсчёт выполняющих наборов, он решает за 2^{O(n log log n / √log n)}. Оговорка стоит в самом начале: результат чисто асимптотический и о скорости на реальных формулах ничего не говорит. OpenAI выложила свой препринт «The Exponential Time Hypothesis is False» в репозитории openai/math. Какими методами шла её модель, в открытых материалах не сказано.

Как это проверяют машиной

Формализация Anthropic написана на Lean 4 моделями. Версии Lean и Mathlib закреплены (v4.33.1). Главный файл MainResults.lean короткий, без доказательств, и формулирует на машинах Тьюринга из Mathlib две вещи: «ETH ложна» и Теорему 1 статьи об алгоритме подсчёта для k-CNF формул. Машина проверяет доказательство, но не проверяет, что формулировка честно соответствует статье. Эту сверку делает человек, поэтому файл и держат коротким.

Повторить проверку можно самому:

• установить elan и в папке eth выполнить lake exe cache get, lake build и lake env lean scripts/PrintAxioms.lean;
• сборка занимает около 8 минут на 24 виртуальных CPU, пик памяти около 7 ГБ;
• два предупреждения «declaration uses sorry» ожидаемы: они относятся к Challenge.lean, где теоремы намеренно оставлены без доказательств;
• проверка аксиом должна показать три стандартные: propext, Classical.choice, Quot.sound;
• полная проверка в CI запускает Comparator: он сверяет формулировки с Challenge.lean и перепроверяет доказательства вторым, независимо написанным ядром nanoda.

Отдельно в репозитории лежит сжатая схема идеи. По словам авторов, по ней Claude Opus 5.5 на высоком уровне усилий может воспроизвести опровержение. Время сжатия тензорных сетей на K_K с λ битами на ребро оценивается как 2^{e(K)·K²λ}·poly(λ), а рекурсия даёт e(9K^16) ≤ 0.9·e(K) + O(1/K). Узлы раскладываются в сетку, диагонали прямоугольников образуют swap, а для одного бита SWAP = I − 2·singlet. Но схема, как признают авторы, даёт лишь оценку O(2^{δn}) для любого δ > 0, а не более сильные границы из статьи.

OpenAI: три результата и новый способ их выпускать

OpenAI в тот же период объявила о трёх результатах внутренних моделей: в гармоническом анализе, теории сложности и квантовой теории поля. Вместо обычного релиза она передала их внешним экспертам, которых называет «шепердами». Те собирают научные группы, чтобы результаты объяснить. Рукописи компания называет «сырыми научными данными», которые ещё предстоит превратить в понимание.

Стратегии выпуска подсказали сами эксперты, и они разные. По математике публикуется только ИИ-вывод, а разбор исследователи организуют сами. По информатике группа соавторов сразу публикует доказательство на естественном языке и формализацию в Lean, а вывод доступен всем. По физике группа сама решает, что и когда выпускать, и пока придерживает ИИ-материалы. OpenAI признаёт, что не знает, какой подход лучше, и просит обратной связи. Ещё одна оговорка: выбор первых «шепердов» определяет, кто включится первым, и создаёт асимметрию информации.

У коллабораций четыре принципа:

• Прозрачность. Участников не обязывают подписывать NDA, они могут обсуждать работу и публиковать выводы.
• Без академического авторства. OpenAI не претендует на авторство открытий своих моделей, а приглашение стать «шепердом» не означает, что эксперт сделал исходное открытие.
• Признание. Группа получает его за понимание и тексты и следит, чтобы работа корректно ссылалась на чужие идеи и методы.
• Независимость. Участие добровольное и неоплачиваемое, стороны не говорят друг за друга.

Математика и физика

Модели OpenAI доказали гипотезу локального сглаживания, сформулированную Соггом в 1991 году, для любой размерности. Она описывает поведение волн в момент фокусировки: самая сильная фокусировка должна быть кратковременной. По заявлению компании, отсюда следуют гипотеза Какейи и гипотеза Штейна об ограничении во всех размерностях. Раньше было известно два случая: для двух измерений (Гут, Ван, Чжан, 2019) и для трёх (Ван и Залл, 2025). В основе доказательства новое вспомогательное уравнение в частных производных.

В физике заявлено строгое доказательство существования квантовой хромодинамики и объединённого расширения Стандартной модели в четырёх измерениях, а также чистой теории Янга — Миллса, которая входит в задачу тысячелетия Института Клэя. Работа опирается на подход Балабана в конструктивной квантовой теории поля. Группу возглавляет Дэвид Гросс, нобелевский лауреат 2004 года за асимптотическую свободу. В неё входят Майкл Дуглас, Артур Джаффе (соавтор постановки задачи тысячелетия), Игорь Клебанов и Никита Некрасов. По ETH работу проверяют Рассел Импальяццо, Рамамохан Патури и Райан Уильямс. Они выдвинули два условия, и OpenAI их приняла: опубликовать все сырые данные и профинансировать конференцию о последствиях для области.

Доказательство для КХД получено 18 сентября. Публикацию физики отложили до конца формализации, потому что объём работы большой. Независимую компьютерную проверку, по данным компании, прошли математика, информатика и Янг — Миллс. Кроме того, OpenAI направит 5 млн долларов в Simons Foundation: фонд будет распределять их на семинары, конференции и программы по осмыслению этих результатов.

Что с этим делать

Прямого эффекта для вашего монтажного стола нет, и если верить самим авторам, практических последствий ETH пока никто не может оценить. Нас зацепило другое: схема. Лаборатории называют выдачу модели сырьём, а работой считают превращение его в понимание, причём руками людей, которые за это отвечают. Это очень знакомая сцена: генерация даёт материал, а автором становится тот, кто умеет отличить находку от шума и объяснить, почему она держится. Пожалуй, и нам пора привыкать к вопросу, который в науке задают уже сейчас: чем проверено и кто подпишется.

Модели закрывают задачи быстрее, чем люди успевают их прочесть.