Google DeepMind представила систему AlphaProof Nexus, которая сочетает генерацию доказательств с помощью большой языковой модели и машинную проверку в Lean. По данным статьи, система самостоятельно решила 9 из 353 открытых задач Эрдёша, которые она пыталась доказать, включая две задачи, остававшиеся без ответа 56 лет.
Кроме того, AlphaProof Nexus доказала 44 из 492 открытых гипотез из Online Encyclopedia of Integer Sequences, закрыла 15-летний вопрос о функциях Гильберта в алгебраической геометрии и улучшила известную оценку в выпуклой оптимизации. Стоимость вывода, как сказано в работе, составляла несколько сотен долларов на одну задачу.
В основе системы используется Gemini 3.1 Pro, но модель не строит всю логическую цепочку в обычном естественном языке. Она генерирует шаги доказательства в формальном языке Lean, а компилятор проверяет каждый шаг. Сообщения об ошибках сразу подаются в следующую попытку, что помогает модели опираться на символьную проверку и снижает риск логических сбоев. Люди подключаются только на финальном этапе проверки результата.
Авторы описывают четыре варианта агентов с разным уровнем сложности.
- Agent (A): независимые подагенты на Gemini 3.1 Pro по циклу создают шаги доказательства, получают проверку в Lean и используют ошибки для новой попытки.
- Agent (B): добавляет запросы к AlphaProof — системе Google на базе обучения с подкреплением для олимпиадной математики, которая может достраивать пропущенные части доказательства.
- Agent (C): включает эволюционный механизм. Подагенты делят общую популяцию черновиков доказательств, а оценочные агенты на Gemini 3.0 Flash проверяют их на правдоподобие и новизну, после чего ранжируют по системе Elo.
- Agent (D): объединяет все эти возможности.
Для задач Эрдёша применялся Agent (D). Однако последующий анализ показал, что самый простой Agent (A), который использует только LLM и обратную связь от компилятора, тоже смог доказать все девять решённых задач Эрдёша, хотя на самых трудных примерах он обходился дороже.
Исследователи объясняют результат простого агента двумя причинами: быстрым ростом качества базовых языковых моделей и «силой обратной связи от компилятора в заземлении рассуждений LLM». При этом полностью оснащённый агент пока лучше справляется с самыми трудными задачами. Авторы пишут, что это указывает на сдвиг от узкоспециализированных обученных систем к простым агентным циклам по мере роста возможностей LLM.
Лучшие результаты система показала в комбинаторике, выпуклой оптимизации и теории чисел — там, где библиотека Mathlib для Lean достаточно развита, а задачи можно разбить на управляемые подцели. При этом большинство задач Эрдёша остались нерешёнными. Авторы отдельно отмечают, что это тем более касается задач, для которых нужна большая новая теория. Агенты также сохраняют ограничения самих языковых моделей.
По словам авторов, польза системы не сводится к уже решённым задачам. Математики, работавшие с ней, сообщили, что даже неудачные попытки доказательства помогали лучше понять задачу. В статье это сформулировано так: «AI-driven formal proof search can serve not only to solve problems but to deepen human understanding.»
Так как черновики доказательств были формализованы, эксперты могли сосредоточиться на нерешённых подзадачах, а не перепроверять весь ход рассуждений с нуля. Авторы также пишут: «Formal verification can serve as a filter for determining which proofs merit human review.» По их словам, агенты хорошо выявляли ошибки в формализациях, уже присутствующих в литературе.
Согласно статье, систему уже используют в текущих исследованиях по квантовой оптике и теории графов. Все доказательства в Lean и часть доказательств на естественном языке опубликованы на GitHub.
На этом фоне авторы приводят и другие недавние результаты. OpenAI недавно использовала закрытую reasoning-модель, чтобы опровергнуть гипотезу Эрдёша о единичных расстояниях. Лауреат медали Филдса Тим Гауэрс назвал это «вехой в математике ИИ». До этого GPT-5.2 Pro помогла решить задачу Эрдёша №281, а Теренс Тао назвал этот случай «perhaps the most unambiguous instance» того, как LLM решила открытую математическую задачу. Затем GPT-5.4 решила ещё одну задачу Эрдёша.
В материале отмечается, что такие результаты в каком-то смысле выглядят даже более впечатляюще, поскольку языковая модель должна удерживать всю логическую цепочку в естественном языке без проверки каждого шага через Lean. Подход DeepMind более системный и масштабируемый, но он нацелен на другую задачу: создание стабильного инструмента ИИ для повседневной математической работы.
Теренс Тао ранее призывал не делать слишком далеко идущих выводов из заголовков. Фактическая доля успешных решений задач Эрдёша у ИИ пока находится на уровне около 1–2% и в основном касается более простых примеров. У системы Google показатель составил 9 из 353 задач, что почти совпадает с ориентиром Тао в 2%.
Источник: The Decoder, исследовательская статья Google DeepMind.
