27 октября 2026 г.
Exponential Time Hypothesis оказалась ложной: доказательство модели OpenAI проверено в Lean
Два результата из трёх OpenAI выложила публично 26.10.2026, а проверяют их внешние группы из UC San Diego и MIT.
16 октября модель OpenAI выдала доказательство того, что Exponential Time Hypothesis ложна. На следующий день доказательство прошло проверку в Lean.
На эту гипотезу опирались сотни статей об условной сложности задач в теории графов, вычислительной биологии, базах данных и вычислительной геометрии. Теперь вопрос, насколько быстрее такие задачи могут решаться, открыт заново.
Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.
Проверку отдали наружу. Месяц назад OpenAI выложила сотни манускриптов с решениями математических задач одной пачкой. Теперь у каждого результата есть внешняя группа, которую компания называет пастухами: ETH верифицируют Russell Impagliazzo и Ramamohan Paturi из UC San Diego вместе с Ryan Williams из MIT.
По требованию группы OpenAI выложила все сырые данные и обязалась оплатить конференцию о последствиях результата. NDA с участниками не подписывают, на авторство открытий своих внутренних моделей компания не претендует, участие добровольное и неоплачиваемое.
Проверить можно самому. Формализация лежит в репозитории openai/math. Поставьте comparator, landrun и lean4export в PATH, затем из каталога lean/ выполните `lake update`, `lake exe cache get` и `lake env comparator ComparatorChallenges/<result>.json`. Toolchain репозитория — leanprover/lean4:v4.34.1.
Второй публичный результат закрывает старую геометрическую задачу. Local smoothing умели доказывать только в двух пространственных размерностях (Guth, Wang, Zhang, 2019), а гипотезу Какейи в трёх.
Модели OpenAI выдали local smoothing для каждой размерности через новое вспомогательное дифференциальное уравнение. Вместе с ним закрылись гипотеза Какейи и гипотеза Стейна о restriction во всех размерностях.
Третий результат, существование QCD и чистой теории Yang–Mills, в открытый доступ не попал. Группа под руководством Дэвида Гросса, нобелевского лауреата по физике 2004 года, пишет текст сама, артефакты модели не публикуются, а обращения по теме идут на единственный адрес YANGMILLS4D@gmail.com.
В репозитории openai/math уже 721 манускрипт в 373 семействах, а Lean-формализация есть у 300 из 719 top-line результатов на 26.10.2026. Модель, которая их выдала, не названа. На один результат уходило в среднем 3 часа счёта ChatGPT Pro, а задач модели задали около 4000.
Сверху компания внесла $5 млн в Simons Foundation. Фонд раздаёт эти деньги на воркшопы, конференции и программы, где исследователи разбирают результаты, полученные ИИ.
Текст по Yang–Mills группа Гросса пишет сама, и до его выхода физический результат снаружи проверить нечем.
* Meta Platforms Inc. признана в РФ экстремистской организацией, её деятельность запрещена; Facebook и Instagram заблокированы. Meta AI и другие продукты компании — продукты этой организации.
Первоисточник