В публикации OpenAI отметила, что по большинству выбранных проблем не было существенного прогресса как минимум десять лет. Среди заявленных результатов — доказательство существования несофиковых групп, решение гипотезы жесткости Коннеса и новые результаты в области упаковки сфер, теории кодирования, сложности арифметических схем, квантовых вычислений и экстремальной комбинаторики.
Результаты были получены с помощью внутренней версии модели Astra. Компания оценила стоимость поиска решений при использовании API Sol в $2000. После генерации аргументов ученые-люди подготовили научные рукописи, а модель помогла перевести доказательства в формальный язык Lean. При этом OpenAI не раскрыла технические детали Astra и сроки её публичного выпуска.
Менее чем через сутки после публикации пресс-релиза OpenAI исследователь Anthropic Левент Алпёге сообщил, что использовал общедоступную модель Claude Fable и без доступа к интернету смог решить пять из тех же математических задач. Среди них — задачи о сложности арифметических схем, квантовом параллельном повторении и ближайшем векторе.
Алпёге уже использовал ИИ для математических исследований ранее. В июле он заявил, что с помощью Claude Fable 5 ему удалось опровергнуть 87-летнюю гипотезу Якобиана — результат позже получил независимую проверку. В OpenAI также демонстрировали возможности своих моделей в математике: в мае компания сообщила о созданном ИИ опровержении гипотезы Эрдёша о числе различных расстояний, полученном при тестировании одной из неопубликованных моделей.
В OpenAI подчеркнули, что появление ИИ-систем, способных создавать математические доказательства, требует новых подходов к вопросу авторства. Компания считает, что полностью приписывать человеку доказательство, созданное ИИ, некорректно, поскольку это искажает вклад как модели, так и исследователя. OpenAI призвала исследователей изучить опубликованные работы, проверить предложенные идеи и использовать их как основу для новых открытий.

