OpenAI показала Astra с 10 математическими достижениями и проверкой в Lean

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

Список задач выглядит так, будто его собирали на кафедре, а не для красивой презентации. Тут и первая явная конструкция несофической группы, и опровержение гипотезы жёсткости Конна, и доказательство квантовой теоремы о параллельном повторении, и гипотеза Эрхарта об объёме, и улучшение верхней оценки плотности упаковки сфер, которое не удавалось получить с 1978 года.

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

По подсчётам компании, на поиск всех десяти решений ушло около $2000 вычислительных затрат по тарифам Sol API. На фоне ручной работы исследователей и аспирантов сумма выглядит почти скромно. Но для OpenAI важнее другое: Astra показала не один удачный ответ, а серию формализуемых доказательств в разных областях — от теории групп до криптографии на решётках и экстремальной комбинаторики.

Как Astra проверяли

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

В этой нише гонка уже идёт. Google DeepMind год назад показала, что большие модели можно подталкивать к сложным олимпиадным и логическим задачам, а команды вокруг OpenAI, Anthropic и стартапов вроде Harmonic и Imandra давно гоняют автоматическое доказательство теорем как один из самых тяжёлых сценариев для ИИ. Проблема у большинства систем всё та же: догадку они подкинуть могут, а вот довести её до строгой проверяемой формы — уже нет.

Здесь OpenAI, похоже, пытается показать не только масштаб, но и качество самих доказательств. В публичных материалах компания выложила сертификаты и описание того, как модель рассуждала, чтобы результаты можно было разбирать не по пересказу, а по цепочке формальных шагов. Для матсообщества это заметно интереснее очередного рекорда на закрытом тесте: в таких задачах ценится не эффектный ответ, а возможность его воспроизвести и проверить без веры на слово.

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