Команда Google DeepMind с использованием системы на базе больших языковых моделей (LLM) и формальной верификации Lean автоматически доказала девять открытых математических задач, сформулированных Палом Эрдёшем, а также 44 гипотезы из Энциклопедии целочисленных последовательностей (OEIS). Работа опубликована в препринте на arXiv.
Исследователи Google DeepMind разработали агентную систему AlphaProof Nexus, которая впервые в истории автоматически решила девять открытых задач из списка венгерского математика Пала Эрдёша (Paul Erdős). Некоторые из этих задач оставались нерешёнными более 50 лет. Кроме того, система доказала 44 из 492 открытых гипотез из Энциклопедии целочисленных последовательностей (OEIS), а также разрешила 15-летний вопрос в алгебраической геометрии и обнаружила новый алгоритмический параметр в теории оптимизации.
Ключевой особенностью подхода стала комбинация LLM (предположительно, Gemini 3.1 Pro) с формальной верификацией в среде Lean. Агент генерирует попытки доказательств, которые затем автоматически проверяются компилятором Lean на логическую корректность. Человеческое рецензирование требовалось только на финальном этапе — для подтверждения уже верифицированных результатов. По словам авторов работы, стоимость решения одной задачи составила несколько сотен долларов.
Как отмечается в препринте, даже базовая версия агента, использующая простой цикл «генерация — проверка», смогла воспроизвести все девять успехов в задачах Эрдёша. Более сложные механизмы, такие как эволюционный поиск и обучение с подкреплением, давали преимущество только на самых трудных задачах. Это подтверждает тенденцию: по мере улучшения базовых моделей простые агентные архитектуры начинают догонять специализированные системы.
Формальная верификация сыграла критическую роль в фильтрации ошибок. Анализ неудачных попыток показал, что ИИ часто «галлюцинировал» леммы, ссылаясь на несуществующие результаты, или маскировал сложность задачи, переформулируя её в виде вспомогательной леммы. В неформальных доказательствах такие ошибки могли бы остаться незамеченными, тогда как Lean выявлял их автоматически. Кроме того, агент обнаружил неточности в формулировках некоторых задач в математической литературе, скорректировав их перед решением.
Пока успехи системы ограничены областями, где библиотека Lean наиболее развита: комбинаторикой, теорией чисел и оптимизацией. Задачи, требующие разработки принципиально новых теорий, остаются за пределами возможностей AlphaProof Nexus. Из 353 открытых задач Эрдёша решено лишь девять, однако авторы подчёркивают, что работа демонстрирует потенциал автономных ИИ-систем в математике.
«Наш самый производительный агент самостоятельно решил 9 из 353 открытых задач Эрдёша при стоимости в несколько сотен долларов за каждую, доказал 44 из 492 гипотез OEIS и применяется в исследованиях по комбинаторике, оптимизации, теории графов, алгебраической геометрии и квантовой оптике», — говорится в препринте.