DeepMind AlphaProof Nexus: как AI-агент ищет формальные доказательства в Lean

По состоянию на 27 мая 2026 года DeepMind AlphaProof Nexus выглядит как один из самых показательных кейсов ИИ в математике за год. В препринте на arXiv исследователи Google DeepMind описали агентную систему, которая пишет формальные доказательства в Lean: 9 решённых задач Эрдеша из 353 попыток и 44 доказанные гипотезы OEIS из 492.

Главное здесь не в громком лозунге «ИИ решил математику». Его как раз лучше не повторять. AlphaProof Nexus интересен другим: модель не просто выдаёт красивый текст доказательства, а работает в цикле с компилятором Lean. Система предлагает ход, Lean жёстко проверяет формальный код, ошибка возвращается агенту, и тот чинит доказательство или разбивает задачу на подлеммы.

Это отличает новый кейс от истории, где ChatGPT помог человеку с задачей Эрдеша #1196. Там ИИ был частью человеческого поиска. Здесь акцент на другом: агент пытается довести доказательство до машинно проверяемого состояния. И это же отделяет работу от соседних новостей про модели рассуждения: речь не о публичной функции Gemini или ChatGPT, а о исследовательском контуре для формального proof search.

Что именно произошло

Препринт Advancing Mathematics Research with AI-Driven Formal Proof Search подан на arXiv 21 мая 2026 года. Авторы пишут, что AlphaProof Nexus стал для них рамкой для LLM-assisted proof generation: агенты получают Lean-файл с формулировкой теоремы, библиотечными импортами и пустым местом вместо доказательства. Дальше задача системы — заменить это пустое место доказательством без sorry, то есть без заглушек, которые в Lean закрывают цель, но не доказывают её по-настоящему.

В полной конфигурации агент решил 9 из 353 формализованных задач Эрдеша. Две из них, по словам авторов, оставались открытыми 56 лет. Кроме того, система доказала 44 из 492 открытых гипотез из OEIS — энциклопедии целочисленных последовательностей. В статье также перечислены исследовательские применения за пределами этого набора: алгебраическая геометрия, оптимизация, теория графов, аддитивная комбинаторика и квантовая оптика.

Эти числа нужно читать аккуратно. 9/353 — это сильный сигнал для формальных доказательств, но одновременно напоминание о масштабе нерешённой части. Большинство задач агент не решил. А стоимость «несколько сотен долларов на задачу» в статье относится к inference cost успешного прогона, а не ко всей цене исследования, подготовки формализаций, инфраструктуры и работы математиков.

Что такое AlphaProof Nexus

AlphaProof Nexus — не один монолитный «математический мозг». В статье описаны несколько вариантов агента. Базовая версия запускает независимых prover-subagents: каждый делает многоходовые LLM-вызовы, правит Lean-скетч и после каждого шага отдаёт файл на проверку компилятору. Если Lean возвращает ошибку, это становится входом для следующей попытки.

Полная версия добавляет два механизма. Первый — возможность вызывать AlphaProof как специализированный инструмент для отдельных целей внутри доказательства. Второй — эволюционный слой: удачные и частично полезные скетчи попадают в population database, получают оценки, затем используются как материал для новых попыток. В статье отдельно указано, что prover-часть базового агента использовала Gemini 3.1 Pro, а rater-subagents в эволюционном слое — Gemini 3.0 Flash.

Для читателя, который работает с агентными системами, самая важная деталь знакомая: компилятор здесь играет роль внешнего судьи. Как и в обычных AI-агентах с tool feedback, модель не должна сама решать, верен ли её ответ. Она получает проверяемую обратную связь от инструмента, меняет состояние задачи и пробует снова.

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

Почему Lean меняет уровень доверия

Обычные математические ответы LLM трудно использовать в исследовании без ручной проверки. Текст может звучать убедительно и при этом содержать скрытую логическую дыру, ссылку на несуществующую лемму или подмену условия. В математике такие ошибки особенно опасны: одна неверная промежуточная строка может испортить весь результат.

Lean решает не все проблемы, но закрывает одну критическую: проверку формального доказательства. В Lean определения, теоремы и доказательства записаны как код. Компилятор проходит доказательство по шагам и отслеживает оставшиеся цели. Доказательство считается завершённым, когда целей не осталось и в файле нет заглушек.

Именно поэтому история AlphaProof Nexus пересекается с темой формальной верификации и границ доверия к Lean. Машинно проверяемое доказательство сильнее обычного текста, но оно не снимает вопрос о спецификации. Если исходная формализация неточно передала человеческую гипотезу, Lean честно проверит не ту задачу. Авторы статьи это понимают: после каждого решённого Erdős-примера эксперты команды проверяли, что Lean-постановка соответствует исходной формулировке.

Где агент ошибался

