AIREITERЗаголовок «Claude решил великую теорему Ферма» звучит эффектно, но здесь важно не пропустить одно слово: формализовал. Anthropic опубликовала артефакт для Lean, который, по заявлению компании, проверяет теорему от начала до конца. Однако математический маршрут в нём не новый: это известная цепочка Фрея—Серра—Рибе—Уайлса—Тейлора—Уайлса, а не самостоятельно найденное доказательство.
Сначала разделим два разных утверждения
В узком смысле ответ положительный: Anthropic выпустила публичный репозиторий с формализацией великой теоремы Ферма (FLT) на Lean 4, а также инструкциями по сборке и проверке. Но более широкое утверждение, будто Claude сам решил знаменитую задачу, неверно: математический прорыв десятилетия назад совершили Эндрю Уайлс и Ричард Тейлор.
FLT утверждает, что уравнение a^n + b^n = c^n не имеет решений в положительных целых числах при n > 2. Доказательство Уайлса опубликовали в 1995 году; результат Anthropic превращает уже известную математическую схему в проверяемый машиной артефакт. Исторический контекст изложен в анонсе проекта FLT от Lean Community.
Формальное доказательство в Lean отвечает не на тот же вопрос, что и неформальная математическая статья. Оно показывает, что точно закодированное утверждение следует из проверенных определений, зависимостей и аксиом в конкретном окружении. Но оно не доказывает, что ИИ изобрёл лежащую в основе математику, и не гарантирует, что названия теорем соответствуют их описаниям.
Что именно выпустила Anthropic
В исследовательской публикации от 4 сентября 2026 года Anthropic сообщает, что Claude за 11 дней создал первую полную сквозную формализацию FLT на Lean, проверенную компьютером. В публикации говорится примерно о 13 миллионах строк Lean, 30 300 доказанных формулировках теорем и 29 500 утверждениях, использованных в финальном доказательстве. Кроме того, система сгенерировала около 6 миллиардов выходных токенов.
Для работы использовалась платформа Prove2Me, которую Anthropic описывает как систему с ориентированным ациклическим графом формулировок теорем и координацией нескольких агентов. По словам компании, формализация опирается на упрощённое изложение уже известного доказательства, связанного с Фреем, Серром, Рибе, Уайлсом и Тейлором—Уайлсом.
Для проверки заявления публичный репозиторий на GitHub полезнее самого анонса. Его цель по умолчанию — FinalCheck.lean, а объявление теоремы выглядит так:
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ nВ репозитории прямо сказано, что это исследовательский артефакт, который не сопровождается и не принимает вкладов. Проект фиксирует Lean 4.33.1 и Mathlib v4.33.0, содержит файл PROOF-PATH.md, а также предоставляет HTML-версию графа теорем и определений, доступную для просмотра офлайн.
Финальная проверка в репозитории должна завершиться ошибкой, если доказательство использует добавленную аксиому, sorry, native_decide, unsafe или похожий обходной путь. Благодаря этому артефакт можно изучать самостоятельно, не полагаясь на скриншоты и пересказ авторов.
Как воспроизвести проверку
Надёжная проверка начинается с зафиксированного окружения репозитория, а не с попытки открыть отдельный файл .lean в другом проекте. В руководстве Lean Community по проверке объясняется почему: новые версии Lean выходят ежемесячно, Mathlib меняется часто, а обратная совместимость не гарантируется.
Сначала зафиксируйте окружение
В репозитории указано, что сборка рассчитана на Linux или macOS и требует elan, Git, Python, GNU coreutils и сетевое подключение, чтобы Lake мог загрузить и собрать зафиксированные зависимости. Авторы сообщают примерно о 67 ГБ в каталоге .lake и ещё примерно 220 ГБ сгенерированных C-файлов, которые впоследствии можно удалить.
По данным репозитория, на одну параллельную задачу требуется около 5 ГБ памяти, а отдельным модулям нужно до 36 ГБ. При 96 задачах собственная сборка проекта заняла 5 часов 32 минуты и достигла пикового потребления памяти в 153 ГБ. Это цифры, приведённые авторами репозитория, а не измерения из этой статьи; воспринимайте их как ориентир для планирования, а не как гарантированное время работы.
Выберите подходящий уровень проверки
- Только изучить код: откройте
FinalCheck.lean,PROOF-PATH.mdиATTRIBUTION.md, не выполняя сборку. - Полная сборка Lean: используйте зафиксированный toolchain и запустите
lake build. - Независимое воспроизведение: после успешной сборки и экспорта запустите скрипты comparator и nanoda.
Для свежего клона репозиторий предлагает примерно такую последовательность:
git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt
# Уменьшите число, если ваша машина не может выделить необходимый объём памяти.
LEAN_NUM_THREADS=96 lake build
# Сверьте результат с формулировкой задачи, использующей только Mathlib.
verification/comparator/run.sh
# Запускайте после проверки comparator.
verification/nanoda/run.shУ каждого этапа своя задача:
| Этап | Данные, указанные репозиторием | Назначение |
|---|---|---|
lake build | 60 475 модулей; 5 часов 32 минуты при 96 задачах в указанном запуске | Собирает проект из исходников и позволяет ядру Lean проверить объявления, вошедшие в сборку |
| Comparator | 14 часов 46 минут в указанном запуске; пиковое потребление памяти — 230 ГБ | Проверяет, что открытая теорема и используемые константы соответствуют целевой формулировке задачи в Mathlib |
nanoda | Около 30 минут при 16 потоках после экспорта | Воспроизводит проверку экспортированного окружения с помощью независимо написанного ядра на Rust |
Comparator не заменяет чтение формулировки теоремы. Он помогает исключить ситуацию, когда проект доказывает ослабленное или слегка изменённое утверждение. Файл PROOF-PATH.md связывает математические этапы с объявлениями Lean, а сгенерированные HTML-страницы позволяют изучать зависимости без запуска веб-приложения.
В репозитории также указаны дополнительные затраты на вторичные проверки: запись экспорта размером 37,8 ГБ может потребовать около 90 ГБ памяти, а процесс nanoda — примерно 40 ГБ во время проверки.
Что подтверждают эти данные — и чего они не подтверждают
| Уровень проверки | Что он устанавливает | Чего он не устанавливает |
|---|---|---|
| Сборка ядром Lean | Переданные доказательные термы типизируются в зафиксированном окружении Lean | Что Claude открыл саму математику или что неформальное объяснение соответствует каждому названию теоремы |
FinalCheck.lean и проверка аксиом | Финальная теорема репозитория проверяется относительно заявленного списка аксиом и отбрасывает несколько перечисленных обходных путей | Что это именно историческая формулировка FLT, если не изучить саму формулировку |
Вывод #print axioms | При успешной ожидаемой проверке зависимости включают стандартные аксиомы Lean — propext, Classical.choice и Quot.sound, а не скрытую пользовательскую аксиому | Что вся цепочка поставки программного обеспечения прошла независимую проверку |
| Comparator | Доказанный результат и используемые константы совпадают с применяемой репозиторием задачей только на Mathlib | Что все текстовые описания проекта понятны или пригодны для обучения |
| Повторная проверка nanoda | Экспортированное окружение принято второй реализацией ядра Lean на Rust | Что экспорт, скрипты или операционная система полностью защищены от любых возможных ошибок |
PROOF-PATH.md и атрибуция | Дают человеку маршрут для проверки соответствия математических шагов и исходных материалов | Что автоматически сгенерированные названия теорем точно описывают их формулировки без участия человека |
В чек-листе Lean Community «Did you prove it?» сформулировано главное правило: компиляция проверяет закодированное утверждение, но не то, соответствует ли название теоремы предполагаемому неформальному смыслу. В случае этого артефакта comparator и его опора на Mathlib снижают такой риск, однако всё равно необходимо прочитать объявление теоремы и маршрут доказательства.
Что показывает артефакт — и чего он не показывает
Система создала формально проверенный артефакт Lean необычного масштаба. Но это не демонстрация нового пути к FLT, нового элементарного доказательства или самостоятельного математического открытия Claude.
Anthropic утверждает, что доказательство следует упрощённой версии маршрута Уайлса. Репозиторий также указывает на уже существующие наработки: файл ATTRIBUTION.md отмечает 106 файлов с материалами проекта FLT Imperial College London или flt-regular, а также использование Mathlib. Эта история происхождения важна для точного понимания того, на чём построен выпущенный артефакт.
В рамках запуска проект доказал 30 300 формулировок теорем, около 29 500 из которых вошли в финальное доказательство; при этом репозиторий описывает 29 511 страниц теорем. Это формальные объявления и зависимости, а не 29 511 новых математических результатов. Формальное доказательство разворачивает неявные шаги, типы, приведения, определения и библиотечные зависимости, которые в человеческом доказательстве можно оставить на уровне экспертного понимания.
В репозитории отдельно сказано, что исходники создавались прежде всего для проверки, а не для чтения: названия генерируются машиной, обозначения вроде P2M являются метками конвейера, и главным считается содержание утверждения, а не его имя. Поэтому маршрут доказательства и comparator здесь не менее важны, чем заголовочная теорема.
Предыдущие работы над Lean не стоит смешивать с заявлением 2026 года. В статье 2023 года о великой теореме Ферма для регулярных простых сообщалось о полной формализации без sorry случая I теоремы Куммера для регулярных простых; при этом авторы отмечали, что случай II и лемма Куммера оставались значительным объёмом работы. В редакции 2025 года формализация для регулярных простых уже описывалась как полное доказательство этого более узкого случая.
| Работа | Охват | Практическая роль |
|---|---|---|
flt-regular research | Результаты для регулярных простых и базовая инфраструктура алгебраической теории чисел | Предыдущий формальный строительный блок и исходные материалы |
| Imperial FLT project | Долгосрочная переиспользуемая формализация современной теории чисел вокруг FLT | Библиотечная и командная инфраструктура |
| Anthropic repository | Заявленная сквозная теорема FLT на Lean 4 со сборкой и повторными проверками | Крупный исследовательский артефакт, ориентированный на проверенный результат, а не на долгосрочное сопровождение |
Проект Imperial/Lean FLT описывает формализацию современной теории чисел как более широкую инфраструктурную работу, а не просто перевод одной теоремы. Релиз Anthropic разумнее воспринимать как дополнительное свидетельство возможностей скоординированных ИИ-агентов внутри существующей формальной экосистемы, а не как доказательство того, что цели предыдущего проекта больше не важны.
Чему здесь можно доверять
| Если вы хотите узнать… | Корректный ответ… | Что делать дальше |
|---|---|---|
| Действительно ли Anthropic выпустила рабочий артефакт | Да; есть официальный анонс и публичный репозиторий с зафиксированным окружением | Изучить вместе исследовательскую публикацию и репозиторий |
| Является ли закодированная теорема FLT | В репозитории есть конкретное объявление теоремы, comparator и маршрут доказательства | Проверить FinalCheck.lean, comparator и PROOF-PATH.md |
| Собирается ли код без ошибок | Репозиторий описывает сборку с нуля и приводит собственный результат | Повторить сборку с Lean 4.33.1 и Mathlib v4.33.0, если у вас есть подходящее оборудование |
| Изобрёл ли Claude новое доказательство | Подтверждений этому нет; использованный маршрут опирается на известную математику Уайлса и Тейлора—Уайлса | Называть результат формализацией или proof engineering с помощью ИИ |
| Легко ли сопровождать этот артефакт | Нет; репозиторий прямо называет себя неподдерживаемым, а код сгенерирован машиной | Воспринимать его как исследовательский артефакт, а не готовую библиотеку для подключения к Mathlib |
| Доказывает ли это общую математическую автономность | Нет; результат показывает возможности на чётко заданной цели формализации с существенной вспомогательной инфраструктурой | Разделять способность к формальной проверке и открытие теорем в свободной постановке |
Если вам достаточно самой новости, официальный релиз и репозиторий подтверждают существование проекта. Если нужен аудит, воспроизведите сборку в зафиксированном окружении и изучите формулировку теоремы. А при оценке исследований в области ИИ учитывайте всю систему: оркестрацию агентов, существующие библиотеки, предыдущие формализации и вычислительные ресурсы.
FAQ
Открыл ли Claude новое доказательство великой теоремы Ферма?
Нет. Артефакт Anthropic формализует известный маршрут доказательства, связанный с Фреем, Серром, Рибе, Уайлсом и Тейлором—Уайлсом. Достижение здесь — масштаб и скорость создания проверяемого машиной артефакта Lean, а не новое математическое решение.
Доказывает ли успешная сборка Lean неформальную теорему?
Она доказывает, что закодированное утверждение следует из проверенных зависимостей в данном окружении Lean. Но всё равно нужно убедиться, что утверждение и его определения действительно соответствуют той неформальной теореме, о которой вы говорите.
Использует ли репозиторий sorry или дополнительные аксиомы?
В репозитории сказано, что финальная проверка отбрасывает sorry, добавленные аксиомы, native_decide, unsafe и несколько похожих обходных путей. Ожидаемый список аксиом состоит из трёх стандартных аксиом Lean: propext, Classical.choice и Quot.sound. Однако проверку лучше воспроизвести самостоятельно, а не ограничиваться анонсом.
Можно ли воспроизвести результат на обычном ноутбуке?
Возможно, вам удастся изучить репозиторий и частично его собрать, но полная проверка — совсем не лёгкая задача для обычного компьютера. Репозиторий сообщает о пиковом потреблении 153 ГБ памяти при сборке, до 230 ГБ для comparator и значительных требованиях к диску, поэтому аппаратные ресурсы здесь становятся одним из главных ограничений.
Чтобы корректно проверить заявление, начните с зафиксированного артефакта на GitHub, прочитайте объявление теоремы до того, как поверите заголовку, и описывайте результат как крупную формализацию известной математики с помощью ИИ.