ИИ-система AlphaProof Nexus решила девять из 353 задач Эрдёша, которые исследователи предложили ей, и доказала 44 из 492 гипотез о числовых последовательностях. Две решённые задачи оставались открытыми более полувека. Результаты исследования опубликованы в журнале Science 8 октября 2026 года. [1]
Работа была доступна ещё с 21 мая в виде препринта — версии статьи до журнальной публикации. Поэтому появившееся 12 октября освещение результатов не означает, что систему представили сегодня. [2], [4]
Что доказала система
Исследователи проверяли AlphaProof Nexus на открытых научных задачах — вопросах, для которых ещё не было известно доказательство. Это следующий шаг после применения ИИ к олимпиадной математике, где решение задачи уже существует.
Один из наборов включал гипотезы из OEIS — онлайн-энциклопедии целочисленных последовательностей. В ней собраны ряды целых чисел, их свойства и связи; некоторые предполагаемые свойства ещё требуют доказательства. Большинство задач из обоих наборов в этом эксперименте осталось без решения. Результат относится к выбранным задачам и условиям проверки: он не показывает, какую долю всех открытых математических вопросов система способна решить. [1]
Как проверяются доказательства
Языковая модель строит доказательство на Lean — формальном языке, на котором математические утверждения и шаги рассуждения записываются так, чтобы их могла проверить программа. Lean проверяет, следует ли заключение из заданных условий и предыдущих шагов.
Если проверка обнаруживает ошибку, система получает сообщение о ней. Модель исправляет доказательство и снова отправляет его на проверку. Система повторяет этот цикл, пока ищет решение; итоговое доказательство должно пройти проверку целиком, без пропусков, оставленных вместо обоснования.
Такой подход позволяет обнаруживать логические ошибки, которые в обычном ответе могут выглядеть убедительно, как и другие галлюцинации LLM. В расширенной конфигурации агенты также могут обращаться к специализированному инструменту AlphaProof для поиска отдельных частей доказательства. [2]
Что остаётся за математиками
У программной проверки есть важное условие: записанное на Lean утверждение должно точно передавать исходную математическую задачу. Если при переводе изменился смысл, корректное доказательство будет отвечать на другой вопрос. В исследовании специалисты отдельно проверяли соответствие формальных утверждений исходным гипотезам. Эта работа остаётся необходимой частью оценки результата. [2]
Авторы выложили доказательства на Lean и их изложения, написанные людьми обычным математическим языком. Читатель может изучить формальную запись и ход рассуждения в открытом репозитории. [3]
Здесь виден принцип, который в разработке ИИ-систем называют harness engineering: результат зависит от инструментов и обратной связи вокруг модели. В этом случае математический вывод проходит строгую программную проверку. Переносить такую уверенность на произвольные ответы ИИ оснований нет: для них нужны собственные способы проверки, соответствующие задаче.
