AlphaProof Nexus решил открытые задачи и прошёл рецензию

Google DeepMind сообщила о решении десятков открытых математических задач с помощью новой системы AlphaProof Nexus. Результаты исследования опубликованы в журнале Science, что делает работу одной из немногих в области ИИ-математики, прошедших полноценное рецензирование. Система решила девять из 353 открытых задач Эрдёша, причём две из них оставались нерешёнными 56 лет.

Помимо задач Эрдёша, AlphaProof Nexus доказала 44 гипотезы из базы целочисленных последовательностей OEIS, решила открытый вопрос в алгебраической геометрии и улучшила известную оценку в минимаксной оптимизации — методе, применяемом при обучении некоторых ИИ-моделей. Решения девяти задач Эрдёша команда выложила в открытый доступ ещё до публикации статьи.

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

Публикация выходит на фоне споров о роли ИИ в математике. Ранее OpenAI выложила сотни ИИ-доказательств на GitHub, не отправляя их в научные журналы. Ассоциация за математику с участием человека (Association for Human Mathematics) под руководством Теренса Тао призвала к бойкоту таких действий.

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

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