AlphaProof Nexus решил 9 открытых задач Эрдёша с проверкой в Lean

Google DeepMind опубликовала в Science работу об AlphaProof Nexus — агентах, доказывающих теоремы на Lean с проверкой каждого шага компилятором. Лучший агент решил 9 из 353 открытых задач Эрдёша, включая две 56-летней давности, и 44 из 492 гипотез OEIS при затратах в несколько сотен долларов на задачу.

• Решены 9 из 353 задач Эрдёша и 44 из 492 гипотез OEIS
• Две задачи Эрдёша оставались открытыми 56 лет
• Инференс обходился в несколько сотен долларов на задачу
• Базовый цикл «генерация LLM + проверка Lean» повторил успех