Как Claude, по данным Anthropic, за 11 дней оформил доказательство теоремы Ферма в Lean

Anthropic сообщила, что Claude создал первую полную сквозную формализацию последней теоремы Ферма (FLT), которую может механически проверить Lean. Главное уточнение: Claude не открыл новое доказательство теоремы. Он перевёл уже известный современный путь доказательства в гигантский формальный объект, пригодный для машинной проверки. По данным компании, работа заняла около 11 дней и дала примерно 13 миллионов строк Lean-кода. 215

Что именно было доказано

Последняя теорема Ферма утверждает: при натуральном показателе степени (n\geq3) у уравнения (a^n+b^n=c^n) нет нетривиальных решений в положительных целых числах.

В библиотеке Mathlib, на которой строятся многие проекты для Lean, утверждение записано в эквивалентной форме: если такое равенство выполнено для натуральных чисел, то хотя бы одно из (a), (b) или (c) равно нулю. 31

Проект следовал изложению стратегии Уайлса и Тейлора—Уайлса в версии Дармона—Даймонда—Тейлора, а не искал новый математический маршрут. Это существенно: при формализации нужно записать не только центральную идею доказательства, но и все определения, предпосылки, вспомогательные результаты и переходы, которые в обычной статье могут быть опущены словами «стандартным рассуждением». Проект Imperial College по формализации FLT также описывает свой путь как современный вариант доказательства Уайлса/Тейлора—Уайлса. 511

Почему получилось 13 миллионов строк

Ассистент доказательств не принимает фразу вроде «отсюда немедленно следует». Каждый вывод должен быть выражен так, чтобы система могла проверить его типы и логическую корректность; каждый результат должен опираться на уже формализованные зависимости.

Anthropic сообщает примерно о 30 300 машинно проверенных теоремах, созданных в ходе проекта; около 29 500 из них входят в итоговую замкнутую цепочку зависимостей доказательства. Разработка затрагивает алгебру, геометрию, гармонический анализ и теорию чисел. 215

Поэтому формулировку «за 11 дней» нельзя понимать как замену всей интеллектуальной истории теоремы Ферма одиннадцатью днями работы. Компания также оценивает объём генерации примерно в шесть миллиардов токенов. В это вошли многочисленные варианты доказательств, проверки Lean, исправления ошибок и инженерная работа по организации долгого процесса формализации. 5

Как много агентов не потеряли нить рассуждения

Результат, согласно описанию Anthropic, зависел не только от способности одной модели удерживать огромный текст в контексте. Ранние попытки продвигались вперёд, но испытывали трудности с общей памятью о состоянии проекта. Успешный запуск использовал оболочку на базе Prove2Me — платформы для совместной формализации математики. 529

Основой организации стал ориентированный граф зависимостей:

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

Prove2Me называет такие проекты «миссиями» формализации, в которые агенты вносят повторно используемые формальные доказательства. 29 По сути, граф превращает одну хрупкую сверхдлинную задачу в множество небольших проверяемых подзадач и хранит рабочую память проекта вне отдельного запуска модели.

Что в данном случае означает «проверено компьютером»

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

Это существенно сильнее, чем правдоподобный текст доказательства, сгенерированный ИИ. Ядро Lean проверяет, следует ли каждый закодированный шаг из логических правил системы, аксиом и импортированных зависимостей. По данным Anthropic, также было подтверждено, что конечное утверждение совпадает с принятой в Mathlib формулировкой FermatLastTheorem. 531

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

Почему Кевин Баззард назвал результат выдающимся

По сообщению Anthropic, математик Кевин Баззард охарактеризовал работу как «выдающееся достижение автоформализации». 21 Значение здесь не в том, что агенты решили отдельные упражнения Lean, а в заявленной способности собрать многоуровневую, повторно используемую формальную разработку масштаба, на который раньше ожидались годы координированной работы людей.

Если подобные результаты окажутся воспроизводимыми и менее затратными, формализация может быть полезна математике в нескольких отношениях:

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

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

Как корректно понимать заявление Anthropic

Формализация FLT — значимый ориентир для ИИ-помощи в формальной математике именно потому, что цель была уже доказана людьми, а итоговый артефакт предполагается доступным для независимой проверки. Представлять это как новое решение последней теоремы Ферма со стороны Claude было бы неверно.

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

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