Новый агент Google, который решал открытые задачи по математике

Часто говорят: harness не важен, главное, насколько умная модель. Но если просто попросить Gemini “реши открытые задачи Эрдёша”, она не начнёт стабильно выдавать проверяемые доказательства. В работе Google интересен именно harness: как вокруг Gemini собрали систему, которая хранит частичные Lean-доказательства, продолжает удачные ветки и не теряет полезные ошибки прошлых запусков.

Обычный coding agent работает линейно: получил задачу, написал код, запустил проверку, исправил ошибки, снова проверил. Для Lean-доказательств это тоже работает: модель видит theorem statement, пишет доказательство, Lean возвращает ошибки, модель правит файл.

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

Одна попытка в агенте Google называется episode. Внутри episode Gemini 3.1 Pro правит Lean-файл. После правки запускается Lean. Все ошибки в доказательстве попадают в модель обратно.

Если остаётся конкретная незакрытая Lean-цель, Gemini может вызвать AlphaProof. Это работает как маленькая модель-субагент: он пытается закрыть одну подцель.

После episode результат не выбрасывается, если у модели было хоть какое-то продвижение. Из него делают sketch.

Sketch, это текущая версия Lean-доказательства. Не просто текстовая идея, а Lean-файл: часть доказательства уже написана, часть целей ещё открыта. Рядом лежит план, summary, список целей и вызовы AlphaProof.

Новая попытка обычно стартует не с пустого файла. Агент выбирает из базы один root sketch и два inspiration sketches.

Root sketch, это основной черновик. Его Lean-код Gemini реально продолжает редактировать. Если root уже содержит полезную лемму или частично закрытое доказательство, новая попытка наследует этот прогресс.

Inspiration sketches, это дополнительные черновики в prompt. Их код не становится стартовым файлом. Они нужны как подсказки: в другой ветке пробовали такую лемму, там была такая ошибка, там AlphaProof закрыл такую подцель, там план выглядел перспективно.

Все попытки доказательств оцениваются отдельной моделью Gemini Flash, чтобы получить score для каждого sketch. Root sketch не обязательно выбирается как самый лучший по score. Sketches семплируются: сильные черновики получают больше шансов, но менее исследованные ветки тоже иногда выбираются. Так модель не циклится на одном подходе и получает больше exploration.

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

Подагенты напрямую не общаются. Один prover-subagent не пишет другому. Обмен идёт через базу sketches и global goal cache.

Результат: 9 из 353 формализованных задач Эрдёша и 44 из 492 OEIS-гипотез.

P.s. lean это язык формальной верификации математики. На ней можно написать любое утверждение или доказательство любой теоремы и компилятор сможет верифицировать, правильное ли оно.