Формализация Великой теоремы Ферма в Lean

Полный перевод исследования Anthropic на русский. Оригинал — по ссылке.

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

Около 1637 года Пьер де Ферма записал на полях своего экземпляра «Арифметики» Диофанта утверждение, которому предстояло стать одной из самых известных математических гипотез всех времён: не существует положительных целых чисел a, b, c, удовлетворяющих aⁿ + bⁿ = cⁿ ни для какого n > 2. Великая теорема Ферма (FLT), как стала называться эта гипотеза, оказалась невероятно трудной для доказательства. Первое доказательство, представленное сэром Эндрю Уайлсом в 1995 году, занимало 129 страниц и потребовало месяцев кропотливой работы для проверки.

Десять лет спустя нидерландский специалист по информатике Ян Бергстра предложил «формализовать» доказательство Уайлса: преобразовать математические рассуждения в форму, которую компьютеры могут проверять автоматически. С тех пор математики разрабатывают методы, необходимые для кодирования столь сложного доказательства, включая многолетнюю коллективную инициативу, начатую в 2024 году Кевином Баззардом из Имперского колледжа Лондона для завершения формализации с использованием системы помощи в доказательствах Lean.

Недавно Тяньи Пэн, исследователь Anthropic, чья группа в Колумбийском университете создаёт инструменты для формализации с помощью искусственного интеллекта, решил проверить, сможет ли Claude добиться прогресса в формализации ВТФ.1 Результат превзошёл его ожидания. За 11 дней, работая в значительной степени автономно, Claude создал первое сквозное, проверенное компьютером доказательство ВТФ. Попутно он написал 13 миллионов строк Lean и доказал 29 500 промежуточных теорем.

Мы поделились полученным доказательством с Кевином Баззардом, который сказал:

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

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

Задача проверки математических доказательств

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

Последняя теорема Ферма — наглядный пример.2 Ферма записал формулировку теоремы на полях книги, сопроводив её интригующей заметкой:

Я открыл поистине чудесное доказательство этого, но эти поля слишком узки, чтобы его вместить.

Более 350 лет поколения математиков искали доказательство ПТФ — чудесное или какое-либо иное. В 1908 году была объявлена премия в размере 100 000 немецких золотых марок — что соответствует 1–2 миллионам долларов сегодня — для любого, кто сможет представить правильное доказательство, и только за первый год было представлено 621 неверная попытка.

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

Уайлс опубликовал первое верное доказательство ВТФ в мае 1995 года; оно опиралось на современные математические методы, которые значительно превосходили всё, что могло быть известно Ферма в 1637 году. Поскольку элементарное доказательство не было найдено после столетий попыток, математическое сообщество теперь считает, что собственное первоначальное «удивительное доказательство» Ферма было неверным.

Формализация последней теоремы Ферма

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

Для ВТФ предполагалось, что процесс формализации займёт годы. Только план, который математическое сообщество использовало для описания начального этапа проекта, занимает 86 страниц.

Claude завершил доказательство за 11 дней, попутно создав проверяемые компьютером доказательства 30 300 теорем (использовав 29 500 в окончательном доказательстве). Десятки агентов Claude совместно определяли понятия, доказывали промежуточные теоремы и использовали эти теоремы для доказательства всё более сложных утверждений. При 13 миллионах строк кода Lean доказательство Claude более чем в 5 раз превосходит по размеру Mathlib, основную библиотеку математических доказательств сообщества, на которой строится эта теорема.3

Смотреть видео из оригинала

Доказательство Claude следует упрощённой версии доказательства Уайлса, изложенной Дармоном, Даймондом и Тейлором. Математический вклад людей ограничивался редкими высокоуровневыми указаниями Тяньи: «Якобиан как схема кажется высокоприоритетным», «добейтесь скорого завершения [теоремы] Мазура». Вы можете найти фрагменты рассуждений Claude здесь.

Фрагменты рассуждений Claude в момент, когда он осознаёт, чего только что достиг.

Ряд первоначальных попыток Claude потерпел неудачу: хотя агенты добились некоторого раннего успеха, они быстро потеряли представление о состоянии проекта и перестали эффективно сотрудничать. Их неудачные усилия составили около 7% строк без шаблонного кода в окончательном доказательстве.

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

1. Поддерживая ориентированный ациклический граф (DAG) утверждений теорем, который агенты использовали, чтобы решать, какие доказательства им следует пытаться построить дальше. Это было особенно полезно для смягчения ухудшения памяти и позволило нескольким агентам работать параллельно.
2. Ускоряя компиляцию Lean и сводя к минимуму потребление ресурсов за счёт разделения утверждений теорем и доказательств по разным файлам, при этом связи между ними поддерживались независимо.
3. Обеспечивая поиск и повторное использование путём поддержания описания каждого утверждения теоремы на естественном языке, что привело к более простому пути доказательства.

