OpenAI: десять математических результатов, формализованных в Lean, — и роль внутренней модели

1 августа OpenAI опубликовала рукопись «Ten Advances in Mathematics and Theoretical Computer Science», приписав результаты собственной внутренней модели. Одновременно был создан репозиторий GitHub `openai/ten-proofs`, где выложены формализации всех десяти доказательств на Lean 4. Среди результатов выделяются улучшение показателя для упаковки сфер — первое с 1978 года —, построение несофической группы и контрпример к гипотезе жёсткости Конна. Репозиторий — это проект Lean 4.32.0 на базе mathlib под лицензией Apache-2.0: любой может перекомпилировать доказательства командами `lake exe cache get` и `lake build All`, а папка ComparatorChallenges объясняет, как провести проверку независимо.

Пресса связала эти результаты с «Astra» — названием следующего семейства моделей, о котором OpenAI объявила в тот же день, 1 августа; сама рукопись, однако, говорит лишь о «внутренней модели», которая не выпущена. Такие цифры, как около 2000 долларов затрат на токены или 249 страниц документа, взяты из сторонних публикаций, поскольку официальная страница анонса сейчас недоступна. В статье есть благодарности математикам-людям за вычитку и указание на независимую параллельную работу Шуосина Чжоу, выполненную отчасти с помощью GPT-5.6 Sol.

По данным SiliconANGLE, математические рассуждения исходят от модели, но превратили её вывод в публикуемые рукописи люди-исследователи: насколько весома эта доработка, не оценено. Использование Lean 4 смещает спор: сертификат гарантирует логическую корректность доказательства, но не подтверждает автоматически, что формализованное утверждение совпадает с исторической открытой проблемой, — эта проверка остаётся человеческой. Ни один из десяти результатов не прошёл формального рецензирования. Прецедент давит: в октябре 2025 года заявление о десяти «решённых» GPT-5 задачах Эрдёша оказалось безосновательным, и Томас Блум, куратор erdosproblems.com, назвал это серьёзным искажением. О сегодняшних десяти результатах тот же Блум говорит уже «big news». Как замечает физик-теоретик Тобиас Й. Осборн, названные 2000 долларов — это стоимость выигравших токенов, а не общий «урожай» попыток; по этому поводу OpenAI не сообщила ничего. Всё это происходит на фоне «Leiden Declaration on Artificial Intelligence and Mathematics», опубликованной в июне 2026 года и, по данным the-decoder, поддержанной более чем 3000 математиками и Международным математическим союзом; декларация требует прозрачности, защиты прав авторов и человеческой ответственности за результаты.

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