Внутренняя версия новой модели Astra от компании OpenAI получила десять важных результатов в математике. Разработчики описали эти достижения как существенный прогресс в геометрии высоких размерностей и теории кодирования. Компания выпустила объемную работу с подробными разборами, объясняя ход рассуждений нейросети. Исследователи также опубликовали специальный репозиторий с формализациями всех доказательств на языке Lean 4. Математические аргументы полностью сгенерировала внутренняя версия системы, работая без прямого вмешательства человека. Люди лишь совместно с нейросетью подготовили итоговые рукописи, передавая их научному сообществу. Представители OpenAI подчеркнули важность честной атрибуции, описывая процесс получения интеллектуальных результатов. Приписывание авторства человеку исказило бы реальный вклад ИИ, развивающего современную науку. Общий объем вычислений для поиска решений стоил бы около двух тысяч долларов. Эта оценка не включает последующую проверку, выполняемую математическим сообществом.

Один из заявленных результатов напрямую касается проблемы квантовой параллельной повторяемости. Эта концепция описывает изменение вероятности успеха при многократном запуске интерактивной игры. Нейросеть доказала экспоненциальную повторяемость для произвольных конечных квантовых игр с двумя участниками. Данный результат может оказаться важным для разработки новых криптографических протоколов. Еще одно достижение относится к сложной задаче поиска ближайшего вектора решетки. Модель получила более сильный результат о сложности приближенного решения этой задачи. Главным достижением публикации OpenAI называет успешное построение не-софической группы. Среди других результатов отмечены улучшенные оценки для упаковки шаров в высоких размерностях. Исследователи также представили новые нижние границы в арифметической схемной сложности. Компания заявила о нахождении контрпримера к известной гипотезе жесткости Конна.

Формализация доказательств на языке Lean значительно снижает риск обычных логических пробелов. Опубликованный код можно легко собрать и проверить машинными методами. Однако автоматическая проверка совершенно не заменяет полноценную научную экспертизу. Математикам еще предстоит оценить точность соответствия формальных утверждений исходным задачам. OpenAI прямо сослалась на одобренную Международным математическим союзом Лейденскую декларацию. Этот документ призывает сохранять прозрачную атрибуцию при использовании ИИ в исследованиях. Компания берет на себя полную ответственность за корректность опубликованных материалов. При этом сами математические аргументы приписываются системе, а не людям. Издание The Quantum Insider отметило отсутствие даты публичного запуска модели Astra. Разработчики пока не предоставили нейросеть для независимого тестирования внешними экспертами.