С помощью Prove2Me и мультиагентной системы на основе Claude Code команда агентов завершила доказательство чуть менее чем за две недели, использовав около шести миллиардов выходных токенов внутренней исследовательской модели общего назначения, примерно сопоставимой с Claude Fable 5.1. Готовое доказательство было проверено Lean; оно использует лишь три стандартные аксиомы Lean, а компаратор подтвердил, что формулировка теоремы совпадает с собственной формулировкой последней теоремы Ферма в Mathlib.

Снижение нагрузки формальной верификации

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

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

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

Написание кода на Lean, по-видимому, также помогает Claude доказывать новые результаты. Многие из наших недавних результатов, автором которых является Claude, формализовались параллельно с их доказательствами, и Claude, по-видимому, использует эти частичные доказательства для независимой проверки своих гипотез — подобно тому, как он пишет численные симуляции, чтобы проверить, движется ли он в верном направлении.

Формализация последней теоремы Ферма была проектом, требовавшим большого количества токенов, но также является крупнейшим доказательством Lean из когда-либо созданных. Исследователи Anthropic провели небольшой эксперимент, используя три личных тарифа Claude Max для формализации применений метода окружностей Харди — Литтлвуда. Сотрудничая исключительно через Prove2Me, агенты совместно завершили формализацию теоремы Виноградова о трёх простых числах всего за три дня. Мы считаем, что при наличии правильной структуры совместная формализация крупных результатов с использованием потребительских подписок на искусственный интеллект достижима.

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

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

Благодарности

Наша работа по формализации — небольшая часть долгой истории теоремы Ферма и развития формальной математики. Первое полное доказательство Эндрю Уайлса совместно с Ричардом Тейлором стало кульминацией более чем трёхсот лет математики, объединив идеи Герхарда Фрея, Жан-Пьера Серра, Кена Рибета, Барри Мазура, Роберта Лэнглендса, Джерролда Таннелла, Ютаки Таниямы, Горо Симуры и Андре Вейля, среди прочих. Доказательство Claude следует изложению Анри Дармона, Фреда Даймонда и Ричарда Тейлора.

Наше доказательство использует части проекта Imperial College London FLT, возглавляемого Кевином Баззардом, и проекта flt-regular. Lean и Mathlib — оба самостоятельные труды, созданные с любовью, и в них внесли вклад сотни математиков, многие из которых работают с Lean FRO. Мы благодарим Кевина Баззарда за проверку доказательства и за его комментарии.

Узнать больше

Полное доказательство доступно на GitHub вместе с письменным пошаговым разбором доказательства.

Рекомендуемое ознакомительное чтение

• Доказательство в коде — недавно вышедшая книга об истории программы для доказательства теорем Lean и формализации математики.
• Документальный фильм BBC 1996 года «Последняя теорема Ферма» содержит интервью с Уайлсом и другими математиками, участвовавшими в доказательстве, и некоторые авторы этой публикации с теплотой его вспоминают.
• Для тех, кто имеет математическую подготовку, техническую историю соответствия между утверждениями и типами — лежащей в основе дисциплины ассистентов доказательств, таких как Lean, Rocq и Agda, — можно найти в статье Филипа Уодлера Утверждения как типы.
• Чен, С., Марваха, К., Лу, С., Юэн, Х. и Пэн, Т. (2026). Prove2Me: открытая совместная платформа для масштабирования формализации математики. arXiv. https:\/\/doi.org\/10.48550\/arXiv.2608.28433
• Автоматизация математики, Адам Марблстоун, в журнале Asterisk Magazine.

Сноски

1. Во время обучения в бакалавриате научный руководитель Пэна хотел включить результаты из дипломной работы Пэна в статью для Nature. Он спросил Пэна, уверен ли тот, что доказательство верно. Пэн честно ответил: «Я уверен на 99 %, но трудно быть на 100 % уверенным в доказательстве такой длины». Пэн упустил возможность опубликовать свою работу в Nature.
2. Существует множество других историй о том, как математическое сообщество сталкивалось с трудностями при проверке. Среди наиболее известных — доказательство гипотезы Кеплера, представленное Томасом Хейлзом в 1998 году: оно находилось на рассмотрении четыре года, прежде чем комиссия из 12 рецензентов остановилась на формулировке «уверены на 99 %» (впоследствии Хейлз возглавил проект из двадцати человек, Flyspeck, в рамках которого доказательство было формализовано). Сообществу потребовалось примерно четыре года и три изложения объёмом по 300 страниц, чтобы принять доказательство гипотезы Пуанкаре, представленное Григорием Перельманом в 2002 году. Доказательство слабой гипотезы Гольдбаха, представленное Харальдом Хельфготтом в 2013 году, всё ещё находится на рассмотрении. Иногда результаты, которые впоследствии оказываются ошибочными, принимаются годами, а другие математики строят свои теории на этих ошибочных основаниях.
3. Отчасти это связано с тем, что Mathlib лаконична и тщательно проверена, тогда как наше доказательство, вероятно, гораздо длиннее, чем необходимо.