722 работы закрытой модели OpenAI по математике. Что из них проверила машина?

722 рукописи, 372 семейства результатов, один коммит под названием Initial commit. Так 6 октября выглядел релиз OpenAI по математике: результаты внутренней модели за несколько недель легли в открытый репозиторий одним днём. А 21 сентября компания говорила о «более чем 100» решённых открытых задачах.

Месяц назад мы разбирали, как рой из 10 000 агентов OpenAI решал задачу Навье–Стокса, и главным там оказался машинный проверяющий: Lean. Вопрос к новому релизу тот же: где стоял проверяющий, а где его нет.

Что OpenAI выложила 6 октября

По README репозитория процедура была одна на почти все результаты: модели ставили открытые задачи, около 4 000 штук, в среднем на результат уходило три часа «мышления» ChatGPT Pro. Затем ответы сгруппировали в семейства и отобрали по значимости. Исключения названы прямо: область без нулей для дзета-функции и гипотеза Ходжа для CM абелевых многообразий получены не по общей схеме, а текст про Re(s) > 11/12 правили люди.

Имена в списке громкие. Квази-гипотеза Римана: дзета-функция и все L-функции Дирихле без нулей при Re s > 7/8. Показатель умножения матриц ω ≤ 9/4 над комплексными числами. Гипотеза Барнетта о гамильтоновых циклах. Контрпримеры к нескольким гипотезам Капланского. Формула Бёрча и Свиннертон-Дайера для части эллиптических кривых. Саму модель OpenAI обещает выпустить, по её словам, «responsibly», без даты.

Ещё одна деталь видна только по папкам. У каждой рукописи в названии стоит дата, и 564 из 722 датированы 23–27 сентября, из них 370 приходятся на два дня, 23 и 24 сентября. Ещё 112 помечены 5 октября, накануне публикации.

«Есть Lean» не значит «проверено»

Пересказы пишут, что «многие доказательства формализованы». Это правда, но формулировка скрывает три оговорки, которые OpenAI сама оставила в репозитории.

Первая: ссылка на Lean стоит у 235 семейств, а 137 опираются только на текст. README говорит о них прямо: «Some of the unformalized results could have issues», и обещает быстро исправлять.

Вторая: формализация часто покрывает главную теорему, а не всю статью. В описании Lean-части для квази-гипотезы Римана написано, что оценка 7/8 доказана формально, а поздние приложения статьи в формализацию не вошли.

Третья: каталог lean/formalization.yaml перечисляет 162 статьи с формализованным главным результатом. В поле охвата стоит «Partial progress», а в поле ревью status: unchecked. Lean гарантирует, что вывод корректен. Что формально записано ровно то утверждение, которое заявлено в заголовке статьи, проверяет человек, и по собственной отметке OpenAI эта проверка не сделана.

Что просили математики и что сделала OpenAI

21 сентября при Институте перспективных исследований в Принстоне собрали консультативную группу AGMAI, девять математиков. Решать, с какой скоростью OpenAI занимается математикой, группа не может, только советовать, как публиковать. 29 сентября она выпустила рекомендации по итогам больше 600 ответов от коллег и начала их с фразы, которую трудно прочитать иначе: «we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models».

Через неделю вышел релиз. Сверили по пунктам.

Сама группа 7 октября ответила сдержанно: релиз это «the beginning, not the completion, of the process of human understanding». Рекомендации она подтвердила ещё раз.

Как проверить доказательство OpenAI самому

Сильная сторона релиза в другом. Для формализованных результатов OpenAI приложила задания для comparator, инструмента Lean FRO, который сверяет доказательство с заранее записанным утверждением. Повторить проверку может любой. Собирать всю библиотеку сразу README не советует: в ней 122 140 файлов .lean, и сборка может упасть на системном лимите vm.max_map_count, поэтому проверяют по одному результату.

lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

На следующий день это сделал участник форума OpenAI davegoldblatt, а саму проверку провёл Claude Code. Итог: 2 924 модуля собраны без ошибок и предупреждений, доказательство приняли и comparator, и независимое ядро nanoda. Его собственная оговорка точнее любого заголовка: «this checks the Lean proof, not the paper». Один прогон, одна машина, и проверен формальный текст, а не статья.

Что из этого взять тем, кто работает с агентами

Наше мнение, с которым можно спорить: главный результат релиза не в 722 рукописях, а в том, как легко стало отличить проверенное от заявленного. Где есть comparator, проверка формальной части сводится к одной команде, и выполнить её может агент. Где его нет, остаются репутация компании и «could have issues». Мы окажемся неправы, если независимые математики за ближайшие месяцы найдут серьёзные ошибки именно в формализованной части: тогда граница проходит не там.

Для своих агентов вывод тот же, что и с роем Навье–Стокса. Тесты, типы и сборка работают как ваш Lean, а отдельный ревьюер работает как comparator: он проверяет, что сделано то, что просили, а не только то, что код компилируется. Как собрать такую проверку для AI-функции в продукте, показано в разборе экзамена и hillclimb для Claude API. Разводить исполнителя и проверяющего по разным субагентам учит курс по Claude Code.