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

Anthropic 4 сентября объявила, что Claude создал первое полное доказательство последней теоремы Ферма, проверенное компьютером. По данным компании, десятки агентов Claude работали в значительной степени автономно в течение 11 дней, сгенерировали примерно 13 million строк кода Lean и доказали 30,300 теорем, из которых около 29,500 вошли в окончательное доказательство.

В общепринятом математическом смысле это не новое доказательство последней теоремы Ферма. Эндрю Уайлс и Ричард Тейлор завершили принятое человеческое доказательство в 1990-х годах. Вместо этого Claude перевёл уже известный путь, изложенный в литературе, на формальный язык, логические шаги которого может проверить компьютер.

Это различие существенно. Результат практически не добавляет новых знаний о том, верна ли последняя теорема Ферма, но демонстрирует, что система ИИ способна формализовать массив передовой математики, на который, как прежде ожидалось, потребуются годы работы специалистов. Кевин Баззард, математик из Imperial College London, возглавляющий отдельный проект формализации, скомпилировал код Anthropic и выполнил проверки компаратором. По его словам, доказательство проходит проверку.

1. Что Claude формально доказал

Последняя теорема Ферма утверждает, что не существует положительных целых чисел \(a\), \(b\) и \(c\), удовлетворяющих \(a^n+b^n=c^n\), когда целый показатель степени \(n\) не меньше трёх. Формулировка элементарна, однако известные доказательства опираются на сложные результаты об эллиптических кривых, модулярных формах, представлениях Галуа, теории деформаций, алгебраической геометрии и теории чисел.

Репозиторий Anthropic выражает окончательную теорему непосредственно над натуральными числами Lean. В её формулировке берутся положительные натуральные числа \(a\), \(b\) и \(c\), а также \(n \geq 3\), и доказывается, что равенство не может выполняться. Отдельная финальная проверка выводит существующую в Mathlib формулировку последней теоремы Ферма из этой теоремы.

Аргумент следует работам Фрея, Серра, Рибе, Уайлса и Тейлора—Уайлса, в частности изложению 1995 года Анри Дармона, Фреда Даймонда и Ричарда Тейлора. Он использует связь между гипотетическим решением уравнения Ферма и эллиптической кривой Фрея, затем применяет результаты о модулярности и понижении уровня, чтобы получить противоречие.

Баззард отметил важную деталь конструкции. Путь Anthropic, основанный на Уайлсе, охватывает простые показатели \(p \geq 17\). Полный результат включает ранее формализованную работу о регулярных простых числах, закрывающую остальные случаи. Тем не менее полученная теорема Lean охватывает каждый показатель из натуральных чисел не меньше трёх.

Артефакт также зависит от значительного объёма более ранней человеческой работы. Anthropic сообщает, что адаптировала материалы из проекта Imperial College FLT, проекта flt-regular и Mathlib. В файле атрибуции указано 106 файлов, содержащих материалы из первых двух проектов, и 23 файла, воспроизводящих текст Mathlib. Следовательно, достижение представляет собой интеграцию и расширение существующей формальной экосистемы под руководством ИИ, а не 13 million строк, созданных независимо от предшествующей формальной математики.

2. Как многоагентная система справилась с доказательством

Изначально Anthropic обнаружила, что агенты Claude могли доказывать отдельные результаты, но теряли представление о проекте в целом. Агенты дублировали работу, неэффективно повторно использовали уже доказанные теоремы и переставали координироваться по мере роста доказательства. На неудачные попытки всё ещё приходится около 7% окончательного нешаблонного кода.

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

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

Многоагентный контур на базе Claude Code координировал десятки агентов во время 11-дневного запуска. Сообщается, что человеческий математический вклад ограничивался отдельными приоритетами высокого уровня — например, направлением агентов к якобианам или просьбой завершить теорему, связанную с работой Мазура. Внутренний журнал зафиксировал корневую теорему как доказанную 18 августа.

Anthropic сообщает, что запуск потребил примерно шесть billion выходных токенов. Использовалась внутренняя исследовательская модель общего назначения, описанная лишь как приблизительно сопоставимая с Claude Fable 5.1, поэтому точная модель и конфигурация публично недоступны. Компания не раскрыла денежную стоимость или вычислительную стоимость проекта.

Готовая разработка содержит 29,511 страниц теорем и 1,450 модулей определений в доступной для просмотра документации. Anthropic насчитывает 30,300 проверяемых компьютером теорем во всём запуске, включая результаты, которые в итоге не понадобились в окончательном пути зависимостей.

3. Как было проверено доказательство

Формальное доказательство ценно только тогда, когда контролируются формулировка теоремы, допустимые предположения и процесс верификации. Репозиторий Anthropic фиксирует проект на Lean 4.33.1 и Mathlib 4.33.0 и включает несколько уровней проверки.

