OpenAI опубликовала 722 математические рукописи, созданные нереализованной внутренней моделью, описав эту работу как результат процесса, в основном выполненного одним промптом для одного агента. Статьи сгруппированы в 372 семейства связанных результатов, однако математики утверждают, что эти заявления нельзя полностью оценить, пока не будут опубликованы модель, промпты и дополнительные доказательства.

Эта публикация появилась на фоне того, как ИИ-лаборатории все чаще используют математику как полигон для проверки возможностей рассуждения передовых моделей, и она становится ранним тестом того, как следует публиковать, проверять и раскрывать ИИ-исследования.

Представитель OpenAI сообщил, что почти всё было получено из одного промпта, переданного одному ИИ-агенту, хотя для некоторых результатов могло потребоваться несколько попыток. Компания заявила, что предложила модели около 4 000 задач и отобрала те результаты, которые сочла достаточно значимыми для публикации.

Эндрю Сазерленд, математик из MIT, рассказал Scientific American, что к заявлению об одноразовомении следует относиться с осторожностью. «Пока они не выпустят модель и люди не смогут воспроизвести их результаты, я считаю, что любые заявления о решении задач с первого раза одним агентом следует считать неподтвержденными», — сказал Сазерленд. «Нам следует требовать доказательств».

Цифра 722 обозначает рукописи, а не решенные задачи. Семейство результатов может содержать основную теорему вместе с сопутствующими рассуждениями, следствиями или альтернативными доказательствами. OpenAI сообщила, что средний результат потребовал вычислительных ресурсов, эквивалентных примерно трем часам «размышлений» ChatGPT Pro. Это отличается от заявления компании о задаче Навье — Стокса в прошлом месяце, где были задействованы 10 000 координирующихся агентов, работавших 88 часов.

OpenAI опубликовала сокращенные резюме рассуждений для 10 результатов. Однако каталог формализаций в репозитории GitHub показывает, что лишь 162 из 722 рукописей на данный момент содержат проверенный компьютером основной результат. Это около 22% коллекции, и это означает, что результат переведен на Lean — программное обеспечение, механически проверяющее каждый логический шаг. Lean стал рабочим стандартом для проверенных машиной доказательств в математике, поэтому примерно560 все еще неформализованных рукописей представляют главный открытый вопрос этой коллекции.

OpenAI признала, что не все рукописи имеют формализации в Lean, и предупредила, что «некоторые неформализованные результаты могут содержать проблемы». Успешная проверка Lean подтверждает лишь то, что доказательство следует из формулировки в том виде, как она записана в Lean. Она не устанавливает, что формулировка соответствует исходной задаче, и не показывает, что результат нов или важен. Эти вопросы все еще требуют рассмотрения математиками.

Исследователи уже выразили обеспокоенность материалами и способом их публикации. Дмитрий Рыбин написал на X:

I was trying to read the OpenAI proof that chromatic number of a plane is >= 6. But it is totally unbelievable alien math? Somehow the model found that any K-coloring <=> "weakly measurable" K-coloring, which seems out of nowhere 1/2 pic.twitter.com/W13ScT3nel — Dmitry Rybin (@DmitryRybin1) October 7, 2026

Кит Адлер написал на X:

The openai/math repo has Issues turned off and has never accepted a pull request. That's disappointing. If you publish 722 manuscripts and ask for Lean formalisations, you need somewhere for people to send them. I'm formalising OpenAI's Saxl's Conjecture proof in Lean 4 against… — Keith Adler (@keithadler) October 7, 2026

Институт перспективных исследований в Принстоне, штат Нью-Джерси, также поставил под вопрос последствия математических работ, созданных ИИ. «Теперь ИИ может выдавать математические рассуждения в ситуациях, когда человек, задавший промпт, не в состоянии понять эти рассуждения, проверить их или взять за них ответственность», — говорится в заявлении института. «Мы считаем, что человеческое понимание математики остается первостепенно важным. Как в эту новую эпоху мы можем работать над новой парадигмой, в которой человеческое понимание математики является частью ответственной научной работы?»

Профессор Абхишек Саха отнесся к публикации более позитивно, написав: «Это очень важный день для математики». Он отметил, что большинство результатов относятся к категориям «выдающиеся достижения в рамках существующей программы» и «неожиданные прорывы». По его оценке, коллекция содержит интересные задачи, но результаты, сопоставимые с задачами тысячелетия — семью задачами с призом в 1 миллион долларов от Института Клэя, — в ней отсутствуют. Он выделил квазигипотезу Римана как единственную из 722, достигающую этого уровня значимости.

Саха написал на X:

Some further thoughts on the 372 results released by OpenAI today, across 722 manuscripts. If I were to classify theorems that mathematicians prove and publish according to their groundbreaking nature, I would (very roughly) divide them into four categories: A) Non-breakthrough… httpst.co/BA10SxBlx7 — Abhishek Saha (@ObhishekSaha) October 7, 2026

Публикация также не соответствовала рекомендациям, выданным консультативной группой при Институте перспективных исследований 29 сентября. Группа рекомендовала раскрывать название модели, промпты, обобщенную цепочку рассуждений, затраченное время и вычислительные затраты для каждого результата. OpenAI предоставила средние показатели вычислений и 10 резюме рассуждений, но не промпты. Компания заявила, что продолжает работу над ответственной публикацией модели.

Дэниел Литт, математик из Университета Торонто, занял противоположную позицию, утверждая, что нет причин требовать от OpenAI держать ответы на эти математические вопросы в секрете.

Anthropic в прошлом месяце выбрала иной подход, опубликовав на GitHub все 13 миллионов строк проверенного в Lean доказательства Великой теоремы Ферма. Эта работа формализовала теорему, опубликованную Эндрю Уайлсом в 1995 году, а не представляла новые математические результаты. Две публикации иллюстрируют раскол в стратегиях раскрытия информации в отрасли: с одной стороны — полное, проверенное машиной доказательство известной теоремы, с другой — большой массив новых заявлений с частичной формальной верификацией.

OpenAI сообщила, что будет добавлять формализации в Lean по мере их получения. На данный момент 162 из 722 рукописей имеют формализованный основной результат. Статус остальных теперь зависит от того, чего, по словам исследователей, им не хватает больше всего: выпуска модели, исходных промптов и независимых формализаций оставшихся рукописей.