AlphaProof Nexus решил задачи Эрдеша, простоявшие 56 лет без ответа

Математика - одна из тех областей, где "почти доказал" не считается. Либо доказательство верно на каждом шаге, либо его нет. Именно поэтому то, что Google DeepMind опубликовал в журнале Science 8 октября, вызвало такой резонанс: система AlphaProof Nexus не просто решила открытые математические задачи, но и прошла полноценное рецензирование - со всеми вытекающими последствиями для репутации результата.

Что именно сделал AlphaProof Nexus

Система атаковала 353 открытые задачи из коллекции Пола Эрдеша - венгерского математика, который за свою жизнь сформулировал, пожалуй, больше нерешенных вопросов, чем кто-либо другой в истории дисциплины. Из этих 353 задач AlphaProof Nexus решил девять, включая две, которые Эрдеш и его коллаборатор Андраш Шаркези поставили еще в 1970 году. 56 лет без ответа.

Параллельно система прошлась по 492 открытым гипотезам из онлайн-энциклопедии целочисленных последовательностей (OEIS) и нашла формальные доказательства для 44 из них. Кроме этого - одна задача в алгебраической геометрии и улучшенная оценка в min-max оптимизации, методе, который используется в обучении самих ИИ-моделей.

Как это работает

Архитектура системы строится вокруг Gemini 3.1 Pro, который генерирует и переписывает доказательства на формальном языке Lean. Lean - это не просто формальная нотация, а полноценный верификатор: после каждого редактирования он проверяет шаг и возвращает сообщение об ошибке, если что-то не так. Эти ошибки становятся сигналом для следующей попытки.

Для сложных подзадач система может задействовать AlphaProof - специализированный инструмент доказательства теорем. Но, что любопытно, девять задач Эрдеша были решены даже без него - только Gemini плюс Lean.

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

В числе авторов работы - испанский инженер Франсиско Руис, участвовавший в разработке системы в Google DeepMind.

Рецензирование как аргумент в споре

Публикация появилась на фоне острой дискуссии в математическом сообществе. OpenAI на прошлой неделе выложил на GitHub сотни математических доказательств, сгенерированных ИИ, - без рецензирования, без публикации в журнале. Ассоциация математиков-людей под руководством Теренса Тао, лауреата Филдсовской медали, призвала к бойкоту этого подхода.

DeepMind выбрал другой путь: Science - один из двух самых престижных научных журналов в мире, и попасть туда без рецензирования невозможно. При этом результаты были предварительно опубликованы на Arxiv еще в мае - то есть математическое сообщество имело несколько месяцев, чтобы их изучить до финальной публикации.

Это не просто процедурная разница. Публикация в рецензируемом журнале означает, что независимые эксперты изучили работу и сочли ее достаточно состоятельной для печати - в отличие от самостоятельной выгрузки файлов на GitHub.

Что это значит для математики и ИИ

Пока что AlphaProof Nexus решил 9 из 353 задач Эрдеша - это 2,5%. Звучит скромно, но дело не в проценте. Дело в том, что система вообще смогла решить хоть одну задачу из этого списка самостоятельно. Раньше единственным путем к решению задач Эрдеша был человек с годами погружения в тему.

При этом система работает не как калькулятор - она не вычисляет, она исследует. Предлагает стратегию, наталкивается на противоречие, меняет подход. Авторы отдельно подчеркивают, что более простая версия системы - просто генерация и проверка доказательств по очереди, без сложной многоагентной координации - тоже справилась с теми же девятью задачами Эрдеша. Это говорит о том, что ключевым оказался не сложный оркестр агентов, а сама связка "генерация + жесткая верификация".

Для разработчиков ИИ результат в min-max оптимизации особенно интересен: система улучшила теоретическую границу метода, который используется при обучении генеративных моделей. То есть ИИ потенциально помогает улучшить обучение будущих ИИ.

Для тех, кто следит из России

Доступ к статье в Science требует подписки или институционального доступа. Препринт на Arxiv открыт. Демонстрационного продукта для конечных пользователей нет - AlphaProof Nexus остается исследовательской системой, а не публичным сервисом.

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