OpenAI заявляет, что её следующая модель Astra решила десять открытых математических проблем

Как заявляет OpenAI, внутренняя версия её следующей крупной модели под названием Astra получила десять новых результатов в области математики и теоретической информатики. Каждая из этих задач оставалась открытой не менее десяти лет. Компания опубликовала 249-страничную рукопись вместе с проверяемыми компьютером сертификатами на языке Lean 4 для каждого результата на GitHub.

Главным результатом стало первое в истории явное построение несофической группы, что разрешает центральный вопрос теории групп, остававшийся открытым с тех пор, как Михаил Громов ввел понятие софичности в 1999 году. За прошедшие с того момента 27 лет ни одному математику не удавалось доказать или опровергнуть существование несофических групп.

Остальные результаты охватывают сразу несколько областей. Astra опровергла гипотезу жесткости Конна для алгебр фон Неймана, доказала гипотезу Эрхарта об объеме и решила три задачи из знаменитого каталога Пала Эрдёша, включая задачу под номером 183 о многоцветных числах Рамсея. Модель также впервые с 1978 года улучшила общую верхнюю оценку плотности упаковки сфер в пространствах высокой размерности, доказала теорему о параллельном повторении для квантовых игр с двумя игроками и установила новые нижние оценки схемной сложности вычисления перманента.

Руководитель отдела математических исследований OpenAI Себастьен Бюбек подтвердил эти результаты в сети X, назвав их «прекрасными» и отметив, что каждое доказательство сопровождается сертификатом Lean и пошаговой цепочкой рассуждений (chain-of-thought). По данным OpenAI, общая стоимость вычислений для решения всех десяти задач составила около 2000 долларов по тарифам Sol API.

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

Для OpenAI это уже привычная практика. В мае компания объявила, что то же семейство моделей с долгосрочным планированием опровергло гипотезу Эрдёша о единичных расстояниях — задачу дискретной геометрии 80-летней давности. Лауреат Филдсовской премии Тим Гауэрс тогда заявил, что без колебаний рекомендовал бы это доказательство к публикации в Annals of Mathematics.

Томас Блум, курирующий проект erdosproblems, назвал в X новые десять результатов «важнейшей новостью», подчеркнув, что они имеют даже большее значение, чем контрпример к гипотезе о единичных расстояниях.

В OpenAI пока не сообщили, когда Astra станет доступна публично, охарактеризовав её лишь как «следующую крупную модель». Ряд наблюдателей, включая инвестора Марка Кречманна, предполагают, что Astra относится к серии GPT-6. Компания также предоставляет 100 000 научных исследователей бесплатный доступ к своим передовым моделям до 2027 года — этот шаг укрепляет её связи с академическим миром и одновременно концентрирует научную инфраструктуру на собственной платформе.

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