После прорыва OpenAI — новый удар по задачам Эрдёша: AI-агент Google решил ещё 9 открытых проблем

Google DeepMind, Google и академические партнёры выложили на arXiv работу об AlphaProof Nexus — системе, которая ищет математические доказательства с помощью агентов на базе больших языковых моделей и проверяет результат в Lean. Самый сильный вариант агента автономно решил 9 из 353 формализованных открытых задач из каталога ErdosProblems, а также доказал 44 из 492 открытых гипотез из OEIS, энциклопедии целочисленных последовательностей.

Новость легко спутать с недавним прорывом OpenAI по задаче единичных расстояний, но это разные истории. У OpenAI речь шла об одном громком результате в дискретной геометрии. У Google — о проверяемом поиске доказательств для набора уже формализованных исследовательских задач.

Как работает AlphaProof Nexus

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

На задачах Эрдёша авторы запустили систему не на ручной подборке красивых примеров, а на всех Lean-формализациях, доступных в репозитории Formal Conjectures на момент эксперимента: 353 постановки из более чем 1200 задач каталога. После каждого успеха эксперты проверяли соответствие исходной задаче. Доказательства опубликованы в репозитории google-deepmind/alphaproof-nexus-results, а результаты занесены на вики Теренса Тао.

Почему это важно

Формальная проверка не превращает LLM в безошибочного математика. В статье прямо описаны провалы: агент мог прятать трудность в вспомогательную лемму с заглушкой или ссылаться на несуществующее «известное» утверждение. Но такие ошибки не проходят финальный барьер. Успех засчитывается только тогда, когда Lean принимает доказательство без sorry, то есть без незакрытых мест.

Ограничения тоже существенные. Выборка смещена к задачам, которые сообщество уже успело записать в Lean. В OEIS авторы дополнительно проверяли первые члены последовательностей через тестовые леммы, чтобы снизить риск неверной формализации. Даже в списке Эрдёша агент закрыл 9 задач из 353, а не «решил математику».

Зато масштаб уже другой, чем у единичной демонстрации. Авторы пишут о стоимости вывода в несколько сотен долларов на задачу, а базовый агент, который чередует генерацию LLM и проверку Lean, позже смог повторить все 9 успехов, хотя на сложных задачах обходился дороже. AlphaProof Nexus уже применяется или тестируется в нескольких областях математики и физики.

Что меняется для науки

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

После результата OpenAI это выглядит как ускорение одной линии: крупные лаборатории начинают показывать не просто рассуждающие модели, а рабочие связки «агент плюс формальная проверка». Если такой подход станет дешевле и удобнее, следующий прорыв может прийти не из одной эффектной задачи, а из регулярного потока маленьких доказательств.