Google DeepMind выпустил систему AlphaProof Nexus, которая автономно решила девять из 353 открытых задач Эрдёша — математического наследия венгерского учёного Пола Эрдёша, оставившего после себя сотни нерешённых вопросов. Две из решённых задач не давались математикам 56 лет.
Стоимость вычислений — несколько сотен долларов за задачу.
Система устроена иначе, чем подходы вроде o3 от OpenAI. Там языковая модель сама ведёт всю логическую цепочку на естественном языке. Здесь модель Gemini 3.1 Pro генерирует шаги доказательства на формальном языке Lean, а компилятор сразу проверяет каждый шаг. Если ошибка — сообщение об ошибке идёт обратно в модель как подсказка. Человек подключается только в самом конце.
Кроме задач Эрдёша система доказала 44 из 492 открытых гипотез из базы OEIS, закрыла 15-летний вопрос об алгебраической геометрии и улучшила известную оценку в выпуклой оптимизации.
Исследователи испытали четыре версии агента — от простой до полностью укомплектованной. Неожиданный результат: простейший агент (только LLM плюс обратная связь от компилятора) тоже справился со всеми девятью задачами — чуть дороже на самых сложных, но справился. Авторы объясняют это двумя факторами: быстрым ростом качества языковых моделей и «силой компилятора как заземления для рассуждений».
Общий показатель успеха — 2,5%. Большинство задач Эрдёша система не решила. Теренс Тао, один из крупнейших ныне живущих математиков, ранее предупреждал не переоценивать такие результаты: реальная доля решённых задач у AI держится около 1–2%, и в основном это более простые случаи.
Показательно другое: математики, работавшие с системой, говорят, что даже провальные попытки доказательства помогали лучше понять задачу. Формальные наброски позволяли сосредоточиться на нерешённых подзадачах, а не перепроверять всё с нуля. Система уже используется в текущих исследованиях по квантовой оптике и теории графов.
Все доказательства на Lean опубликованы на GitHub.
