OpenAI Astra: десять результатов в математике и кто их проверил
OpenAI открыла рукописи и Lean-файлы для десяти математических результатов Astra. Разбираем заявления компании и границы независимой проверки.
1 августа 2026 года OpenAI заявила о десяти новых результатах внутренней модели Astra в математике и теоретической информатике. Компания открыла 249-страничную рукопись, 62 страницы заметок о поиске решений и Lean-файлы для машинной проверки всех десяти доказательств.
История OpenAI Astra в математике выглядит убедительнее обычного пресс-релиза: исходные материалы можно скачать и разбирать. Однако на дату анонса OpenAI не назвала независимых рецензентов этих работ. Публикация доказательств и их внешняя оценка — разные этапы.
Факты и статус проверки актуальны на 1 августа 2026 года.
Что OpenAI выпустила вместе с Astra
Astra пока нельзя вызвать в ChatGPT или через API. OpenAI называет её внутренней версией своей следующей крупной модели и не раскрывает архитектуру, размер, контекстное окно или дату публичного запуска. Поэтому результаты нельзя переносить на доступную линейку GPT-5.6.
По версии компании, модель сгенерировала математические аргументы. Затем люди вместе с той же моделью подготовили рукописи, после чего Astra формализовала доказательства в Lean. OpenAI берёт ответственность за корректность пакета и приписывает сами математические аргументы системе.
Поиск решений, как оценивает OpenAI, потребовал столько токенов, сколько стоили бы примерно $2000 по текущему тарифу Sol API. Это оценка компании, а не воспроизводимый бюджет эксперимента: число запусков, длительность работы и распределение входных и выходных токенов не опубликованы.
Десять результатов OpenAI Astra: таблица заявлений
В таблице ниже формулировки сверены с официальной рукописью OpenAI. Ссылка «Lean» ведёт к отдельному сертификату результата. Столбец о внешней проверке фиксирует только публично названную независимую рецензию на дату релиза.
| Область | Что заявляет OpenAI | Открытые материалы | Независимая рецензия |
|---|---|---|---|
| Упаковка сфер в больших размерностях | Точно определена асимптотическая сила линейной программы Кона — Элкиса; получена новая общая верхняя граница плотности упаковки. | рукопись, Lean | Не указана на странице релиза |
| Двоичные и сферические коды | Классические верхние границы для кодов с фиксированным расстоянием улучшены на экспоненциальный множитель для всех параметров. | рукопись, Lean | Не указана на странице релиза |
| Несофические группы | Построена явная несофическая группа; это закрывает вопрос, допускает ли каждая счётная группа конечные перестановочные приближения. | рукопись, Lean | Не указана на странице релиза |
| Гипотеза жёсткости Конна | Построены бесконечные семейства неизоморфных групп со свойством (T) и одной алгеброй фон Неймана; гипотеза опровергнута. | рукопись, Lean | Не указана на странице релиза |
| Сложность арифметических схем | Для перманента получены нижние границы Ω(n2 log log n) для схем без деления и Ω(n4/log n) для формул. | рукопись, Lean | Не указана на странице релиза |
| Квантовое параллельное повторение | Доказана экспоненциальная теорема о повторении для любой конечной квантовой игры двух игроков. | рукопись, Lean | Не указана на странице релиза |
| Задача ближайшего вектора | Прямое сведение из 3SAT даёт n1/400-факторную трудность аппроксимации евклидовой задачи ближайшего вектора. | рукопись, Lean | Не указана на странице релиза |
| Гипотеза Эрхарта об объёме | Во всех размерностях доказана точная граница (n + 1)n/n! для выпуклого тела с единственной внутренней целой точкой в барицентре. | рукопись, Lean | Не указана на странице релиза |
| Многоцветные числа Рамсея | Получена сверхэкспоненциальная нижняя граница Rk(3) = kΘ(k), закрывающая задачу Эрдёша 183. | рукопись, Lean | Не указана на странице релиза |
| Экстремальная теория графов | Две конструкции двудольных графов опровергают гипотезы о компактности и вырожденности, закрывая задачи Эрдёша 146 и 180. | рукопись, Lean | Не указана на странице релиза |
Отсутствие внешней рецензии в таблице не означает, что доказательства ошибочны. Это текущий статус: OpenAI опубликовала проверяемый пакет, а независимая оценка математического сообщества только начинается.
Что на самом деле проверяет Lean-сертификат
Lean принимает формальную запись теоремы и доказательство в виде проверяемого терма. Небольшое ядро системы подтверждает, что вывод следует из определений, аксиом и импортированных теорем. Ошибка языковой модели в промежуточном рассуждении не пройдёт эту проверку, если она попала в итоговый формальный терм.
Граница проверки проходит раньше, чем кажется. Документация Lean прямо оговаривает: формальная теорема должна верно передавать смысл исходного неформального утверждения, а импортированные библиотеки и аксиомы должны быть корректными. Lean не определяет научную новизну результата, полноту обзора литературы или его значение для области.
OpenAI выложила отдельный Lean-файл для каждого результата и задачи Comparator для повторной проверки. Репозиторий можно собрать независимо. Такой подход близок к тому, как работают формальные доказательства в Lean у других исследовательских систем. Публичного отчёта независимой команды о пересборке всего пакета Astra на момент публикации ещё нет.
Где заканчивается проверка OpenAI
У нынешнего релиза есть заметное отличие от предыдущего математического результата OpenAI. В мае компания приложила к опровержению гипотезы о единичных расстояниях замечания внешних математиков и назвала Ногу Алона, Тима Гауэрса, Арула Шанкара и Якоба Цимермана. В публикации Astra внешние рецензенты не перечислены.
Независимым специалистам предстоит проверить три слоя. Сначала нужно сопоставить формальные утверждения с исходными открытыми задачами и исключить ослабление условий. Затем потребуется проверить приоритет и полноту ссылок на предыдущие работы. После этого сообщество сможет оценить глубину и значение новых методов, а не только логическую корректность.
Этот порядок совпадает с рекомендациями Лейденской декларации об ИИ и математике, которую OpenAI сама упоминает в релизе. Декларация требует раскрывать применение автоматических инструментов, поддерживать независимую проверку и публиковать результаты в рецензируемых изданиях. Рукопись и Lean-код закрывают часть требований к прозрачности, но не заменяют внешнюю экспертизу.
Что Astra меняет в работе исследователя
Впервые OpenAI показывает один и тот же процесс сразу на десяти задачах: система ищет аргумент, люди помогают превратить его в читаемую рукопись, а модель формализует результат. Это уже похоже на производственный контур математического исследования, хотя ключевые решения по выбору задач, проверке постановок и публикации остаются за людьми.
Открытые материалы здесь важнее названия будущей модели. Без рукописей и формальных сертификатов десять результатов остались бы набором заявлений в блоге компании. С ними специалисты получают возможность искать ошибки, сравнивать доказательства с предыдущими работами и оценивать новые идеи независимо от OpenAI.
По состоянию на 1 августа корректная формулировка звучит так: OpenAI опубликовала десять существенных математических результатов, которые приписывает внутренней Astra, и снабдила их открытыми Lean-сертификатами. Итоговый научный статус определят независимая проверка, обсуждение приоритета и рецензирование. Подробнее о распределении работы между моделью и человеком мы писали в материале о том, как ИИ меняет роль математика.
Источники
- официальный релиз OpenAI от 1 августа 2026 года;
- рукопись Ten Advances in Mathematics and Theoretical Computer Science;
- заметки OpenAI о поиске десяти решений;
- репозиторий ten-proofs с Lean-сертификатами;
- документация Lean о границах машинной проверки;
- Лейденская декларация об ИИ и математике;
- майский релиз OpenAI с внешними отзывами математиков.
