OpenAI выложила сотни AI-рукописей по математике
Компания говорит, что внутренняя frontier-модель получила новые результаты и Lean-формализации, но математики уже спорят, помогает ли такой релиз науке.
OpenAI опубликовала большую коллекцию математических рукописей и proof artifacts, созданных внутренней frontier-моделью. Компания выкладывает материалы на GitHub: часть доказательств формализована в Lean, а рядом опубликованы детали о том, как модель получала результаты.
В репозитории говорится о 719 рукописях, собранных в 372 семейства результатов. OpenAI пишет, что модели дали около 4 000 задач, а средний результат потребовал compute, примерно сопоставимого с тремя часами ChatGPT Pro thinking. Компания подает релиз как шаг к более сильным AI-инструментам для ученых и говорит, что работает над ответственным выпуском самой модели.
Главный вопрос здесь не только в заявленной математике. Вопрос в проверке. OpenAI прямо отмечает, что не все результаты имеют Lean-формализацию, а в репозитории сказано, что в части неформализованных материалов могут быть ошибки. То есть релиз стал проверкой того, может ли AI-сгенерированная научная работа проходить ревью, исправляться и цитироваться без перегруза для людей, которые реально понимают область.
Этот конфликт уже виден публично. Association for Human Mathematics раскритиковала массовую публикацию и заявила, что такой формат сам по себе не доказывает прогресс математики. Для AI-индустрии вывод простой: frontier-модели выходят из benchmark-математики в реальные исследовательские workflows, но процесс проверки становится не менее важным, чем сама capability модели.
OpenAI
