OpenAI заявила, что её модель опровергла гипотезу ETH

OpenAI 26 октября объявила в своём блоге, что её внутренние модели опровергли гипотезу об экспоненциальном времени (ETH), доказали гипотезу о локальном сглаживании во всех размерностях и строго обосновали существование квантовой хромодинамики. Самостоятельно сейчас можно проверить только первые два результата: по ним в публичном репозитории OpenAI на GitHub лежат тексты и доказательства в Lean, системе машинной проверки доказательств, а материалы по физике внешняя группа пока не публикует. Наша проверка показала, что формальная теорема по ETH доказывает более слабую оценку, чем статья, а трое учёных, которым поручен разбор опровержения, сами пишут, что их участие нельзя считать сертификацией.

Кто и как выпускает результаты

Для каждого результата OpenAI позвала внешних экспертов-кураторов, и те предложили три разных способа выпуска:

• Математика. Гипотезу о локальном сглаживании Согге выдвинул в 1991 году: самая сильная фокусировка волн должна быть кратковременной. Из неё следуют гипотеза Какейи и гипотеза Стейна об ограничении, а в двух измерениях её в 2019 году доказали Гут, Ван и Чжан. Доказательство для всех размерностей модель выдала 18 октября, на следующий день его формализовали в Lean, и по совету эксперта OpenAI просто выложила вывод модели, как в релизе 6 октября. Организовать разбор исследователи могут сами.
• ETH. Результат проверяет и объясняет группа Рассела Импальяццо и Рамамохана Патури (оба UC San Diego) и Райана Уильямса (MIT), а материалы открыты всем. Модель нашла опровержение 16 октября, в Lean его формализовали днём позже. По просьбе группы OpenAI согласилась выложить все сырые данные и профинансировать конференцию о том, что работа значит для области.
• Физика. Группа под руководством Дэвида Гросса сама решает, что публиковать, и пока решила артефакты ИИ не выкладывать, а написать работу своими силами.

Уильямс в Bluesky уточнил, что модели группе не давали: «У нас нет доступа к их внутренним моделям. Мы получили только PDF». Там же он писал, что группа попросила OpenAI как можно скорее выложить все сырые данные по ETH, включая PDF и исходники на Lean.

Правила для внешних групп OpenAI формулирует так: без NDA, участники свободно обсуждают работу и публикуют выводы, участие добровольное и неоплачиваемое, говорят они только от своего имени. Академического авторства за открытия своих моделей OpenAI не ищет. В компании сами признают издержку схемы: выбор первых кураторов определяет, кто подключится раньше, и создаёт неравенство в доступе к информации. Эти группы дополняют недавний взнос OpenAI в 5 миллионов долларов в Simons Foundation на семинары и конференции по результатам ИИ.

Что на кону с ETH

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

Рукопись, которую мы прочитали, заявляет больше, чем пост. Её теорема 1.1, по словам авторов, опровергает не только ETH, но и SETH, Gap-ETH и NSETH, а также их вероятностные версии с ограниченной ошибкой. В приложении C из этого выводится нижняя оценка на схемы E^NP ⊄ SIZE(O(n)) через теорему Уильямса 2013 года, одного из трёх кураторов. Эти утверждения есть в PDF, но не в формализации.

Сами проверяющие в открытом письме пишут: «Наше участие не следует считать сертификацией утверждения. Результат такой значимости требует тщательной независимой проверки». Разбор, по их словам, не должен закреплять владение ни за компанией, ни за отобранной группой исследователей, «включая нас самих». Группа обещает репозиторий с выводами, блог и форму для отзывов.

В мае, когда OpenAI объявила об опровержении гипотезы Эрдёша о единичных расстояниях, отзывы математиков вроде Тима Гауэрса публиковала сама компания, и Scientific American отмечал, что эти комментарии запрашивала OpenAI. Нынешние оговорки проверяющих опубликованы в их собственном письме. Рукописи из этого репозитория уже правили после выпуска: 7 октября OpenAI отозвала три статьи из-за ошибки в знаке.

Физика: Янг-Миллс и КХД

Физический результат, по описанию OpenAI, строго доказывает существование ряда взаимодействующих квантовых теорий поля с калибровочными полями и фермионами в четырёх измерениях, включая квантовую хромодинамику и простейшую теорию великого объединения, которая содержит поля и фермионы Стандартной модели. Саму Стандартную модель нельзя продолжить на сколь угодно малые расстояния, поэтому речь идёт о её объединённом завершении. Попутно доказано существование чистой теории Янга-Миллса, а это часть одной из задач тысячелетия Института Клэя. Работа опирается на подход Балабана в конструктивной квантовой теории поля.

Доказательство для Янга-Миллса модель выдала 9 сентября, для КХД 18 сентября. Выпуск отложили до формализации, и формализацию существования Янга-Миллса закончили 16 октября. В группу Гросса, получившего Нобелевскую премию 2004 года за асимптотическую свободу, входят Майкл Дуглас, Артур Джаффе, Игорь Клебанов и Никита Некрасов. Джаффе вместе с Виттеном сформулировал эту задачу тысячелетия и был сооснователем Института Клэя. Все вопросы группа просит направлять на один адрес: YANGMILLS4D@gmail.com.

Авторский разбор

Что мы проверили

27 октября мы прочитали в публичном репозитории OpenAI формулировки в Lean по ETH и локальному сглаживанию, обе рукописи и историю коммитов, а проект ETH (Lean 4.34.1) просканировали на обходные конструкции. Полную сборку мы не провели, поэтому это чтение и поиск по коду, а не проверка ядром Lean.

Как мы проверяем истории

Опровержение ETH в Lean сформулировано в стандартном виде, лазеек мы не нашли, но формализована более слабая оценка времени, чем в статье. С локальным сглаживанием пост обещает больше, чем доказано: гипотезу Какейи Lean выводит во всех размерностях, а гипотезу Стейна об ограничении, которую OpenAI называет решённой во всех размерностях, только внутри предполагаемого диапазона. Даты открытий из поста репозиторий не подтверждает и не опровергает.

• ETH: для каждого k ≥ 2 одна детерминированная машина точно считает выполняющие наборы любой k-КНФ с n ≥ 20 переменными (3-SAT - случай k = 3), за время с показателем порядка n·(log log n)²/√log n. Рукопись от 25 октября даёт более сильную оценку n·log log n/√log n.
• В проекте ETH нет ни одного sorry, admit или axiom. Есть 11 определений opaque, у каждого явное значение, скрыты они ради скорости проверки. sorry, который обсуждали на Hacker News, стоит в файле-заготовке с одной формулировкой: так устроен репозиторий.
• Локальное сглаживание доказано для всех n ≥ 2 и 2 ≤ p < ∞ со сколь угодно малой потерей ε (нулевой только при p = 2). Гипотезы Какейи, максимальная Какейи, Бохнера-Рисса и Стейна о квадратичной функции выведены формально, ограничение только при строгих неравенствах. Аннотация рукописи и история изменений говорят то же: «внутри предполагаемого диапазона».
• Всё добавлено одним коммитом 26 октября в 20:35 UTC. PDF по ETH датирован «17 октября 2026, исправлено 25 октября 2026». В папке с цепочками рассуждений модели нет ничего ни по одному из двух результатов, так что из сырых данных пока открыты только PDF и исходники Lean.