Агент DeepMind решил 9 открытых задач Эрдёша

Система также доказала 44 из 492 открытых гипотез из Онлайн-энциклопедии целочисленных последовательностей (OEIS). На каждую решённую задачу Эрдёша уходило несколько сотен долларов на вычисления. Ключевое отличие агента от обычного чат-бота — использование Lean, языка и среды для формализации доказательств: ИИ предлагает доказательство в формальном виде, после чего Lean проверяет каждый логический шаг, а при обнаружении ошибки агент получает обратную связь и продолжает поиск.

В AlphaProof Nexus несколько ИИ-агентов параллельно ищут решения, проверяют подходы и уточняют доказательства. В наиболее сложной версии их работу координирует эволюционный алгоритм, а для отдельных этапов используется AlphaProof — система автоматического доказательства теорем на основе обучения с подкреплением. Авторы сравнили эту архитектуру с более простым агентом, чередующим генерацию доказательств языковой моделью и проверку в Lean: при повторном анализе девяти решённых задач Эрдёша простой агент тоже справился со всеми девятью, но на наиболее трудных задачах его использование обходилось дороже.

Система также помогла решить открытую задачу в алгебраической геометрии, улучшить оценку в выпуклой оптимизации и обнаружить ошибки в формализации математических утверждений в научной литературе. Её используют в исследованиях по теории графов и квантовой оптике. При этом большинство открытых задач Эрдёша агент решить не смог, а нынешние успехи сосредоточены в областях с развитой библиотекой формализованных результатов, где сложные рассуждения удаётся разбить на отдельные подзадачи. Система наследует ограничения языковых моделей: результаты могут сильно различаться от попытки к попытке, а задачи, требующие разработки обширной новой теории, остаются за пределами её возможностей.