6 октября 2026 года OpenAI опубликовала сотни математических результатов, созданных ещё не выпущенной внутренней моделью. По словам представителя OpenAI, почти все они получены из одного промпта для одного агента. Среди результатов, как сообщается, есть доказательство гипотезы Субхаша Хота — Unique Games Conjecture. Верно ли оно, пока никто не может сказать наверняка.
Что произошло
6 октября 2026 года OpenAI представила на GitHub 372 так называемых семейства результатов. Одно сообщение описывает их как работы из 17 областей математики и теоретической информатики. В репозитории числится 719 рукописей, при этом первый подсчёт исходил из 722, а после исправления три рукописи были отозваны. Таким образом, 372 — это семейства результатов, а не отдельные задачи, подчёркивает Technology.org.
Один промпт, один агент
Представитель OpenAI сказал изданию Scientific American, что модель получила почти каждый результат из одного промпта для одного агента; для некоторых результатов, правда, понадобилось несколько попыток. The Decoder оценивает средние вычислительные затраты примерно в три часа времени ChatGPT Pro на результат.
Доказательство Unique Games Conjecture
Скотт Ааронсон пишет в своём блоге Shtetl-Optimized, что в публикацию входит доказательство гипотезы Субхаша Хота — Unique Games Conjecture, и что у него есть сертификат Lean. В его записи этот день назван большим днём для математики. Но полной уверенности у него нет: «Or at least, we’re pretty sure that it’s a proof!» («По крайней мере, мы довольно уверены, что это доказательство».) Он также отмечает, что пока ни один человек не понял почти ни одного из этих доказательств; гонка за пониманием только началась.
Жена Ааронсона Дана Мошкович, которая много лет занимается этой гипотезой, по сообщению Technology.org, нашла представленное доказательство настолько трудночитаемым, что не смогла прочитать его без помощи ИИ.
Контекст
Lean — система проверки доказательств, которая проверяет логические шаги доказательства на компьютере. Сертификат Lean поэтому сильный признак, но не понимание: один комментатор указывает, что проверка успокаивает, но к пониманию отношения не имеет. Technology.org добавляет, что Lean проверяет лишь формальное утверждение, а не обязательно то, соответствует ли оно английскому тексту заявления.
Сколько результатов действительно проверено формально, источники сообщают по-разному. Implicator называет около 42 % главных результатов, примерно 300 из 719, с формализацией в Lean по состоянию на 7 октября; это число действует после исправления, при котором три рукописи были отозваны. AI Weekly называет только 162 из 722 рукописей с доказательствами, проверенными в Lean. Единого числа, значит, нет.
Публикация вызвала резкие реакции. Эндрю Сазерленд из MIT, по данным AI Weekly, сказал, что утверждения о решении задач одним агентом следует считать непроверенными, пока модель не выпущена и результаты нельзя воспроизвести. Тот же источник сообщает, что OpenAI отключила функцию «GitHub Issues» и удержала промпты, которые запрашивала консультативная группа. The Decoder сообщает, что некоторые математики упрекнули OpenAI в том, что она проигнорировала суть рекомендации консультативной группы, согласно которой сложные математические задачи не следует пробовать на внутренних моделях, и призвали к бойкоту.
Есть и независимая работа по той же теме. По одному сообщению, группа Дора Минцера из MIT в сентябре опубликовала на ECCC родственную версию гипотезы Хота «4 к 1», после того как до неё дошли слухи о доказательстве OpenAI.
Что это значит
Для математиков возникает проблема объёма: когда сотни рукописей появляются сразу, а понимает их почти никто, узким местом становится чтение и проверка. Замечание Ааронсона о том, что гонка за пониманием только началась, описывает именно это.
Для всех, кому приходится оценивать новости об ИИ, это сообщение — урок осторожности. Утверждение «один промпт, один агент» исходит от OpenAI; формальная проверка охватывает, в зависимости от подсчёта, лишь часть результатов; а сама модель не выпущена, поэтому со стороны никто не может проследить, как получены результаты. Считается ли доказательство установленным, решается не сертификатом или пресс-релизом, а тем, что специалисты могут его проследить.
Для исследовательской культуры реакции показывают, что дело не только в технике. Упрёк в том, что рекомендация консультативной группы проигнорирована, и призыв к бойкоту показывают: часть профессионального сообщества критикует и то, как проведена публикация.
Замечание о толковании: сведения опираются на новостные сводки и блоги. Независимой проверки самого доказательства Unique Games использованные источники не нашли, а подсчёты расходятся от источника к источнику.
Частые вопросы
Что именно означает «372 результата»?
Это 372 семейства результатов из 17 областей математики и теоретической информатики, а не 372 отдельные задачи. В репозитории числится 719 рукописей; первый подсчёт называл 722, после исправления три рукописи были отозваны.
Доказана ли Unique Games Conjecture?
OpenAI представляет доказательство, по словам Скотта Ааронсона — с сертификатом Lean. Но сам Ааронсон пишет, что он и другие «довольно уверены», что это доказательство; ни один человек пока не понял эти доказательства. Независимого подтверждения использованные источники не нашли.
Что такое Lean?
Lean — система проверки доказательств: она проверяет логические шаги доказательства на компьютере. Но она проверяет только формальное утверждение, а не обязательно то, совпадает ли оно с английским текстом заявления.
Почему сообщение вызывает споры?
Потому что неясно, сколько результатов проверено формально, и потому что, по одному сообщению, OpenAI удержала промпты, которые запрашивала консультативная группа. Математик из MIT требует верить утверждению «один промпт, один агент» лишь после того, как его удастся воспроизвести.