Один из самых полезных разделов статьи — разбор неудач. Авторы пишут, что в проваленных задачах агент часто переносил главную трудность в отдельную лемму с sorry, которая почти повторяла исходную цель. Другой тип ошибки — ссылки на якобы известные леммы из литературы. При ручной проверке такие леммы оказывались галлюцинациями.

Это важнее, чем может показаться. AlphaProof Nexus не отменяет слабости LLM; он строит вокруг них проверочный контур. Пока в доказательстве остаётся sorry, задача не закрыта. Пока агент меняет формулировку под себя, валидатор должен остановить результат. Пока автоформализация может исказить исходную задачу, нужен человек, который сравнит формальный объект с математическим смыслом.

В OEIS-эксперименте этот риск тоже учли. Сначала Gemini помог автоформализовать 492 открытых вопроса, затем агент должен был доказать test lemmas: первые члены последовательности должны совпадать с формальным определением. Это не идеальная защита от неверной формализации, но хороший инженерный фильтр перед запуском дорогого поиска доказательства.

Что опубликовано в репозитории

Google DeepMind выложила отдельный репозиторий alphaproof-nexus-results. В нём лежат Lean proofs, сгенерированные AlphaProof Nexus, и часть человеческих текстовых доказательств, следующих структуре найденных Lean-доказательств.

Структура репозитория полезна сама по себе. Там есть папки для задач Эрдеша, OEIS и исследовательских коллабораций: additive combinatorics, algebraic geometry, graph theory, optimization theory и quantum optics. В README также сказано, что проверить доказательства можно через стандартную сборку Lean-проекта: lake exe cache get и lake build.

Есть и важная оговорка: репозиторий содержит только задачи, где AlphaProof Nexus нашёл успешные доказательства. Для полного набора попыток по OEIS и задачам Эрдеша авторы дают ссылки на отдельные формализации. То есть GitHub-репозиторий — витрина доказанных результатов, а не полный журнал всех провалов и промежуточных попыток.

Почему это не AGI и не замена математикам

AlphaProof Nexus хорошо показывает, куда движется ИИ для науки, но из него не следует, что математики стали лишними. Система работала с уже формализованными постановками или постановками, которые помогали формализовать люди и модели. Человеческие эксперты проверяли соответствие Lean-версий исходным задачам. В исследовательских применениях агент часто выступал как инструмент, который помогает уточнить доказательство, найти контрпример или закрыть технически тяжёлую часть.

Даже там, где система доказала новое утверждение, остаётся научная работа вокруг результата: понять, почему доказательство устроено именно так, насколько оно красиво, можно ли обобщить аргумент, как связать его с литературой и какие новые вопросы он открывает. Lean даёт жёсткую проверку логики внутри формальной рамки. Он не заменяет математическую интерпретацию.

Зато практический сдвиг заметен. Если раньше LLM чаще помогали на уровне черновика, подсказки или пересказа, то AlphaProof Nexus показывает другой режим: агент может выполнять много итераций формального поиска, получать строгий машинный сигнал и сохранять только те результаты, которые проходят проверку. Для исследовательских команд это не «автономный математик», а ускоритель скучной и дорогой части proof engineering.

Что смотреть дальше

В этой истории стоит следить не только за следующими числами «сколько задач решено». Более важны три вопроса.

Первый: насколько хорошо можно масштабировать автоформализацию. Пока между человеческой задачей и Lean-теоремой остаётся слабое место, формальная проверка не закрывает всю цепочку доверия. Второй: сможет ли агент лучше работать с большими библиотеками вроде mathlib и не выдумывать леммы, которые похожи на известные, но не существуют. Третий: появятся ли открытые журналы запусков и отрицательных результатов, чтобы сообщество видело не только успешные доказательства.

AlphaProof Nexus не доказывает, что ИИ «понял математику». Он показывает более приземлённую и потому более важную вещь: формальные доказательства становятся агентным процессом. Модель предлагает ход, компилятор проверяет, агент чинит ошибку, человек следит за смыслом постановки. В такой связке ценность даёт не магия одной модели, а дисциплина всего контура проверки.

Читайте также

• ChatGPT помог решить 60-летнюю задачу Эрдеша
• Формальная верификация кода: что показал баг в Lean 4
• Агентный ИИ: архитектуры AI-агентов, ReAct и tool use

Источники и проверка фактов

• arXiv: Advancing Mathematics Research with AI-Driven Formal Proof Search, подано 21 мая 2026 года, проверено 27 мая 2026 года.
• HTML-версия arXiv:2605.22763v1, использована для описания архитектуры, ограничений, чисел 9/353 и 44/492, а также изображений, проверено 27 мая 2026 года.
• Google DeepMind: alphaproof-nexus-results на GitHub, использован для проверки состава proof materials, лицензий и статуса «not an official Google product», проверено 27 мая 2026 года.
• README репозитория alphaproof-nexus-results, использован для проверки структуры директорий и команд сборки Lean-проекта, проверено 27 мая 2026 года.