AlphaProof Nexus с проверкой в Lean решил 9 открытых задач Эрдёша

В новой работе Google DeepMind описан AlphaProof Nexus — связка LLM-агентов с формальной проверкой доказательств в Lean. Система автоматически закрыла 9 из 353 формализованных открытых задач Эрдёша и 44 из 492 гипотез OEIS; важнее всего здесь не стоимость, а переход от правдоподобных текстовых рассуждений к машинно проверяемым артефактам.

Авторы из Google DeepMind опубликовали на arXiv работу «Advancing Mathematics Research with AI-Driven Formal Proof Search», где описывают AlphaProof Nexus — среду для поиска формальных доказательств с участием LLM. В отличие от подхода, при котором модель выдаёт доказательство на естественном языке, агент генерирует шаги в Lean, получает ошибки от компилятора и повторяет попытки до получения корректного формального доказательства.

В эксперименте самый сильный агент AlphaProof Nexus решил 9 из 353 открытых задач Эрдёша, формализованных для проверки, и доказал 44 из 492 открытых утверждений из OEIS. В статье также указана стоимость вывода порядка нескольких сотен долларов на решённую задачу, однако общий результат по задачам Эрдёша остаётся примерно 2,5%, что ограничивает интерпретацию результата как универсального «автоматического математика».

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

Авторы выложили результаты в репозиторий google-deepmind/alphaproof-nexus-results: там находятся Lean-доказательства, естественно-языковые версии части доказательств и инструкции по сборке проекта через lake build. Для разработчиков инструментов формальной верификации это показательный пример того, как LLM-агенты могут быть встроены не как «оракул», а как поисковый слой поверх проверяемой системы доказательств.