AlphaProof Nexus решил задачи Эрдеша за несколько сотен долларов

Полвека ожидания - и несколько сотен долларов

Представьте: математическая задача висит нерешенной с 1970 года. Поколения специалистов бились над ней, публиковали частичные результаты, выдвигали гипотезы. И вот приходит ИИ-агент - и закрывает вопрос за несколько сотен долларов вычислительного времени. Именно это сделал AlphaProof Nexus от Google DeepMind, и это не метафора прогресса - это буквальный факт, подтвержденный препринтом на arXiv от 21 мая 2026 года.

Система автономно решила 9 из 353 открытых задач Эрдеша, включая две, которые оставались без ответа 56 лет. Параллельно она доказала 44 из 492 открытых гипотез из Онлайн-энциклопедии целочисленных последовательностей (OEIS), закрыла 15-летний вопрос в алгебраической геометрии и улучшила известную оценку в выпуклой оптимизации. Все это - при стоимости инференса в несколько сотен долларов за задачу.

Почему задачи Эрдеша - это не олимпиада

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

Поэтому 2,5% решенных задач Эрдеша - это не скромный результат. Это качественный скачок от решения олимпийских задач (AlphaProof в 2024 году взял серебряный уровень на IMO) к настоящей исследовательской математике. Примерно то же самое, что перейти от игры в шахматы по правилам к разработке новой теории игр.

Архитектура: четыре агента и один сюрприз

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

Система реализована в виде четырех агентных вариантов:

- Агент A - базовый: LLM генерирует, Lean проверяет, цикл повторяется - Агент B - добавляет запросы к AlphaProof (система на основе обучения с подкреплением для олимпийской математики) - Агент C - вводит эволюционный компонент: суб-агенты делятся популяцией набросков доказательств, оцениваемых по системе Эло - Агент D - полная конфигурация со всеми возможностями

Но главный сюрприз обнаружился постфактум: простейший Агент A также смог доказать все девять задач Эрдеша - просто дороже на наиболее сложных из них. Исследователи объясняют это двумя факторами: быстрым улучшением базовых языковых моделей и "силой компиляторной обратной связи для заземления рассуждений LLM". Иными словами, жесткий верификатор компенсирует слабости языковой модели в формальной логике.

Сравнение с OpenAI: разные философии верификации

За несколько дней до публикации DeepMind OpenAI также заявила о решении задачи Эрдеша - но с принципиально иным подходом, опирающимся на рассуждения на естественном языке. Это и есть ключевое различие двух стратегий.

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

Что это значит за пределами математики

Здесь скрывается более широкий урок для индустрии. Исследователи DeepMind прямо указывают на "продолжающийся сдвиг от специализированных обученных систем к простым агентным циклам по мере роста возможностей LLM". Грубо говоря: завтра Агент A будет справляться с тем, на что сегодня нужен Агент D - просто потому что базовые модели становятся мощнее.

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

Стоимость в несколько сотен долларов за задачу выглядит иначе, когда сравниваешь ее с годами работы математика-исследователя. Экономика начинает меняться радикально.

Для российской аудитории

AlphaProof Nexus - исследовательская система, не публичный продукт. Доступа через API или веб-интерфейс нет. Препринт и репозиторий с доказательствами доступны на arXiv и GitHub без ограничений - их можно читать без VPN. Если DeepMind в будущем откроет исследовательский доступ, история с геоблокировкой типична для Google: российские аккаунты могут столкнуться с ограничениями, но академический контент традиционно остается открытым.

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

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