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

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

Великая теорема Ферма — показательный пример. Ферма записал её формулировку на полях книги с таинственной припиской:

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

Более 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 — главной библиотеки математических доказательств сообщества, на которой строится эта теорема.

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

"THE FLT root reads Proved on the site. Historic moment (modulo re-check)."

"!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign's goal: e2e FLT on prove2me."

"🏁🏁🏁The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign."

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

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

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

  1. Поддерживая направленный ациклический граф (DAG) утверждений теорем, который агенты использовали, чтобы решить, какие доказательства они должны попытаться сделать дальше. Это было особенно полезно для снижения деградации памяти и позволило нескольким агентам работать параллельно.
  2. Ускоряя компиляцию Lean и минимизируя потребление ресурсов путём разделения утверждений теорем и доказательств на разные файлы, с независимо поддерживаемыми связями между ними.
  3. Включая поиск и повторное использование путём сохранения естественноязычного описания каждого утверждения теоремы, что привело к более простому пути доказательства.
DAG, показывающий Claude, формализующий под-теоремы по пути к FLT
Ключевые вехи из плана Prove2Me, которые Claude использовал для формализации Великой теоремы Ферма. Три цветных раздела соответствуют трём основным под-теоремам, которые Claude пришлось доказывать на пути к своей конечной цели. Этот граф тесно следует оригинальному доказательству Уайлса.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Рекомендуемая научно-популярная литература

  • The Proof in the Code — недавняя книга об истории помощника доказательства Lean и формализации математики.
  • Документальный фильм BBC 1996 года «Великая теорема Ферма» содержит интервью с Уайлсом и другими математиками, участвовавшими в доказательстве, и тепло вспоминается некоторыми авторами этого поста.
  • Для тех, кто имеет математическую подготовку, техническую историю propositions-as-types (базовой дисциплины помощников доказательств таких как Lean, Rocq и Agda) можно найти в Propositions as Types Филипа Вэдлера.
  • Chen, S., Marwaha, K., Lu, X., Yuen, H., & Peng, T. (2026). Prove2Me: An open collaborative platform for scaling math formalization. arXiv. https://doi.org/10.48550/arXiv.2608.28433
  • Automating Math, Адам Марблстоун в Asterisk Magazine.

Примечания

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