Во-первых, проект был собран с нуля. Его 60,475 модулей были проверены ядром Lean. Окончательная теорема зависит ровно от трёх стандартных аксиом Lean: экстенсиональности высказываний, классического выбора и корректности факторизации. Распределённые модули доказательства не содержат незавершённых заполнителей sorry, вновь объявленных аксиом, небезопасного кода, обходов через нативные решения или внешних реализаций.

Во-вторых, проект использовал Lean Comparator для сравнения доказанной теоремы с отдельно предоставленной проверочной формулировкой, основанной только на Mathlib. Эта проверка призвана установить, что решение доказывает то же самое утверждение, не использует неодобренных аксиом и принимается ядром. Компаратор вынес вердикт о принятии.

В-третьих, независимая реализация ядра Lean под названием nanoda проверила экспортированную версию окружения и без ошибок приняла 1,052,234 деклараций. Anthropic внесла в nanoda четыре патча: один для вывода прогресса и три для ускорения поиска дефиниционального равенства. В репозитории сказано, что ни один из них не изменяет и не ослабляет правило типизации.

Баззард предоставил наиболее релевантное внешнее подтверждение. Он скомпилировал код на машине с 96 ядрами и самостоятельно запустил компаратор. Он описал репозиторий как содержащий более 13.4 million строк и сказал, что его компиляция заняла почти в 20 раз больше времени, чем компиляция математической библиотеки Lean.

Воспроизвести все проверки возможно, но это требует значительных аппаратных ресурсов. Документированная сборка Anthropic заняла 5 hours and 32 minutes при 96 параллельных задачах, достигла пика в 153 GB памяти и использовала примерно 67 GB для сборки Lean плюс до 220 GB удаляемых сгенерированных C-файлов. Запуск компаратора занял 14 hours and 46 minutes и достиг пика в 230 GB. Экспорт окружения для второго ядра создал файл размером 37.8 GB.

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

4. Что изменилось для математики с ИИ-ассистированием

До этого результата последняя теорема Ферма оставалась последним пунктом в многолетнем списке Фрика Вейдейка из 100 заметных задач по формализации теорем. Проект Imperial College начался в 2024 году при финансировании на пять years и первоначально ставил целью свести теорему к результатам, известным к концу 1980-х годов. В материалах проекта отмечалось, что полная формализация потребует перевода тысяч страниц неформальной математики.

Вместо этого доказательство Anthropic доводит работу до окончательной теоремы от начала до конца. Баззард подчеркнул, что это не делает его проект избыточным: инициатива Imperial разрабатывает многократно используемые, читаемые человеком дополнения к Mathlib и следует более современному доказательству. Anthropic называет свой репозиторий исследовательским артефактом, который не будет поддерживаться и не принимает вклад.

Таким образом, практический прогресс заключается в пропускной способности. Агенты Claude собрали формальные определения и доказательства в алгебре, гармоническом анализе, геометрии и теории чисел в масштабе, который более чем в пять раз превысил число строк Mathlib. Результат показывает, что агентная система на основе графа может сохранять зависимости и координировать работу над формализацией, слишком большой для контекста одной модели.

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

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

Частые вопросы

Открыл ли Claude новое доказательство последней теоремы Ферма?

Нет. Он формализовал уже известный путь в литературе Фрея–Серра–Рибе–Уайлса–Тейлора—Уайлса, чтобы Lean мог проверить каждый логический шаг.

Был ли результат независимо проверен?

Кевин Баззард скомпилировал публичный код и запустил Lean Comparator, сообщив, что он проходит проверку. В репозитории также зафиксированы успешные проверки Lean и независимым ядром nanoda.

Какая модель Claude создала доказательство?

Anthropic не назвала точную публичную модель. Компания описывает внутреннюю исследовательскую модель общего назначения как примерно сопоставимую с Claude Fable 5.1.

Могут ли исследователи воспроизвести верификацию?

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

Репозиторий на 13 million строк полностью состоит из новой математики, написанной ИИ?

Нет. Агенты ИИ сгенерировали и интегрировали большую часть разработки, опираясь при этом на Mathlib и более раннюю работу по формализации с открытым исходным кодом из проектов Imperial College FLT и flt-regular.

Источники

• Исходное объявление Anthropic в X
• Anthropic: формализация последней теоремы Ферма
• Репозиторий Anthropic с последней теоремой Ферма
• Кевин Баззард: FLT—Anthropic опередила меня
• Исследовательская статья Prove2Me
• Проект формализации Lean в Imperial College London
• Репозиторий Lean Comparator и модель верификации