Claude собрал доказательство теоремы Ферма в Lean

Claude за 11 дней, почти без участия людей, написал в Lean полное доказательство Великой теоремы Ферма. В 02:00:57 по UTC 18 августа корневое утверждение на платформе Prove2Me получило статус PROVED, а в рассуждениях модели появилась строка: «Корень FLT на prove2me в статусе PROVED. Исторический момент для этой кампании».

Подробности Anthropic опубликовала в посте 7 сентября. Масштаб такой: 13 млн строк кода на Lean, больше чем впятеро объёмнее Mathlib, главной общей библиотеки формальной математики, на которой это доказательство стоит. По пути агенты доказали 30 300 промежуточных теорем, из них в итоговое доказательство вошли 29 500. Работа съела около шести миллиардов выходных токенов внутренней исследовательской модели общего назначения, которую в Anthropic сравнивают с Claude Fable 5.1.

Зачем проверять то, что уже доказано

Нового математического результата здесь нет, и в Anthropic это подчёркивают сами: в отличие от недавней работы о гипотезе Римана, где Claude получил новую математику, здесь новое в проверке. Доказательство сверяют так, как сверяют вычисление на калькуляторе. Lean - это ассистент доказательств: он принимает рассуждение, только если каждый шаг выведен явно, даже самый тривиальный.

История самой теоремы показывает, почему это важно математикам. Эндрю Уайлс представил доказательство в июне 1993 года в серии лекций на три дня. Через два месяца проверки один из рецензентов задал вопрос, который вскрыл критическую дыру. Уайлс год пытался её закрыть, сначала один, потом со своим бывшим студентом Ричардом Тейлором, и был близок к тому, чтобы бросить проект, когда понял, что отброшенный раньше подход всё-таки работает. Корректное доказательство вышло в мае 1995 года и заняло 129 страниц. Ещё в 1908 году за доказательство объявили премию в 100 000 немецких золотых марок, и только за первый год прислали 621 неверную попытку.

Похожих историй в посте несколько. Доказательство гипотезы Кеплера, которое Томас Хейлз предложил в 1998 году, четыре года провело на рецензии, и комиссия из 12 рецензентов остановилась на формулировке «уверены на 99%». Позже Хейлз возглавил проект Flyspeck из двадцати человек и формализовал доказательство. У самого Тяньи Пэна, исследователя Anthropic, который запустил нынешний эксперимент, есть личная версия той же проблемы. В студенчестве научный руководитель хотел включить результаты из его дипломной работы в статью для Nature и спросил, уверен ли он в доказательстве. Пэн ответил честно: «Уверен на 99%, но в таком длинном доказательстве трудно быть уверенным на 100%». В Nature работа не попала.

Что делали люди

Пэн руководит в Колумбийском университете группой, которая делает инструменты для формализации с помощью ИИ, и хотел проверить, сможет ли Claude хотя бы продвинуться с теоремой Ферма. Результат, по словам Anthropic, оказался выше его ожиданий. Математический вклад людей свёлся к редким указаниям верхнего уровня от Пэна, вроде «якобиан как схема, похоже, в высоком приоритете» или «дожать теорему Мазура поскорее».

Всю остальную работу делали десятки агентов Claude. Они вводили определения, доказывали промежуточные теоремы и на их основе брались за всё более сложные утверждения. За основу взяли упрощённую версию доказательства Уайлса из изложения Анри Дармона, Фреда Даймонда и Ричарда Тейлора. План на Prove2Me распадался на три крупные подтеоремы, и граф близко повторял исходное доказательство Уайлса.

Anthropic выложила фрагменты рассуждений, в которых модель осознаёт, что сделала. Сначала осторожное «Исторический момент (с поправкой на перепроверку)», потом «R = T закрыто и каскадом дошло до корня. Это цель кампании: сквозное FLT на prove2me». R = T здесь - центральный шаг подхода Уайлса, утверждение, что кольцо деформаций совпадает с алгеброй Гекке. Как только оно было доказано, статус «доказано» поднялся по графу зависимостей до самой теоремы.

Почему не вышло с первого раза

Несколько первых попыток провалились. Агенты быстро добивались частных успехов, но затем теряли представление о том, в каком состоянии проект, и переставали нормально работать вместе. От этих неудачных заходов в итоговом доказательстве осталось около 7% строк, если не считать шаблонного кода.

