OpenAI представила модель Astra: ИИ решил 10 фундаментальных математических задач за $2000

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

Главным достижением стало построение первой в истории явной конструкции несофической группы. Вопрос об их существовании стоял открытым с 1999 года, когда Михаил Громов ввел понятие софичности. Это открытие может существенно продвинуть исследования в фундаментальной теории групп.

Все десять доказательств были формально верифицированы в системе Lean 4 — инструменте, сочетающем язык программирования и проверку теорем. На GitHub опубликованы 249-страничный манускрипт и машиночитаемые сертификаты для каждого результата, что исключает ошибки и позволяет независимую проверку каждого шага рассуждений.

По оценке OpenAI, на поиск всех решений ушло около 2000 долларов по тарифам API. Математик Томас Блум из Манчестерского университета оценил итоги как «большую новость», превосходящую по значимости майскую публикацию о контрпримере к гипотезе о единичных расстояниях. При этом он подчеркнул: ИИ-системы опираются на десятилетия наработок математического сообщества и не заменяют ученых.

Задачи премии тысячелетия Astra пока не атаковала серьезно, однако компания планирует продолжить эксперименты в этом направлении и обещает опубликовать подробную техническую документацию по модели. Ранее ИИ OpenAI уже опроверг гипотезу Эрдеша 1946 года — став первым автономным решением центральной задачи комбинаторной геометрии.