Google DeepMind опубликовал препринт про агента AlphaProof Nexus, который автономно нашел формальные доказательства для 9 из 353 открытых задач из каталога венгерского математика Пола Эрдёша. Медианная стоимость успешной попытки — около $200, разброс от $20 до $800.

Среди решенных — задача #12 Эрдёша и Шаркози из 1970 года, которая была открыта 56 лет: построить бесконечное множество натуральных чисел, в котором ни одно число не делит сумму двух больших. И задача #125 из 1996-го — про плотность сумм специально построенных множеств в системах счисления с основаниями 3 и 4. Доказательства не банальные: например, для #125 агент построил аргумент, опирающийся на близость степеней тройки и четверки (3^m ≈ 4^k).

Эрдёшем агент не ограничился. По другим направлениям результаты такие:

  • 44 из 492 открытых гипотез из онлайн-энциклопедии целочисленных последовательностей OEIS;

  • 15-летняя задача о функциях Гильберта в алгебраической геометрии;

  • улучшенная оценка сходимости для одного из алгоритмов выпуклой оптимизации;

  • задача #57 из известного списка открытых задач британского математика Бена Грина;

  • текущие исследования по квантовой оптике с Марио Кренном и по теории графов.

Архитектура простая. На вход агент получает Lean-файл с теоремой, где вместо доказательства стоит пустая заглушка. Gemini 3.1 Pro генерирует наброски доказательства, Lean-компилятор проверяет каждый шаг и возвращает ошибки обратно в модель, цикл повторяется. В полной версии поверх работает эволюционный алгоритм: пул субагентов берет наброски из общей базы, а отдельные экземпляры Gemini 3.0 Flash сравнивают эти наброски между собой и выставляют им Elo-рейтинги — как в шахматах. Дополнительно агент может вызывать AlphaProof, олимпиадную систему DeepMind на обучении с подкреплением, как инструмент для отдельных подцелей.

Самое интересное в препринте — раздел, где DeepMind проверяет, нужны ли вообще все навороты их архитектуры. Они взяли те же 9 задач и прогнали на них упрощённые версии агента: без эволюционного алгоритма, без вызова AlphaProof, на меньших моделях. Результат неудобный для самих авторов: связка из одного Gemini 3.1 Pro и Lean-компилятора закрыла все 9 задач — на сложных дороже, но закрыла. Сам AlphaProof в одиночку, без LLM сверху, не решил ни одной даже при бюджете $60 на задачу. Меньшие модели (Gemini 3.0 Flash и Flash-Lite) тоже не справились ни с чем. Авторы прямо пишут о "сдвиге от специализированных обученных систем к простым агентным циклам по мере роста возможностей LLM". На фоне того, что за последние четыре месяца задачи Эрдёша уже закрывали GPT-5.2 в связке с Aristotle, внутренняя модель OpenAI, агент Aletheia от того же DeepMind и даже любитель с ChatGPT Pro за подписку $200 в месяц, формулировка звучит как тихое признание: специализированные доказательные системы свою эпоху отыгрывают.

P.S. Поддержать меня можно подпиской на канал "сбежавшая нейросеть", где я рассказываю про ИИ с творческой стороны.