OpenAI выложила на GitHub 722 математические работы от закрытой модели

OpenAI несколько дней назад выложила на GitHub 722 математические работы, которые сгенерировала внутренняя, ещё не вышедшая frontier-модель. Темы: теория чисел, алгебраическая геометрия, анализ, комбинаторика. Часть результатов сопровождается формальными доказательствами на Lean. Китайское издание Jiqizhixin формулирует последствия жёстко: ИИ начал производить новую математику быстрее, чем математики успевают её понимать, а сообществу понадобятся годы, чтобы всё это переварить.

Что именно опубликовано

Сам масштаб бросается в глаза. Семьсот с лишним работ одним пакетом, в нескольких разделах математики сразу. Обычно такие объёмы набираются годами и десятками авторов.

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

• 722 работы в открытом репозитории на GitHub
• Источник: внутренняя неопубликованная модель OpenAI
• Направления: теория чисел, алгебраическая геометрия, анализ, комбинаторика
• Часть работ имеет формальную верификацию в Lean
• Статус независимой экспертизы: в доступном материале не указан

Узкое место сместилось на проверку

Lean здесь играет роль страховки. Это система доказательств, в которой каждый шаг проверяет компилятор. Если доказательство собралось, логических дыр в нём нет. Но остаются вопросы, которые машина не снимает. Формализовано ли именно то утверждение, которое заявлено в статье? Интересен ли результат или это побочное следствие известного? Попадает ли он в живую линию исследований?

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

Вторая часть заголовка Jiqizhixin о том, что у математиков «исчезли исследовательские проекты». Механика простая. Если модель закрывает задачу, над которой аспирант собирался работать полтора года, тема обесценивается раньше, чем он успел защититься. Это оценка издания, а не подтверждённый факт по конкретным людям, но логика понятна. Больше всего рискуют те, кто занимается техническими, хорошо формализуемыми задачами.

Как с этим работать

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

Журналам и арXiv-подобным площадкам придётся определиться с политикой. Принимать ли тексты, написанные моделью, и требовать ли формальное доказательство как условие рассмотрения. Без этого поток машинных работ просто забьёт очередь.

Инженерам и руководителям команд полезен более широкий вывод. Формальная верификация выходит из академической ниши и становится способом принимать результаты ИИ без доверия на слово. Тот же принцип применим к коду и критичным системам.

Наконец, пока нет независимых разборов, имеет смысл воздерживаться от громких выводов. Главный показатель на ближайшие месяцы: какая доля из 722 работ выдержит проверку и сколько из них окажутся содержательными, а не просто корректными.