Claude формализовал Великую теорему Ферма: 13 миллионов строк Lean за 11 дней

От знаменитого доказательства — к проверяемому коду

Anthropic сообщила о первом полном компьютерно проверенном доказательстве Великой теоремы Ферма. Claude за 11 дней в значительной степени автономной работы записал доказательство на языке Lean, создав 13 миллионов строк кода и доказав 30 300 промежуточных теорем; 29 500 из них вошли в финальную цепочку. Компания открыла получившийся проект на GitHub, поэтому речь идёт не только о демонстрации в закрытой системе, но и о доступном для проверки формальном артефакте.

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

Почему формализация сложнее обычной переписи

Человеческое математическое изложение неизбежно пропускает очевидные для специалиста переходы и ссылается на большой корпус ранее доказанных результатов. Proof assistant не принимает такие сокращения: каждый используемый объект должен быть определён, а каждый логический переход — выведен из доступных аксиом и уже проверенных теорем. Поэтому перевод 129-страничного доказательства Уайлса, опубликованного в 1995 году, нельзя свести к механической замене формул на синтаксис Lean.

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

Десятки агентов работали по графу теорем

Первые попытки Anthropic не были успешными. Агенты быстро теряли представление о состоянии большого проекта и переставали эффективно координироваться; следы этих неудачных ветвей составили около 7% содержательных строк финального доказательства. Перелом произошёл после перехода на Prove2Me — открытую платформу для совместной формализации, созданную Тяньи Пэном и его коллегами из Columbia University.

Prove2Me представляла работу как ориентированный ациклический граф утверждений. Агенты выбирали ещё не закрытые узлы, доказывали промежуточные результаты и переиспользовали их выше по графу; раздельное хранение формулировок и доказательств ускоряло компиляцию, а естественно-языковые описания облегчали поиск. Поверх этой структуры Anthropic использовала multi-agent harness на базе Claude Code. Человеческое участие, по описанию компании, ограничивалось редкими высокоуровневыми указаниями о приоритетах.

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

Финальное доказательство было принято Lean и использует только три стандартные аксиомы языка. Дополнительный comparator подтвердил совпадение формулировки корневой теоремы с формулировкой Великой теоремы Ферма в Mathlib. Это существенная защита от формального трюка, при котором система безошибочно доказывает более слабое или иначе сформулированное утверждение.

Кевин Баззард изучил результат и назвал его доказательством без предположений сверх математических аксиом, отметив многоуровневую структуру артефакта. Однако компьютерная проверка отвечает на строго очерченный вопрос: следует ли вывод из формализованных определений, аксиом и зависимостей. Она не делает 13 миллионов строк автоматически удобными для чтения, не заменяет содержательное объяснение для математиков и не устраняет необходимость аудита инфраструктуры и выбранной формализации. Anthropic сама подчёркивает, что формальный артефакт не должен вытеснять понятное человеку изложение.

Цена результата — шесть миллиардов выходных токенов

Кампания потребила около шести миллиардов output tokens внутренней исследовательской модели общего назначения, которую Anthropic сравнивает по возможностям с Claude Fable 5.1. Объём итогового кода более чем в пять раз превышает Mathlib — основную библиотеку Lean, на которую проект при этом опирается. Компания признаёт, что доказательство, вероятно, намного длиннее необходимого: крупный масштаб здесь показывает достижимость автоматической формализации, но ещё не её компактность или экономичность.

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

Главный эффект — масштабирование проверки математики

Практическая ценность работы выходит за пределы одной знаменитой теоремы. Проверка нового сложного доказательства людьми может занимать месяцы или годы, а рост AI-сгенерированной математики способен сделать ручное рецензирование узким местом. Если формализацию удастся регулярно выпускать вместе с человеческим текстом, proof assistant сможет автоматически обнаруживать разрывы в логической цепочке и снижать нагрузку на рецензентов.

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