Команда Google DeepMind под руководством Сварата Чаудхури (Swarat Chaudhuri) разработала фреймворк AlphaProof Nexus на базе модели Gemini, который впервые решил девять нерешенных математических задач, сформулированных Полом Эрдешем, включая две, остававшиеся открытыми 56 лет. Результаты опубликованы в препринте на arXiv.
Исследователи Google DeepMind продемонстрировали возможности нового агентного фреймворка AlphaProof Nexus, предназначенного для автоматического поиска формальных доказательств математических теорем. Система, использующая обратную связь от компилятора Lean, самостоятельно решила девять открытых задач из области комбинаторики, сформулированных Полом Эрдешем, а также 44 задачи из Энциклопедии целочисленных последовательностей (OEIS). Среди решенных проблем — задача по алгебраической геометрии, не поддававшаяся доказательству 15 лет, и задача по минимаксной оптимизации семилетней давности.
Как отметил руководитель проекта Сварат Чаудхури, работа над AlphaProof Nexus заняла около года. По его словам, ключевым открытием стало то, что «простые агентные циклы с обратной связью от компилятора могут конкурировать с более сложными системами» при использовании современных языковых моделей. «Мы были поражены как возможностями наших систем, так и масштабом предстоящих вызовов», — заявил Чаудхури в посте на X.
Результаты работы уже вызвали интерес у математиков из разных областей — от теории графов до квантовой оптики. По словам Пушмита Коли (Pushmeet Kohli), вице-президента Google DeepMind по исследованиям в области ИИ, агентные системы на базе Gemini способны значительно ускорить процесс формального доказательства теорем. «Эти результаты показывают огромный потенциал даже простых агентных циклов», — написал Коли, опубликовав ссылку на репозиторий с доказательствами, сгенерированными AlphaProof Nexus.
Дэн Рой (Dan Roy), профессор статистики и информатики Торонтского университета, назвал работу «первым крупномасштабным эмпирическим исследованием формального доказательства теорем с помощью агентов на базе языковых моделей». По его мнению, проект задает важный ориентир для дальнейших исследований в этой области.
Фреймворк AlphaProof Nexus работает с формальным языком доказательств Lean, что позволяет верифицировать результаты независимо. В препринте подчеркивается, что система не только решает задачи, но и генерирует доказательства, которые могут быть проверены математическим сообществом.
Источники: X-пост Пушмита Коли, 25 мая 2026; X-пост Сварата Чаудхури, 25 мая 2026; препринт на arXiv.