Если новая публикация OpenAI выдержит проверку математического сообщества, она может оказаться одним из самых интересных событий года в AI. Не из-за очередного бенчмарка, а из-за возможного сдвига в самом процессе исследования.
1 августа 2026 года OpenAI заявила необычное: внутренняя версия Astra, её следующей большой модели, получила новые результаты по десяти открытым задачам математики и теоретической информатики.
По словам компании, речь о задачах, где по основному результату не было заметного продвижения как минимум десятилетие, а в ряде случаев значительно дольше. Среди областей: геометрия в высоких размерностях, теория кодов, теория групп, операторные алгебры, квантовая сложность, криптография на решётках и экстремальная комбинаторика.
Что именно утверждает OpenAI
Важна не только сама сводка результатов, но и способ работы. По версии OpenAI, модель нашла ключевые идеи доказательств. Затем люди готовили черновики статей с помощью той же модели, а на финальном шаге модель формализовала доказательства в Lean.
Lean — это среда proof assistant. Вместо математического текста, который читают и интерпретируют люди, доказательство записывается так, что машина может формально проверить его корректность.
Это не значит, что сообщество обязано принять каждое утверждение автоматически. Но уровень серьёзности публикации меняется: есть статья, есть открытый репозиторий и есть сертификаты, которые можно проверить.
Что вошло в список результатов
- Новые границы плотности упаковки шаров в высоких размерностях.
- Улучшенные границы для двоичных и сферических кодов.
- Построение non-sofic группы.
- Контрпример к гипотезе жёсткости Конна.
- Новые границы сложности арифметических схем.
- Теорема о квантовом parallel repetition для игр двух игроков.
- Результат о трудности приближения задачи ближайшего вектора в решётках.
- Результат по объёмной гипотезе Эрхарта.
- Суперэкспоненциальная нижняя граница для многоцветных чисел Рамсея.
- Результаты экстремальной комбинаторики вокруг гипотез компактности и вырожденности.
Почему это важно за пределами математики
Годами разговор про AI шёл о моделях, которые пересказывают, пишут, переводят или помогают с кодом. Здесь заявка другая: модель предлагает новый математический аргумент для открытой задачи.
Граница между системой, которая упорядочивает существующее знание, и системой, которая задаёт новое направление исследования, становится менее чёткой.
Если результаты подтвердятся, процесс исследования может измениться. Учёный никуда не исчезает, но его роль смещается: меньше ручного перебора вариантов, больше выбора вопросов, проверки направлений, интерпретации и решения о том, что действительно важно.
Где нужна осторожность
Публикация исходит от самой OpenAI, и сообществу ещё предстоит подробно проверить корректность, новизну и значимость каждого результата.
Сертификаты Lean помогают с формальной проверкой, но научное доверие не сводится к технике. В него входят понимание контекста, вклада, связи с предыдущими работами и возможность других исследователей строить дальше на этом результате.
Поэтому точная формулировка звучит не как «AI решил математику», а так: OpenAI опубликовала формальные результаты для публичной проверки, и если они устоят, это поворотная точка в том, как AI встраивается в научное исследование.
Главный вопрос
Если AI начинает производить формальные доказательства открытых задач, как будет выглядеть исследовательский процесс через три-пять лет?
Скорее всего, это не мир, где компьютер заменяет учёного. Вероятнее мир, где учёный работает с системой, которая предлагает направления, выстраивает аргументы и формально проверяет большие куски работы, оставляя человеку суждение, ответственность и смысл.
Источники: OpenAI, репозиторий с Lean-сертификатами.