OpenAI заявила о прорыве Astra в математике. Что это значит для квантовой сложности

1 августа внутренняя версия следующего семейства ИИ-моделей Astra от OpenAI получила 10 результатов в математике и теоретической информатике. The Quantum Insider разобрал, какие из них могут быть важны для квантовой сложности и постквантовой криптографии.

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

«Мы считаем, что атрибуция должна честно отражать то, как был получен результат: приписывать человеку авторство доказательства, полностью сгенерированного ИИ-системой, означало бы искажать вклад системы и природу подлинной человеческой интеллектуальной работы», — заявили в OpenAI.

The Quantum Insider отдельно выделил результаты, связанные с квантовой сложностью и решеточной криптографией.

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

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

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

Контекст Лейденской декларации

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

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

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

Напомним, в мае модель OpenAI опровергла 80-летнюю гипотезу Эрдеша о единичных расстояниях. Тогда компания заявила, что доказательство проверили внешние математики.

Через несколько месяцев исследователь Anthropic Левент Альпоге с помощью Claude Fable 5 нашел контрпример к гипотезе Якобиана.

Обновление от 5.08.2026: в заголовок и текст новости внесены изменения, уточняющие результаты OpenAI.