Google DeepMind 12 января выложила статью, где заявляет о новой теореме в алгебраической геометрии. Доказывали с помощью внутренней математической версии Gemini. Это на фоне недавних разговоров о том, как GPT-5.2 Pro решает задачи Эрдёша, так что все смотрят внимательно.
Сама теорема про «мотивные классы пространств отображений рода 0 в флаговые многообразия». Не буду делать вид, что понимаю, о чём речь. И вы не делайте, если только не занимаетесь алгебраической геометрией профессионально. А вот что действительно любопытно, спрятано в приложении к статье: описание самого процесса.
Президент Американского математического общества высказался
Рави Вакил, математик из Стэнфорда и действующий президент AMS, стал соавтором работы. Он назвал вклад Gemini «озарением, которым я бы гордился сам». Сильное заявление от человека, который буквально написал учебник по алгебраической геометрии.
Но есть нюанс. Вакил признал, что «возможно, со временем пришёл бы к этому выводу сам», но утверждать наверняка не может. Осторожная формулировка. ИИ нашла то, что эксперт мог бы найти. А могла бы и не найти.
Главный вывод Вакила: «осмысленный математический прогресс возник из этого подлинного симбиоза человеческой изобретательности и вклада Gemini». Симбиоз. Не автономия. Запомните это слово.
Как это работало на практике
В статье описана методология, и там нет ничего похожего на «дали модели теорему, получили доказательство». Если верить материалам:
Команда использовала декомпозицию, разбив сложную теорему на простые подзадачи. Начали с того, что скормили Gemini простые частные случаи, чтобы убедиться, что модель понимает определения. В промптах буквально были строки вроде «чтобы убедиться, что ты меня понимаешь, скажи, какие [объекты] ты бы выбрала».
Когда модель застревала, исследователи не просто перегенерировали ответ. Они анализировали частично верные выводы, находили полезное зерно и писали новые промпты: «попробуй использовать эту стратегию из предыдущего шага, но для общего случая». Это не модель рассуждает. Это люди рассуждают о выводах модели.
Успешные доказательства простых подзадач добавляли в контекст для более сложных. По сути, команда построила лестницу задач от простого к сложному, чтобы модель могла по ней подняться. Кто-то должен был спроектировать эту лестницу.
Исследователи читали выводы модели практически на каждом шаге. В одном случае они заметили, что модель сделала неочевидное наблюдение в частичном решении. Человек проверил его и сказал модели: «это хорошая идея, используй её для всего остального».
«Полностью написано людьми»
В статье есть важная оговорка: «изложение в этой работе полностью написано людьми (за исключением фрагментов в приложении, которые явно помечены)».
Итак, у нас доказательство с участием ИИ, где финальный текст написан людьми, декомпозиция задачи придумана людьми, проверка выполнена людьми, стратегическое направление задано людьми. Что именно сделала Gemini?
ИИ оказалась полезна для «рутинных задач вроде поиска связей с междисциплинарными статьями и написания кода для генерации данных». Но Вакил также сказал, что «самым поразительным было то, как это продвинуло проект интеллектуально». Это разные утверждения.
Сравнение с GPT-5.2 показательно
Всё это происходит на фоне дискуссий о задачах Эрдёша. GPT-5.2 Pro недавно решила задачу Эрдёша №397, и филдсовский лауреат Теренс Тао принял доказательство после его формализации в Lean. GPT-5.2 к этому моменту решила задачи №728, №729 и №397.
Но Тао подчеркнул, что это «самые доступные» задачи, решаемые стандартными методами, а не глубокие прорывы. И даже результат с №728 шёл с тремя оговорками: исходная формулировка была неоднозначной, похожие результаты уже были в литературе, а «автономное» решение включало несколько моделей с человеческой координацией на каждом этапе.
Статья DeepMind честнее относится к сотрудничеству. Она не заявляет об автономии.
Что это на самом деле демонстрирует
Работу делала команда Blueshift из DeepMind: исследователи Фредди Мэннерс и Г. Салафатинос вместе с академическими коллегами, включая Джима Брайана и Балажа Элека. DeepMind продвигает ИИ для математики с тех пор, как их системы AlphaGeometry и AlphaProof достигли уровня серебряной медали на Международной математической олимпиаде в 2024-м. Gemini Deep Think взяла золотой уровень на IMO 2025, решив пять из шести задач.
Но олимпиадная математика и исследовательская математика — разные вещи. У олимпиадных задач есть известные решения. Исследование означает поиск чего-то нового. Эта статья претендует на исследование. Вот что интересно.
В разделе методологии упоминается система FullProof, которую использовали в работе, но подробностей о её устройстве нет. Вероятно, что-то похожее на подходы с рассуждениями Pro-моделей от OpenAI или собственный Deep Think от DeepMind.
Неудобная середина
Ни «ИИ теперь может автономно заниматься математическими исследованиями», ни «это просто продвинутый автокомплит» не описывают происходящее точно.
Точнее будет так: модели ИИ теперь могут осмысленно участвовать в математических исследованиях, если встроены в тщательно спроектированный людьми процесс, с экспертным контролем на каждом шаге, со стратегическими промптами, которые по сути учат модель структуре задачи. Впечатляет это или разочаровывает — зависит от ваших ожиданий.
Вакил нашёл «как осмысленный математический прогресс возник из этого подлинного симбиоза». Акцент на симбиозе, а не замене, кажется намеренным. Люди-математики по-прежнему делают тяжёлую концептуальную работу. ИИ ускоряет некоторые части.
В статье не уточняется, что делает FullProof и сколько вычислительных ресурсов потребовалось. Я написал в DeepMind за подробностями. Пока без ответа.
Следите за следующими публикациями. DeepMind запустила инициативу AI for Math в партнёрстве с институтами вроде Имперского колледжа Лондона для исследования математики с участием ИИ. Будет больше результатов, и постепенно станет яснее, что эти инструменты могут и чего не могут.
