OpenAI опубликовала 722 математические рукописи, объединенные в 372 семейства, которые созданы невыпущенной внутренней frontier-моделью и выложены в открытый репозиторий openai/math под лицензией Apache-2.0. Коллекция включает формализации доказательств в Lean, исходные файлы и сокращенные описания рассуждений модели, полученные по итогам примерно 4000 исследовательских задач. Для бизнеса это важно как проверка новой схемы исследований: массовый выпуск машинных результатов с доказательствами, проверяемыми компьютером.
Как устроен репозиторий из 722 работ
Каталог группирует связанные работы в семейства, куда могут входить основной результат, сопутствующие рассуждения, следствия или альтернативные доказательства, причем каждое семейство отнесено к математической дисциплине. Каталог preprints содержит PDF, исходники, инструкции по цитированию и сборке, а отдельная библиотека Lean и каталог формализации описывают доступные доказательства, связанные статьи и конфигурации проверки. Каждый каталог рукописи включает блок BibTeX, а история версий сохраняется: прежние выпуски остаются доступными, исправления выходят как новые версии.
Согласно README, подавляющее большинство результатов получено по единой процедуре с помощью одной невыпущенной внутренней модели, при средних затратах около трех часов мышления ChatGPT Pro на результат. OpenAI расширила эти оценки после насыщения результатов на прежних математических тестах, причем часть выводов опирается на более ранние результаты ее моделей. Два исключения вышли за рамки стандартной процедуры: работа о зоне без нулей дзета-функции Римана и доказательство гипотезы Ходжа для CM абелевых многообразий. Материал о зоне Re(s) > 11/12 для дзета-функции был отредактирован человеком для читаемости.
Покрытие проверкой неравномерно, и это определяет порядок возможного использования коллекции. Многие рукописи сопровождаются формализациями в Lean, позволяющими проверить доказательства компьютером, однако заметная часть пока их не имеет. OpenAI предупреждает, что в неформализованных результатах возможны ошибки, и обещает быстро исправлять их, добавляя новые формализации по мере готовности. Репозиторий также содержит 10 сокращенных описаний рассуждений — от показателя иррациональности числа пи и гипотез Малера до спиновых стекол, факторов свободных групп и системы Власова-Максвелла.
Что выпуск меняет для компаний, использующих ИИ
Для компаний, применяющих ИИ в исследованиях, инженерии и аналитике, практическое изменение — доступ к открыто лицензированным рукописям и машинопроверяемым артефактам, а не только к заявлениям. Команды могут скачать PDF и исходники, изучить доказательства Lean и цитирования, затем решить, стоит ли тратить время специалистов. Небольшой компании это удешевляет первичный отбор сложной математики, а крупная организация может поручить экспертам проверку отдельных семейств и связать формализованные фрагменты с моделированием, расчетами или оптимизацией.
Та же структура задает ограничения, которые руководителям следует учитывать в решениях. Неформализованные рукописи требуют больших затрат на проверку, а сама OpenAI предупреждает о возможных ошибках, поэтому коллекция — это не собрание устоявшихся фактов. Неполон и контекст: OpenAI раскрыла примерное число попыток и средние вычисления в единицах ChatGPT Pro, но не дала название модели, промпты, время и стоимость по каждому результату, как просили математики. Перед использованием нужно выяснить, какие семейства имеют проверки Lean, что менялось между версиями и есть ли независимая экспертиза.
Признаком закрепления тренда станет перенос коллекции в научный репозиторий вне контроля лаборатории и выпуск модели-автора с заявленными мерами безопасности. OpenAI говорит, что изучает альтернативы на базе сообщества, профинансирует семинары и программы по пониманию результатов ИИ и работает над ответственным выпуском модели. Если появятся постоянные идентификаторы, fuller раскрытие методики и независимая проверка превратят машинную математику в более удобный объект закупки и аудита для корпоративных исследований.
