ИИ от Google решил математические задачи, остававшиеся открытыми 56 лет, за несколько сотен долларов

Исследовательская система Google DeepMind получила полные, проверенные машиной доказательства для девяти открытых задач, поставленных математиком Палом Эрдёшем, две из которых оставались нерешёнными 56 лет. Та же система закрыла 44 гипотезы, взятые из Онлайн-энциклопедии целочисленных последовательностей, решила пятнадцатилетний открытый вопрос алгебраической геометрии и улучшила известную оценку в выпуклой оптимизации. Бросающаяся в глаза цифра важна меньше, чем метод. Каждое из этих доказательств не просто заявлено машиной, а проверено ею.

Эрдёш, умерший в 1996 году, оставил сотни точных и упрямых вопросов, многие из которых легко сформулировать и мучительно трудно закрыть. За десятилетия они стали своего рода постоянным экзаменом для этой области. Гипотезы о последовательностях берутся из открытой базы данных, в которой математики ищут закономерности и где угаданная формула может годами оставаться недоказанной. Это не искусственные тесты, придуманные, чтобы польстить модели. Это реальный завал открытой математики.

Именно в этом различии вся суть. Система под названием AlphaProof Nexus пишет свои рассуждения на Lean — формальном языке, чей компилятор отбрасывает любой шаг, который не может подтвердить. Доказательство либо проходит, либо нет, и нет места уверенному абзацу, который потом оказывается ошибочным. Для того, кто пытается понять, реально ли «открытие» ИИ, здесь и проходит граница между пресс-релизом и результатом.

Рекомендуем к прочтениюInstagram тестирует ярлык «AI-creator» и оставляет решение за создателями

Внутри решатель работает на Gemini 3.1 Pro, а модель полегче отвечает за ранжирование. Цикл почти скучен. Модель набрасывает доказательство на Lean, компилятор возвращает ошибки, и эти ошибки питают следующую попытку. Честность держится на символической обратной связи, а не на гладком тексте. Команда построила четыре версии нарастающей сложности, одна из которых порождает и ранжирует конкурирующие наброски доказательств. И всё же самая простая версия — обычный цикл из модели и компилятора — в одиночку решила все девять задач Эрдёша.

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

Оговорки весят больше заголовка. Девять решённых из 353 испытанных задач Эрдёша — это доля попаданий около 2,5 процента. Цифра по последовательностям, 44 из 492, ниже девяти процентов. Авторы прямо признают, что большинство этих задач остаётся вне досягаемости, тем более те, что требуют обширной новой теории, и что успехи скапливаются там, где математическая библиотека Lean уже глубока. Уберите эти возведённые людьми леса и тщательно подобранный список целей — и системе почти не на чем стоять.

Осторожность заслуженна. В одном осмеянном эпизоде конкурирующая лаборатория объявила, что её модель решила десять задач Эрдёша, пока математики не указали, что ответы уже были в опубликованной литературе. Модель их нашла, а не доказала. AlphaProof Nexus построен так, чтобы быть невосприимчивым к этой ошибке. Доказательство на Lean известного результата всё равно остаётся верным, а доказательство на Lean чего-то по-настоящему нового подделать нельзя. Демис Хассабис, возглавляющий DeepMind, особо подчеркнул, что эта работа не является общим искусственным интеллектом, — необычно осторожная ремарка для компании, редко стесняющейся своих моделей.

Есть и более тонкая выгода, которую отмечают исследователи. Полезны оказались даже неудачи. Поскольку каждое частичное доказательство проверяется формально, математики могли точно видеть, какие подцели система способна закрыть, а какие нет, не перепроверяя всё рассуждение вручную. Машина перестаёт быть оракулом и становится неутомимым соавтором, который показывает свою работу и указывает, где по-прежнему прячется трудная часть.

Результат не стоит особняком. Он приходится на тот же период, что и отдельное заявление конкурирующей рассуждающей модели, которая, как сообщается, опровергла примерно 80-летнюю гипотезу Эрдёша в дискретной геометрии — вывод, который действующие математики уточнили и поддержали. Две лаборатории, два метода — один опирается на формальную проверку, другой на сырые цепочки рассуждений — вышли к одному рубежу с разницей в недели. Соревнование больше не о чат-ботах, которые звучат умно.

Работа изложена в статье, опубликованной в этом месяце, и методы опираются на открытые инструменты, а именно на Lean и его созданную сообществом библиотеку, так что сторонние группы могут проверить и повторно прогнать доказательства, а не верить корпоративному блогу. В DeepMind не сказали, попадёт ли система к исследователям за пределами компании. Следить стоит не за девяткой. Вопрос в том, превратятся ли эти 2,5 процента в десять, а затем в двадцать, потому что в тот день спор о том, для чего нужны эти машины, придётся начинать заново.

Похожие материалы

Grok Build CLI от xAI идёт напрямую против Claude Code в вашем терминале за 99 долларов

Стратегический альянс: «Говорящий Том» и «Леди Баг» запускают мультиплатформенный кроссовер

Maestro: игра о дирижировании в VR получила DLC по «Звёздным войнам» и вышла на PSVR2

iOS 26.5 наконец зашифрует сообщения между iPhone и Android

Mac-агент Perplexity стоит 200 долларов в месяц и читает вашу почту

Переворот в мире раскладушек: Как Samsung Galaxy Z Flip 7 наконец повзрослел