Агент AlphaProof Nexus от Google DeepMind решил 9 из 353 открытых математических задач Пала Эрдёша, две из которых оставались нерешёнными 56 лет. Система также доказала 44 из 492 гипотез из Онлайн-энциклопедии целочисленных последовательностей. На решение каждой задачи Эрдёша тратилось по несколько сотен долларов.
В отличие от обычных чат-ботов, система использует язык Lean для формализации доказательств. ИИ предлагает решение, которое проходит машинную проверку каждого логического шага. Если система находит ошибку, агент получает обратную связь и продолжает поиск. Результат считается верным только после прохождения строгой проверки.
Архитектура AlphaProof Nexus включает несколько ИИ-агентов, работающих параллельно под управлением эволюционного алгоритма. Для отдельных этапов используется система AlphaProof, основанная на обучении с подкреплением. Сравнение с более простым агентом показало, что организация поиска напрямую влияет на стоимость решения сложных задач.
Система применяется в алгебраической геометрии, выпуклой оптимизации, теории графов и квантовой оптике. Она помогла обнаружить ошибки в научной литературе. При этом агент ограничен задачами, где есть развитая библиотека формализованных результатов, и пока не способен разрабатывать новые математические теории с нуля.
