Полное доказательство теоремы Ферма проверил Lean

Anthropic опубликовала первое полное доказательство Великой теоремы Ферма, которое от начала до конца проверяет компьютер: Claude написал его на языке Lean за 11 дней. Как сообщает Anthropic, модель работала в основном автономно, а сообщество закладывало на формализацию такой сложности годы работы.

Коротко

• Десятки агентов Claude работали параллельно через платформу Prove2Me, а математический вклад людей ограничивался редкими указаниями Тяньи Пэна общего характера, например заняться якобианом как схемой или быстрее закрыть теорему Мазура.
• Итоговый текст занимает 13 миллионов строк Lean и опирается на 29 500 промежуточных теорем; всего агенты доказали 30 300 утверждений и израсходовали около шести миллиардов выходных токенов внутренней исследовательской модели.
• Формализация переносит часть работы рецензентов на компьютер: по словам Кевина Баззарда из Imperial College London, такие методы помогут искать ошибки в существующей литературе и проверять математику, созданную языковыми моделями.

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

Проект сдвинулся после перехода на платформу Prove2Me

Ранние прогоны закончились неудачей: агенты добивались локальных успехов, но быстро теряли представление о состоянии проекта и переставали согласовывать работу. На эти попытки пришлось около 7% строк финального доказательства без учёта служебного кода. Открытую платформу для совместной формализации Prove2Me собрал исследователь Anthropic Тяньи Пэн вместе с коллегами из Колумбийского университета.

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

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

Lean принял доказательство на трёх стандартных аксиомах

Готовое доказательство проверил Lean: оно использует только три стандартные аксиомы системы, а отдельный компаратор подтвердил, что формулировка теоремы совпадает с формулировкой из Mathlib. По объёму 13 миллионов строк более чем в пять раз превышают саму Mathlib, основную библиотеку доказательств сообщества. По оценке Anthropic, это самое большое доказательство на Lean из когда-либо построенных, при этом текст, вероятно, длиннее необходимого.

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

Доказательство Уайлса 1995 года заняло 129 страниц

Ферма записал утверждение на полях «Арифметики» Диофанта около 1637 года: ни при каком n больше двух не найдётся натуральных a, b и c, для которых aⁿ + bⁿ = cⁿ. Первое верное доказательство Эндрю Уайлс опубликовал в мае 1995 года, на его проверку ушли месяцы. В 1908 году за верное доказательство назначили приз в 100 000 золотых марок, и только за первый год пришло 621 неверное решение.

В июне 1993 года Уайлс представил доказательство в трёх лекциях, но через два месяца проверки рецензент указал на критический пробел. Уайлс закрывал его год, сначала один, затем вместе с бывшим учеником Ричардом Тейлором. Идею формализовать доказательство высказал нидерландский информатик Ян Бергстра примерно десятилетием позже.

В 2024 году Кевин Баззард из Imperial College London запустил проект сообщества по формализации в Lean: только письменное описание начальной фазы занимает 86 страниц. Claude следовал упрощённой версии доказательства Уайлса в изложении Анри Дармона, Фреда Даймонда и Ричарда Тейлора, заимствуя фрагменты из проекта Imperial College London и проекта flt-regular.

Гранты на формализацию других теорем Anthropic и другие лаборатории расширили поддержку внешних исследователей, включая математиков: бесплатные и льготные подписки, исследовательские кредиты и гранты на крупные научные проекты, среди которых формализация других крупных теорем и развитие Lean и Mathlib. В Anthropic ожидают, что формализованное доказательство станет обычным приложением к текстам, написанным для читателей-людей. Полный текст доказательства выложен на GitHub вместе с письменным разбором.