Система DeepMind автономно решила еще 9 задач Эрдеша

Стоимость решения каждой задачи составила всего несколько сотен долларов. Но есть нюанс: на самом деле DeepMind прогоняли через агента все 353 формализованные открытые задачи Эрдеша и сожгли гораздо больше ресурсов. Решение останавливали, если агент выходил за рамки 3000 итераций, и в итоге полностью решенных задач оказалось 9.

Статья с заявлением: arxiv.org/pdf/2605.22763v1. Здесь подробно описана архитектура самого агента AlphaProof Nexus, решившего задачи.

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

Помимо 9 задач Эрдеша (включая, кстати, две, которые были открыты на протяжении 50+ лет), Nexus также доказал 44 открытые гипотезы OEIS.

Кажется, DeepMind первые среди ИИ-лидеров провели настолько масштабный эвал агента на нерешенных задачах. Но точно далеко не последние. Решение открытых проблем уже становится похоже на бенчмарк.

Вот здесь выложили сами доказательства: github.com/google-deepmind/alphaproof-nexus-results