Google DeepMind решила девять задач Эрдёша и десятки гипотез

Компания Google DeepMind представила AlphaProof Nexus — передовой математический фреймворк, который успешно справился с девятью открытыми задачами из легендарного списка Пола Эрдёша. Некоторые из этих математических проблем оставались нерешёнными на протяжении более полувека.

Помимо достижений в задачах Эрдёша, система доказала 44 гипотезы из базы Online Encyclopedia of Integer Sequences (основана Нилом Слоуном в 1964 году), успешно разрешила 15-летнюю проблему функций Гильберта в алгебраической геометрии и повысила точность оценок в задачах выпуклой оптимизации.

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

Главная особенность архитектуры — интеграция языковой модели Gemini 3.1 Pro с системой формальной верификации Lean. В отличие от стандартных LLM, которые строят доказательства исключительно на естественном языке, AlphaProof Nexus генерирует пошаговые выкладки на формальном языке Lean. Это позволяет компилятору автоматически проверять корректность каждого шага.

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

Иллюстрация: Nano Banana

По данным исследователей, стоимость вычислительных мощностей для решения одной такой математической задачи составляла всего несколько сотен долларов.

Перспективы и ограничения

Наибольшую эффективность система демонстрирует в областях с развитыми библиотеками формализованной математики (Mathlib), таких как теория чисел, комбинаторика и выпуклая оптимизация. Тем не менее, общая сложность задач Эрдёша остается серьезным вызовом: из 353 открытых проблем системе удалось покорить лишь девять.

Разработчики подчеркивают, что AlphaProof Nexus не претендует на роль замены ученого, а выступает в качестве высокотехнологичного инструмента. Опыт работы с ИИ показал, что даже неудачные попытки доказательства помогают математикам глубже понять структуру задачи и обнаружить слабые стороны в существующих теориях.

В настоящее время наработки системы уже применяются в исследованиях по теории графов и квантовой оптике. Полный перечень формальных доказательств на языке Lean доступен на платформе GitHub.

Алгоритм решения задачи Эрдёша №125: агент работает с файлом Lean, где основное доказательство скрыто («пробел»). Система анализирует историю попыток (с рейтингом Elo) и план решения, декомпозируя задачи на подцели до уровня лемм, которые верифицируются итеративно. Источник: Tsoukalas et al.

Конкуренция в области ИИ-математики

Проект DeepMind развивается на фоне жесткой конкуренции между ведущими ИИ-лабораториями. Ранее компания OpenAI с помощью своих рассуждающих моделей (reasoning-models) смогла опровергнуть гипотезу Эрдёша о единичных расстояниях. Математик Терренс Тао оценил такие успехи как одни из первых убедительных примеров использования LLM для решения фундаментальных математических проблем.

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

При этом эксперты, включая Терренса Тао, призывают не переоценивать текущие результаты: доля решенных ИИ открытых задач остается крайне низкой и ограничивается относительно простыми случаями.