Одна из самых мощных моделей Anthropic, Claude Fable 5, построила доказательство математической гипотезы, которую специалисты по квантовой оптимизации не могли доказать с 2014 года. Результат описан в препринте исследователей из Гарварда и MIT — Ури Кола, Маора Бен-Шахара, Кфира Сулимани и Дирка Энглунда. Главное отличие от прошлых громких заявлений в духе «ИИ решил математику»: корректность доказательства проверяла не комиссия рецензентов, а программа — система формальной верификации Lean 4, которая принимает результат, только если каждый его шаг логически безупречен.
Речь о гипотезе Фархи, Голдстоуна и Гутмана — авторов популярного квантового алгоритма оптимизации QAOA. Они описали удобный тестовый пример под названием «ring of disagrees» («кольцо несогласных»): по кольцу расставлены спины — крошечные стрелки, — и развернуть их надо так, чтобы каждая смотрела в сторону, противоположную соседям. Авторы предсказали, что QAOA глубины p достигает на ней ровно (2p+1)/(2p+2) от наилучшего возможного результата. Отдельные простые случаи удавалось доказать и раньше, а позже формулу подтвердили численно вплоть до глубины 128 — но строгого доказательства в общем виде не было больше десяти лет: существование нужных настроек алгоритма выводили из подсчета параметров, а это не доказательство.
Важно отметить разделение труда. Исследователи проделали всю подготовительную работу: собрали в Lean библиотеку определений квантовой механики, формализовали известные части задачи и свели всю гипотезу к одному недостающему утверждению, зафиксировав его заранее. А дальше отдали этот пробел модели — с задачей закрыть его, написав доказательство прямо на языке Lean. Работа шла циклом: Fable 5 предлагала план словами, проверяла его численно, переводила в формальный код, получала от компилятора список ошибок и переписывала — пока система не приняла результат. Любопытнее всего, как именно модель это сделала: она нашла скрытую симметрию задачи и позаимствовала инструменты из соседней области — quantum signal processing, метода работы с однокубитными преобразованиями. Это превратило вопрос о существовании решения в явную конструкцию. Заодно у модели получилось объяснить, откуда вообще берется формула (2p+1)/(2p+2), которую двенадцать лет видели только в численных расчетах.
А теперь подвох. За сутки до выхода этого препринта, 28 июня, ту же самую гипотезу доказал математик Кунал Марваха — независимо и фактически тем же ключевым приемом, сведя задачу к паре многочленов через тот же quantum signal processing. И его доказательство тоже написано с помощью ИИ: Марваха активно пользовался ChatGPT 5.5 Pro и отчасти Claude Opus 4.8. Вышло почти синхронное независимое открытие — классический в истории науки сигнал, что задача попросту созрела (так Ньютон и Лейбниц параллельно построили математический анализ, а Дарвин и Уоллес — теорию эволюции). Новизна лишь в том, что сегодня к одному финишу одновременно приходят не два ученых, а два разных конвейера «человек плюс ИИ».
Это и задает честную рамку для оценки. Lean гарантирует, что доказательство безупречно следует из формулировки, — поэтому модели можно не верить на слово: выдуманный или ошибочный шаг просто не скомпилируется. Но проверить, что сама формулировка верно описывает исходную гипотезу, по-прежнему должен человек — узкое место не исчезает, а сдвигается с доказательства на постановку задачи. Поэтому точный итог звучит не как «ИИ обошел людей», а скромнее и интереснее: ИИ стал инструментом, способным самостоятельно пройти трудный участок и предъявить машинно-проверяемый результат. А то, что в этот раз к тому же финишу независимо пришел и человек, — лучшее напоминание, где пока проходит граница.
P.S. Поддержать меня можно подпиской на канал «сбежавшая нейросеть», где я рассказываю про ИИ с творческой стороны.
ссылка на оригинал статьи https://habr.com/ru/articles/1054060/