ИИ 17 октября 2026, 23:35 МСК

Агент Google DeepMind AlphaProof Nexus решил 9 открытых задач Эрдёша

Исследовательский агент AlphaProof Nexus от Google DeepMind решил 9 из 353 открытых задач, связанных с Палом Эрдёшем, две из которых оставались нерешёнными 56 лет.

Кроме того, система доказала 44 из 492 открытых гипотез из Онлайн-энциклопедии целочисленных последовательностей (OEIS). На каждую решённую задачу Эрдёша уходило несколько сотен долларов на вычисления.

Ключевая особенность — использование Lean: ИИ предлагает формальное доказательство, а Lean проверяет каждый логический шаг и возвращает агенту обратную связь при ошибке. В системе несколько агентов работают параллельно, а в самой сложной версии их координирует эволюционный алгоритм; на отдельных этапах применяется AlphaProof. Более простой агент, чередующий генерацию доказательств и проверку в Lean, при повторном анализе тоже справился со всеми девятью задачами, но на самых трудных обходился дороже.

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

Ограничения остаются: большинство задач Эрдёша агент не решил, успехи сосредоточены в областях с развитой библиотекой формализованных результатов, а результаты сильно меняются от попытки к попытке. Задачи, требующие создания обширной новой теории, пока недоступны. Авторы считают, что формальные доказательства позволят включить ИИ в настоящую математическую работу.

• 9 из 353 открытых задач Эрдёша
• 44 из 492 гипотез OEIS
• Две задачи были нерешёнными 56 лет