AlphaProof Nexus решает задачи Эрдёша с помощью формальной логики

Математика перестала быть исключительно человеческой прерогативой: новая система от Google DeepMind, AlphaProof Nexus, самостоятельно справилась с девятью открытыми задачами из списка легендарного Пола Эрдёша. Некоторые из этих проблем оставались нерешёнными десятилетиями, а теперь получили доказательства благодаря комбинации языковой модели Gemini 3.1 Pro и верификатора Lean.

В отличие от стандартных нейросетей, которые могут выдавать правдоподобные, но ошибочные выводы, AlphaProof Nexus использует формальный язык Lean для проверки каждого логического шага. Если модель совершает ошибку, компилятор мгновенно указывает на неё, что исключает риск «галлюцинаций» и заставляет систему искать верный путь. Помимо задач Эрдёша, фреймворк успешно справился с 44 гипотезами из базы данных Нила Слоуна и закрыл 15-летнюю проблему в алгебраической геометрии.

Инструмент уже нашел применение в квантовой оптике и теории графов, при этом стоимость вычислений для каждой задачи составляет всего несколько сотен долларов. Несмотря на технологический прорыв, разработчики признают: из 353 задач Эрдёша система осилила лишь девять. Математик Терренс Тао отмечает, что пока такие успехи ограничены относительно простыми случаями, а ИИ выступает скорее помощником, чем полноценным исследователем, способным на фундаментальные прорывы в глубокой абстрактной математике.