OpenAI выложила 722 математические рукописи — но не все доказательства уже проверены
OpenAI опубликовала на GitHub большой каталог математических работ, созданных внутренней нераскрытой моделью. В нём 722 рукописи, сгруппированные в 372 семейства результатов. Одно семейство может объединять основной результат, дополнительные аргументы, следствия или альтернативные доказательства.
Компания пишет, что перед релизом консультировалась с независимой Advisory Group on Mathematics and Artificial Intelligence при Институте перспективных исследований. Материалы опубликованы с правилами для версий и цитирования; OpenAI также ищет другие площадки, соответствующие рекомендациям группы.
Масштаб впечатляет, но статус этих материалов важнее цифры. Сам репозиторий прямо предупреждает: результаты находятся на разных стадиях проверки. Многие работы формализованы в Lean — языке, где доказательство можно проверить программно, — однако это сделано не для всех рукописей.
Формальная проверка — сильный, но узкий сигнал: она относится к конкретному оформленному доказательству, а не автоматически ко всему каталогу и его научной значимости. OpenAI отдельно допускает, что в неформализованных результатах могут быть ошибки.
Около 4 000 попыток
По описанию проекта, в ходе оценки модели ей поставили примерно 4 000 задач. Большинство результатов получили по одной и той же процедуре; в среднем на один результат ушёл вычислительный бюджет, сопоставимый примерно с тремя часами режима рассуждений ChatGPT Pro.
Каталог не равен 4 000 решённым задачам: OpenAI отобрала из попыток результаты достаточной значимости, затем собрала связанные работы в семьи и отдельные рукописи. Для десяти результатов компания также выложила сокращённые сводки рассуждений модели.
Открытый архив вместо окончательного вердикта
В репозитории лежат PDF, исходники, карта рукописей, инструкции по цитированию и каталог формализаций. OpenAI обещает добавлять Lean-проверки по мере появления и сохранять историю публичных версий: исправления будут выходить новыми версиями, а прежние останутся доступными.
Это полезный шаг для математиков: теперь заявления можно читать, проверять и оспаривать предметно. Но публиковать каталог — не то же самое, что получить независимое рецензирование всех 722 рукописей. Корректная формулировка пока такая: OpenAI открыла большой набор заявленных результатов, часть которых имеет машинную формальную проверку, а часть ещё ждёт такой проверки и внешнего разбора.
