24 мая компания Google DeepMind опубликовала статью, в которой описывается работа автономного агента LLM-Lean. Этот агент самостоятельно решил 9 из 353 открытых задач Эрдёша — некоторые из них оставались нерешёнными более 50 лет — и доказал 44 из 492 гипотез OEIS, при этом затраты на решение каждой задачи составили всего несколько сотен долларов. Подробности системы изложены в публикации на сайте arXiv ([2605.22763] Advancing Mathematics Research with AI-Driven Formal Proof Search). В её основе лежит использование языка больших моделей для формулировки доказательств и компилятора Lean для их формальной проверки; последний автоматически анализирует каждый логический шаг. Человеческая проверка проводится лишь после того, как Lean подтверждает корректность выводов. Кроме того, агент разрешил проблему из области алгебраической геометрии, которая оставалась нерешённой 15 лет, и обнаружил новый алгоритмический параметр в теории оптимизации.
Один из ключевых выводов статьи заключается в том, что даже простой агент, чередующий генерацию текста с помощью LLM и получение обратной связи от компилятора, смог повторить все 9 успехов в решении задач Эрдёша. Более сложная система, включающая эволюционный поиск и обучение с подкреплением, демонстрирует превосходство лишь при решении наиболее трудных задач; это позволяет предположить, что усовершенствование базовых моделей важнее усложнения архитектуры системы. Анализ ошибок показал, что ИИ часто «выдумывал» вспомогательные утверждения и скрывал суть проблем, переформулируя их в виде таких утверждений; компилятор Lean безошибочно выявлял эти недочёты, чего не удавалось добиться при использовании неформальных методов доказательства. На данный момент успехи агента наблюдаются в комбинаторике, теории чисел и оптимизации — областях, где математическая библиотека Lean (Mathlib) наиболее развита; задачи, требующие создания совершенно новых теоретических концепций, пока остаются ему недоступными.
Гэри Маркус охарактеризовал данный подход как нейросимвольный и назвал его «более взвешенным и количественно обоснованным», чем неформальные попытки доказательств со стороны OpenAI; это породило вопрос: не спешило ли само OpenAI с публикацией собственных результатов, зная о грядущем прорыве DeepMind. Нейт Соарес отметил, что основные СМИ практически проигнорировали это событие, объяснив это «сонным состоянием» общества перед лицом появления трансформационных технологий ИИ. За первые сутки публикация набрала 2,6 миллиона просмотров.