AlphaProof Nexus решил 9 открытых задач Эрдёша

AlphaProof Nexus решил 9 открытых задач Эрдёша

AlphaProof Nexus — это исследовательская система Google DeepMind, которая соединяет LLM, то есть большую языковую модель, с формальной проверкой доказательств в Lean. Lean — язык и среда, где математическое доказательство проверяется как строгая программа: если шаг не следует из правил, компилятор его не принимает. AI Digest (ai-digest.ru) разбирает событие: система автономно нашла доказательства для девяти открытых задач Эрдёша и показала, что AI может помогать не только в учебной математике, но и в исследовательских проблемах.

Что именно решил AlphaProof Nexus?

Команда опубликовала результаты для набора открытых математических задач, связанных с каталогом Эрдёша. Система пыталась решить 353 задачи и успешно закрыла 9 из них. Две задачи оставались открытыми десятилетиями, а это важно: речь не о школьных олимпиадных упражнениях, а о вопросах, для которых у математиков долго не было полного доказательства.

Отдельно система доказала 44 открытые гипотезы из OEIS, онлайн-энциклопедии целочисленных последовательностей. Такая база хранит закономерности вроде последовательностей чисел, но доказать, что закономерность верна всегда, намного сложнее, чем угадать несколько следующих чисел.

Как работает связка LLM и Lean?

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

Такой подход отличается от обычного ответа чат-бота. Модель может красиво объяснить решение и всё равно ошибиться в логике, поэтому AI Digest уже разбирал, почему галлюцинации LLM остаются системной проблемой. В AlphaProof Nexus важна не уверенность текста, а машинная проверка каждого шага.

Почему показатель 9 из 353 всё равно важен?

На первый взгляд доля успеха около 2,5% кажется скромной. Но для открытых исследовательских задач это не провал, а демонстрация нового инструмента. Большинство задач из такого набора могут быть слишком трудными или требовать идей, которых модель пока не находит. Зато успешные случаи показывают, что AI способен не просто пересказывать известные решения, а участвовать в поиске новых формальных доказательств.

Экономика тоже меняется. По опубликованным оценкам, вычислительные расходы на успешную задачу составляли всего несколько сотен долларов. Для академической математики это не отменяет работу людей, но делает массовые попытки формального поиска заметно доступнее. Похожую идею AI Digest рассматривал в материале про AI-агентов и Wolfram Engine для персональной математики: ценность появляется там, где модель соединяют с проверяемым инструментом.

Что это меняет для AI-исследований?

Главный вывод в том, что будущие научные AI-системы будут сильнее не как «умные собеседники», а как циклы: предложить ход, проверить его, получить ошибку, исправить и повторить. Такой контур похож на работу coding agent, только вместо тестов и компилятора кода здесь используется формальная математика. Это роднит AlphaProof Nexus с более широкой темой AI-агентов, которые получают обратную связь от инструментов, а не только от пользователя.

Для рынка AI это событие не означает мгновенную автоматизацию науки. Но оно уточняет направление: модели становятся полезнее, когда их ответы можно проверять независимой системой. Именно поэтому связки LLM + проверяющий инструмент могут стать практичнее, чем чистая гонка за более уверенными текстовыми ответами. В математике таким проверяющим слоем стал Lean; в бизнесе похожую роль могут играть тесты, аудит данных и строгие метрики качества.