Пока GPT-5.2 решает задачи Эрдёша, Gemini доказывает теоремы: новости ИИ-математики

Пока GPT-5.2 решает задачи Эрдёша, Google DeepMind осваивает другой формат: математики из Стэнфорда и DeepMind опубликовали статью по алгебраической геометрии, где доказательство теоремы нашли с помощью Gemini Deep Think. Это первый известный случай, когда LLM участвует в открытии теоремы в исследовательской математике — не олимпиадной задачи и не проблемы из готового списка. Статья посвящена мотивному классу пространства отображений рода 0 в флаговое многообразие — объекту на стыке алгебраической геометрии и топологии.

Работа с AI строилась итеративно. Сначала авторы сформулировали гипотезу и проверили ее численно. Затем составили "лесенку" из упрощенных подзадач и скормили ее Gemini Deep Think. Модель решила частные случаи, математики проанализировали ход рассуждений, выделили ключевые идеи — и попросили AI обобщить. Кроме публичного Gemini Deep Think использовали FullProof — неопубликованную систему DeepMind для генерации математических доказательств, построенную на базе Gemini. Инструмент разработал один из соавторов статьи, Джордж Салафатинос. Это первое публичное упоминание FullProof.

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

Статья показывает, что AI-инструменты выходят за пределы тестовых форматов — олимпиад и задач из готовых баз. Если связка GPT-5.2 с Aristotle берет прямой генерацией с формальной верификацией, то подход DeepMind требует диалога и человеческой интерпретации, но работает на задачах, где готового ответа нет ни в какой литературе.

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