AlphaProof Nexus решил 9 задач Эрдёша за пару сотен долларов

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

Помимо этого система закрыла 44 открытые гипотезы в базе целочисленных последовательностей OEIS, разобрала 15-летний вопрос из алгебраической геометрии и нашла новый алгоритмический параметр в теории оптимизации, до которого исследователи раньше не добирались.

Архитектура устроена просто на словах и сложно на деле. Языковая модель уровня Gemini 3.1 Pro генерирует попытки доказательства, а компилятор Lean формально проверяет каждый логический шаг. Никакого человеческого ревью для подтверждения корректности не требуется, всё валидируется автоматически.

Самое интересное в исследовании это то, что базовый агент без всяких наворотов, который просто чередует генерацию модели и фидбэк от компилятора, повторил все 9 успехов с задачами Эрдёша. Полная версия с эволюционным поиском и обучением с подкреплением давала ощутимый выигрыш только на самых тяжёлых задачах. Это укладывается в общий тренд последних месяцев: по мере роста качества foundation моделей простые агентные циклы догоняют сложные специализированные системы.

В отличие от подхода OpenAI с неформальными доказательствами, здесь формальная верификация работает как автоматический фильтр. Разбор провалов показал, что модель регулярно галлюцинирует леммы, ссылаясь на них как на уже установленные результаты, и часто маскирует основную сложность задачи, переписывая её в виде вспомогательной леммы. Неформальные доказательства такие ошибки пропускают, а Lean ловит их сразу.

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

Ограничения тоже честно описаны. Успехи сконцентрированы в комбинаторике, теории чисел и оптимизации, где математическая библиотека Lean уже зрелая. Задачи, требующие построения существенно новой теории, пока остаются недосягаемыми. Большая часть проблем Эрдёша так и не решена.

Источник: https://x.com/kimmonismus/status/2058673672169107757