Исследовательское подразделение Google DeepMind продемонстрировало впечатляющие результаты в области автоматизированного доказательства теорем, решив десятки открытых математических задач. Согласно публикации в журнале Science, новая система AlphaProof Nexus сумела самостоятельно найти решения для девяти из 353 задач Эрдёша, при этом две из них оставались нерешенными более полувека. Как сообщает издание The Decoder, команда разработчиков предпочла сначала верифицировать свои результаты через академическое сообщество.

Помимо успехов с наследием Пала Эрдёша, система доказала 44 гипотезы из базы целочисленных последовательностей OEIS и нашла ответ на открытый вопрос в алгебраической геометрии. Любопытно, что ИИ также улучшил известную границу в минимаксной оптимизации — методе, который, по иронии судьбы, сам активно применяется при обучении нейросетей. Архитектура системы опирается на Gemini 3.1 Pro, которая берет на себя роль чертежника, набрасывая и редактируя доказательства на формальном языке программирования Lean.

Механика доказательства и роль Lean

Процесс работы AlphaProof Nexus напоминает итеративную разработку программного обеспечения, где компилятор выступает в роли строгого судьи. Lean проверяет каждый черновик после любого изменения, а возникающие сообщения об ошибках служат своего рода дорожной картой для следующей попытки модели. Если задача оказывается слишком крепким орешком, система подключает AlphaProof — специализированный инструмент, отточенный именно под математические доказательства. Впрочем, девять знаковых задач Эрдёша поддались системе даже без этой поддержки.

Хронология развития событий показывает, что DeepMind выбрала путь классической науки в противовес недавним действиям конкурентов. В то время как OpenAI просто выложила сотни сгенерированных ИИ доказательств на GitHub, фактически предложив академическому миру разбираться с этим массивом самостоятельно, команда Google пошла по пути рецензирования. Это решение выглядит особенно значимым на фоне призывов к бойкоту ИИ-доказательств со стороны части математиков под руководством Теренса Тао.

Интеграция LLM с формальными верификаторами вроде Lean превращает галлюцинирующий алгоритм в строгого логика, где каждая итерация подтверждается математическим фундаментом. Однако успех в комбинаторике и теории чисел не означает, что ИИ обрел интуицию; скорее, мы видим триумф высокоскоростного перебора в жестко заданных рамках. Пока корпорации спорят о методах публикации, фундаментальная математика рискует превратиться в полигон для тестирования вычислительных мощностей, где элегантность решения приносится в жертву грубой силе оптимизации.

Для профессионального сообщества этот кейс интересен не столько количеством решенных задач, сколько отладкой процесса взаимодействия нейросетей и формальных систем. Мы видим, как Gemini 3.1 Pro обучается на собственных ошибках в режиме реального времени, что минимизирует риск логических провалов, столь характерных для стандартных текстовых моделей. Это создает определенный стандарт для будущих разработок, где «честное слово» модели заменяется строгим протоколом верификации кода.

Человеческий фактор в этой истории остается ключевым: несмотря на вычислительную мощь, именно признание со стороны экспертов через рецензирование легитимизирует эти достижения. Пока одни игроки рынка пытаются завалить науку сырыми данными, другие аккуратно встраивают ИИ в существующие институты. В конечном счете, вопрос не в том, может ли машина решать задачи, а в том, готовы ли мы доверять этим решениям без многоступенчатой проверки человеком.