Google DeepMind смогла решить ещё девять открытых задач Эрдёша и десятки математических гипотез
Google DeepMind представила систему AlphaProof Nexus — новый математический фреймворк, который смог самостоятельно решить девять открытых задач из знаменитого списка Пола Эрдёша (Paul Erdos). Некоторые из них оставались нерешёнными более полувека.
Система также доказала 44 открытые гипотезы из Online Encyclopedia of Integer Sequences (крупнейшая онлайн-база данных целочисленных последовательностей, созданная математиком Нилом Слоуном в 1964 году), решила 15-летнюю проблему, связанную с функциями Гильберта в алгебраической геометрии, и улучшила известную оценку в задачах выпуклой оптимизации.
Главная особенность AlphaProof Nexus — сочетание языковой модели Gemini 3.1 Pro с системой формальной математической проверки Lean. Вместо того чтобы полностью строить доказательство на естественном языке, как это делают обычные LLM, модель генерирует отдельные шаги доказательства в формальном языке Lean, после чего компилятор автоматически проверяет их корректность.
Если система допускает ошибку, то Lean возвращает точное сообщение о проблеме, которое сразу используется для следующей попытки. Такой подход создаёт своеобразный «страховочный контур»: модель не может бесконтрольно галлюцинировать логические переходы, поскольку каждый шаг проходит строгую верификацию.
Иллюстрация: Nano BananaПо словам исследователей, стоимость вычислений для решения одной задачи составляла всего несколько сотен долларов.
Наиболее успешной система оказалась в областях, где уже хорошо развита библиотека формализованной математики Mathlib: в комбинаторике, теории чисел и выпуклой оптимизации. Однако большинство задач Эрдёша всё ещё остаются недоступными для ИИ. Из 353 открытых задач система смогла решить лишь девять.
Авторы подчёркивают, что AlphaProof Nexus не заменяет математиков, а становится новым исследовательским инструментом. Учёные, работавшие с системой, отмечают, что даже неудачные попытки доказательства помогали лучше понять структуру задачи и выявлять слабые места в существующих теориях.
Кроме того, система уже используется в исследованиях по квантовой оптике и теории графов. Все формальные доказательства на Lean опубликованы на GitHub.
Как AlphaProof Nexus решает задачу Эрдёша №125: агент получает файл Lean, в котором настоящее доказательство заменено на «пробел» (a), затем анализирует предыдущие попытки с оценками Elo и текущий план решения, встроенный в запрос (b). После этого система пошагово разбивает доказательство на подзадачи, вызывает AlphaProof для решения отдельных подцелей и итеративно уточняет неудачные шаги, декомпозируя их до уровня лемм, пока все цели доказательства не будут формально подтверждены. Источник: Tsoukalas et al.Разработка DeepMind выходит на фоне растущей конкуренции между крупнейшими ИИ-лабораториями в области математики. Ранее OpenAI при помощи своей reasoning-модели смогла опровергнуть гипотезу Эрдёша о единичных расстояниях, а математик Терренс Тао (Terence Tao) называл подобные результаты одним из первых действительно убедительных примеров решения открытых математических задач с помощью LLM.
При этом подход OpenAI считается более «чистым» с точки зрения возможностей самих языковых моделей: там ИИ строил логическую цепочку без внешней формальной проверки через Lean. DeepMind, напротив, делает ставку не на демонстрацию «сырого интеллекта» модели, а на создание надёжного и масштабируемого инструмента для повседневной математической работы.
Сам Терренс Тао ранее предупреждал, что не стоит переоценивать подобные достижения: реальный процент успешного решения открытых задач ИИ по-прежнему остаётся крайне низким и концентрируется вокруг сравнительно простых случаев.
© iXBT
