Claude за 11 дней собрал крупнейшее в истории доказательство в Lean

Коротко о главном

4 сентября 2026 года Anthropic сообщила, что её модель Claude за 11 дней в основном автономно построила первое сквозное машинно-проверяемое доказательство Великой теоремы Ферма на языке Lean. Прогон породил 13 млн строк кода Lean и доказал 29 500 промежуточных теорем в финальной версии, израсходовав около 6 млрд выходных токенов, — это крупнейшее формальное доказательство в истории. Ценность новости не в самой теореме, а в том, что ИИ-агенты впервые выдержали месячную цепочку строгих рассуждений без потери связности.

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

Важная оговорка: Claude не «изобрёл» доказательство Уайлса, а формализовал уже известное — перевёл человеческую математику в вид, который проверочный ассистент Lean принимает автоматически. Итог сверил математик Кевин Баззард (Imperial College London), а сама проверка Lean опиралась лишь на три стандартные аксиомы. Это не автономное открытие, но убедительная демонстрация того, что длинные ИИ-процессы можно делать проверяемыми.

Что именно сделал Claude

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

Масштаб прогона беспрецедентен. Несколько десятков агентов Claude работали параллельно, сгенерировав в сумме 30 300 доказательств, из которых 29 500 вошли в финальную версию. Суммарный расход — около 6 млрд выходных токенов от внутренней исследовательской модели общего назначения. Одиннадцать дней «настенного» времени — это не один непрерывный поток рассуждений, а результат массового параллелизма: множество агентов одновременно закрывали отдельные леммы и собирали их в общий граф зависимостей.

Почему первая попытка провалилась

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

Prove2Me взяла на себя то, с чем не справляется одиночный агент на длинной дистанции: поддержку графа зависимостей между теоремами, ускорение компиляции Lean и поиск с переиспользованием уже доказанных лемм. По оценке Anthropic, неудачные ранние попытки дали примерно 7% небоилерплейт-строк финального кода — то есть даже «провалы» частично пошли в дело. Практический вывод для инженеров: на длинных ИИ-процессах решает не сама модель, а обвязка вокруг неё — оркестрация, память о промежуточных результатах и внешняя проверка.

Ключевые цифры прогона

Длительность: 11 дней в основном автономной работы.

Объём кода: 13 млн строк Lean — крупнейшее формальное доказательство из когда-либо написанных.

Доказано теорем: 30 300 всего, из них 29 500 использованы в финальном доказательстве.

Расход вычислений: около 6 млрд выходных токенов.

Проверка: Lean подтвердил доказательство, используя лишь три свои стандартные аксиомы; отдельный компаратор сверил формулировку теоремы с версией из библиотеки Mathlib.

Вклад неудачных попыток: около 7% небоилерплейт-строк финального кода.

Что это значит для команд разработки

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

В прикладной разработке аналог верификатора Lean — это тесты, типы, статический анализ и формальные спецификации. Агент, который пишет код и сам же проверяет его набором строгих гейтов, надёжнее агента, отвечающего «на глаз». Именно поэтому связка «генерация + автоматическая проверка каждого шага» — практичный шаблон для внедрения ИИ в CI/CD, автотесты и ревью, а не футуристика. Отдельная ценность истории — честность отчёта: Anthropic прямо назвала долю провальных попыток и роль стороннего инструмента, и такую же прозрачность стоит закладывать в собственные ИИ-пайплайны.

Как переносить приём в свои продукты

Не пытайтесь заставить один агент «додумать» длинную задачу целиком. Разбейте её на модули с чёткими интерфейсами — так же, как леммы в доказательстве, — и позвольте агентам закрывать их параллельно.

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

Проверяйте каждый шаг детерминированно. Тесты, типы, контрактные проверки и линтеры — ваш Lean. Корректность нельзя доверять генератору, её должен подтверждать независимый верификатор.

Считайте бюджет заранее. 6 млрд токенов — напоминание, что длинные автономные прогоны стоят денег; закладывайте лимиты и точки останова, чтобы стоимость не уходила в неизвестность.

Сохраняйте «неудачные» результаты. В прогоне 7% полезного кода пришли из провальных попыток — промежуточные артефакты часто переиспользуются, если их не выбрасывать.

Часто задаваемые вопросы

Claude сам доказал теорему Ферма? Нет. Доказательство Великой теоремы Ферма принадлежит Эндрю Уайлсу (1994). Claude выполнил формализацию — перевёл известное доказательство в машинно-проверяемый вид на Lean, чтобы его корректность мог автоматически подтвердить программный ассистент.

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

Что за Prove2Me и зачем он понадобился? Это открытая платформа для формализации математики от Тяньи Пэна и коллег из Колумбийского университета. Она хранит граф зависимостей теорем, ускоряет компиляцию Lean и переиспользует доказанные леммы. Без неё ранние попытки Claude проваливались.

Можно ли доверять результату? Финальное доказательство проверил сам Lean, опираясь только на три стандартные аксиомы, а формулировку сверил компаратор с библиотекой Mathlib; итог отдельно просмотрел математик Кевин Баззард. Это делает результат воспроизводимым и проверяемым.

Источники

Anthropic — Formalizing Fermat's Last Theorem, 4 сентября 2026 года (первоисточник).

SiliconANGLE — Anthropic uses Claude to formalize proof of Fermat's Last Theorem, 4 сентября 2026 года.