Дело пошло после перехода на Prove2Me, открытую платформу для совместной формализации, которую Пэн сделал с коллегами из Колумбийского университета. Её описывает препринт на arXiv Чена, Марвахи, Лу, Юэна и Пэна. По словам Anthropic, платформа помогла в трёх местах:

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

Поверх платформы работала мультиагентная обвязка на базе Claude Code. Вместе с ней команда агентов закончила доказательство чуть меньше чем за две недели.

Что именно проверил Lean

Готовое доказательство прошло проверку Lean и опирается только на три стандартные аксиомы Lean. Отдельный инструмент-сравниватель подтвердил, что доказанное утверждение совпадает с формулировкой теоремы Ферма в самой Mathlib. Код доказательства и письменный разбор его хода выложены на GitHub.

Anthropic показала результат Кевину Баззарду из Imperial College London, который с 2024 года ведёт общественный многолетний проект формализации теоремы Ферма в Lean. Его оценка:

Это выдающееся достижение автоформализации, на которое, по словам исследователей Anthropic, ушло всего 11 дней, доказывает Великую теорему Ферма без каких-либо допущений, кроме аксиом математики. По ходу мы видим автоформализацию алгебры, гармонического анализа, геометрии и теории чисел и узнаём, что артефакты автоформализации, созданные ИИ, теперь достаточно надёжны, чтобы на них можно было строить дальше; доказательство многослойное.

Про объём в 13 млн строк в Anthropic оговариваются в сноске: Mathlib компактна и хорошо отрецензирована, а доказательство Claude, скорее всего, намного длиннее, чем нужно. Начинали агенты не с нуля: в доказательство вошли адаптированные куски из проекта Imperial College London и из проекта flt-regular.

Проект Баззарда сообщество планировало на годы. Только блупринт, подробный план с картой зависимостей, для начальной фазы проекта занимает 86 страниц. Проект финансируется грантом EPSRC до сентября 2029 года, говорится на его странице на GitHub. Там же указано, что маршрут почти целиком спланировал Ричард Тейлор в обсуждениях с Баззардом: это современный вариант доказательства Уайлса и Тейлора-Уайлса, который во многом опирается на идеи Харе и Винтенбергера. На сайте Lean этот подход называют версией «XXI века», которая учитывает более поздние работы Харе-Винтенбергера, Кисина и других. Там же теорему Ферма называют последним пунктом списка Фрека Видейка из 100 задач для компьютерной формализации, а от проекта ждали ещё и качественных данных для обучения ИИ-систем. Claude же шёл через изложение Дармона, Даймонда и Тейлора.

Свою мотивацию Баззард объяснял в блоге сообщества Lean: теория чисел отстаёт в формализации, и в большинстве недель Lean не знает достаточно современных определений, чтобы хотя бы сформулировать результаты, которые объявляют на Лондонском семинаре по теории чисел. Для сравнения он приводил формализацию прорыва в полиномиальной гипотезе Фреймана-Ружи, которую Теренс Тао с соавторами уложили в три недели.

Три подписки Max и теорема Виноградова

Баззард, просмотрев доказательство, говорит о последствиях шире одной теоремы: «Если автоматическая формализация FLT возможна уже сейчас, значит, мы сделали большой шаг к автоматической формализации современной математической литературы». По его словам, такие методы помогут вычищать ошибки из существующего корпуса, разгрузят рецензентов и дадут строго проверять математику, написанную языковыми моделями, а сейчас это, как правило, крайне затратный процесс, который ведут люди.

В Anthropic ожидают, что формализованное доказательство станет обычным приложением к любому тексту, рассчитанному на читателя-человека. Заменять понятное человеку изложение оно не должно, но, возможно, это единственный реальный способ для математиков успевать за потоком результатов от ИИ. Есть и обратный эффект: многие недавние результаты Claude формализовали параллельно с доказательством, и модель, судя по всему, использует частичные доказательства в Lean, чтобы проверять свои гипотезы, примерно как пишет численные симуляции, чтобы понять, верно ли идёт работа.

Для формализации других больших теорем и доработки Lean и Mathlib Anthropic предлагает внешним исследователям бесплатные и льготные подписки, кредиты и отдельные гранты под крупные проекты.

Отдельный опыт поставили на обычных подписках. Исследователи Anthropic взяли три личных плана Claude Max и поручили агентам формализовать приложения кругового метода Харди-Литлвуда. Работая только через Prove2Me, агенты за три дня формализовали теорему Виноградова о трёх простых.