Модель OpenAI опровергла гипотезу, на которой стоят сотни работ: доказательство проверено в Lean

На этой гипотезе держались сотни работ по вычислительной сложности: через неё формулировали условные оценки в теории графов, вычислительной биологии, базах данных и геометрии. Рушит гипотезу случай 3-SAT.

Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.

Что именно доказано

Счёт быстрее 2^n. В Lean зафиксирован алгоритм, который точно считает число выполняющих наборов k-CNF от n переменных за 2^(O(n(log log n)²/√log n)) и полиномиальный множитель сверху. Манускрипт от 25.10.2026 даёт оценку острее: когда условий в формуле не больше Dn, выходит 2^(O(n/√log n)), то есть субэкспонента при полиномиальной памяти.

Раньше гипотеза Какейи закрывалась по одному измерению за заход: два измерения взяли Guth, Wang и Zhang в 2019, три измерения закрыли Wang и Zahl в 2025. Теперь модели выдали гипотезу локального сглаживания Sogge 1991 года во всех размерностях, и из неё следуют и Какейя, и гипотеза Стайна о рестрикции. Опору даёт новое вспомогательное уравнение в частных производных.

Физика осталась закрытой. Там модели выдали строгое доказательство существования квантовых теорий поля с калибровочными полями и фермионами в четырёх измерениях, включая КХД, а подзадачей идёт существование чистой теории Янга–Миллса, одна из задач тысячелетия института Клэя. Артефакты модели по физике не публикуют: группа во главе с David Gross сначала напишет текст сама.

Как проверить у себя

Оба математических результата лежат в публичном репозитории openai/math: PDF с выводом модели на естественном языке и Lean-доказательства рядом. Заявок и NDA не нужно.

Порядок проверки описан в самом репозитории. Положите comparator, landrun и lean4export в PATH, из папки lean/ выполните `lake update`, `lake exe cache get`, затем `lake env comparator ComparatorChallenges/<Challenge>.json`. Всю библиотеку целиком компилировать не советуют, только малыми частями.

Статус формализации важнее анонса. В каталоге 721 манускрипт в 373 семействах, в Lean формализовано около 42% топ-результатов. 7 октября три манускрипта отозвали из-за ошибки в знаке, она сломала и две зависимые работы, ещё 14 поправили. Перед тем как опираться на работу, её статус видно в журнале истории репозитория.

Результаты получила неназванная внутренняя модель: задач ей задали около 4000, в среднем на один результат уходило три часа размышления на уровне ChatGPT Pro. Опровержение ETH будет разбирать внешняя группа под началом Russell Impagliazzo и Ramamohan Paturi, авторов самой гипотезы, вместе с Ryan Williams из MIT. OpenAI внесла $5 млн в Simons Foundation на воркшопы и программы для тех, кто разбирает результаты ИИ.

Дальше идёт пересчёт условных оценок в сотнях работ, которые ссылались на гипотезу как на данность.