OpenAI Astra решила 10 открытых задач математики и теоркомпьютеринга

1 августа 2026 года OpenAI опубликовала результаты, которые мгновенно облетели математическое сообщество: десять решений задач, которые не продвигались по главному результату как минимум десятилетие, а в большинстве случаев значительно дольше. За всеми этими прорывами стоит не человек — а внутренняя версия Astra, следующей крупной модели OpenAI.

Что именно было решено

Задачи охватывают высокоразмерную геометрию, теорию кодирования, сложность арифметических схем, теорию групп, операторные алгебры, квантовую сложность, решёточную криптографию и экстремальную комбинаторику.

Вот все десять результатов в деталях:

1. Упаковка шаров в высокоразмерных пространствах (Sphere Packing)

Astra впервые с 1978 года улучшила общую верхнюю оценку плотности упаковки шаров в высокоразмерных пространствах. Новые асимптотические оценки достигают порога Кона–Элкиса (Cohn–Elkies threshold).

2. Двоичные и сферические коды (Binary & Spherical Codes)

Экспоненциально улучшены верхние оценки для двоичных кодов при любом минимальном расстоянии, а также соответствующие оценки для сферических кодов.

3. Несофические группы (Non-sofic Groups)

Построена конструкция несофической группы, что разрешает вопрос: допускает ли каждая группа конечные перестановочные аппроксимации. Это давняя открытая проблема теории групп.

4. Гипотеза Конна о жёсткости (Connes’s Rigidity Conjecture)

Построены бесконечно много попарно неизоморфных групп со свойством (T), имеющих одну и ту же групповую алгебру фон Неймана — таким образом, гипотеза опровергнута.

5. Сложность арифметических схем (Arithmetic Circuit Complexity)

Получены новые нижние оценки для вычисления перманента, включая оценку порядка n⁴/log n для формул.

6. Квантовое параллельное повторение (Quantum Parallel Repetition)

Экспоненциальная теорема о параллельном повторении распространена на все конечные двухигровые запутанные игры.

7. Задача о ближайшем векторе (Closest Vector Problem, CVP)

Прямая редукция из 3SAT даёт полиномиально-факторную твёрдость аппроксимации, что имеет последствия для декодирования и для решёточных задач, лежащих в основе постквантовой криптографии.

8. Гипотеза Эрхарта об объёме (Ehrhart’s Volume Conjecture)

Доказана резкая граница во всех размерностях для выпуклых тел, у которых барицентр является их единственной внутренней решёточной точкой.

9. Числа Рамсея для множества цветов (Multicolor Ramsey Numbers)

Получена сверхэкспоненциальная нижняя оценка для чисел Рамсея на многоцветных треугольниках, что закрывает задачу Эрдёша №183.

10. Экстремальные числа в теории графов (Extremal Number Conjectures)

Решены гипотезы о компактности и вырожденности из экстремальной теории графов — задачи Эрдёша №146 и №180.

Сводная таблица десяти результатов

Как это было сделано: Lean 4 и цепочки рассуждений

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

То, что отличает этот релиз от обычного PR-цикла «ИИ занялся математикой» — именно формализация в Lean 4. Каждый из десяти результатов поставляется с машинно-проверяемым сертификатом в репозитории OpenAI на GitHub, вместе с разбором рассуждений модели.

Человеческие исследователи затем доработали аргументы в рукописи и формализовали доказательства с помощью системы Lean.

Процесс работы Astra над задачами выглядел следующим образом:

graph TD
    A[Открытая математическая задача] --> B[Astra генерирует ключевой аргумент]
    B --> C[Команда OpenAI оформляет рукопись]
    C --> D[Astra формализует доказательство в Lean 4]
    D --> E[Публикация: статья + Lean-сертификат + walkthrough]
    E --> F[Машинная верификация любым желающим]

Стоимость: $2000 за десять прорывов

«Вычислительные затраты на генерацию всех десяти решений составили около $2000 по тарифам Sol API.» — OpenAI

По словам OpenAI, токены, использованные для генерации всех десяти решений, обошлись бы примерно в $2000 по тарифам Sol API. Цифра впечатляет на фоне того, что речь идёт о задачах, над которыми лучшие математики мира безуспешно работали десятилетиями.

Если даже большинство результатов выдержат проверку, интересный сдвиг не в победе в рейтинге. Дело в том, что стоимость атаки на давно открытую задачу начинает выглядеть как облачный счёт, а pipeline для таких атак выдаёт нечто, что формальный инструмент может проверить. Это меняет то, кто может попробовать и насколько быстро.

Вопрос авторства: кому принадлежат открытия?

OpenAI намеренно поднимает щекотливый вопрос — кто автор этих результатов?

Компания считает, что атрибуция должна честно отражать то, как был получен результат: заявлять о человеческом авторстве доказательства, полностью сгенерированного ИИ-системой, значит искажать как вклад системы, так и природу подлинного человеческого интеллектуального труда. OpenAI помогла подготовить рукописи и формализовать доказательства в Lean, и берёт на себя ответственность за их корректность, тогда как сами математические аргументы были сгенерированы системой.

В примечаниях к отдельным главам упомянуты живые математики, читавшие рукописи: Сорин Попа для главы о жёсткости Конна, а также Франсуа Шарль, Генри Брэдфорд, Майкл Чэпмен, Алон Догон и Франческо Фурнье-Фасио для главы о несофических группах. Они не являются соавторами — они критические читатели, и это различие имеет весомое значение в дискуссии об атрибуции.

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

Реакция сообщества

Руководитель отдела математических исследований OpenAI Себастьен Бубек подтвердил результаты в X, назвав их «красивыми» и отметив, что каждый поставляется с Lean-сертификатом и разбором цепочки рассуждений.

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

Astra — внутренняя модель; у внешних математиков пока не было времени проработать аргументы с той глубиной, которой обычно удостаиваются подобные гипотезы. Примет ли широкое математическое сообщество результаты, объявленные через пост в блоге, а не в рецензируемом журнале, — остаётся открытым вопросом, для ответа на который и была написана Лейденская декларация.

Что это значит для науки и технологий

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

Особенно важен результат по задаче CVP (closest vector problem — задача о ближайшем векторе): новые результаты о полиномиально-факторной твёрдости аппроксимации имеют прямое отношение к постквантовой решёточной криптографии. Это потенциально затрагивает разработку криптографических стандартов будущего, которые должны быть устойчивы к квантовым компьютерам.

Достижения в теоретической информатике могут улучшить возможности ИИ-моделей, повысить безопасность протоколов и создать новые коммерческие возможности в области шифрования данных, оптимизации и проектирования алгоритмов.

Если хотя бы большинство из этих результатов выдержат независимую проверку — стоимость атаки на открытую математическую задачу превращается в строчку в облачном счёте, а не в десятилетия карьеры.

Весь исходный код формализаций опубликован в открытом доступе на GitHub: github.com/openai/ten-proofs. Полный 249-страничный технический отчёт доступен по адресу cdn.openai.com/pdf/ten-proofs-oai.pdf.