13 миллионов строк за 11 дней: что Claude сделал с теоремой Ферма — и почему это важнее самой теоремы

ИИ не решил за 11 дней задачу, над которой человечество билось три с половиной века. Но то, что произошло, может оказаться не менее важным.

В 1637 году Пьер Ферма записал на полях книги знаменитое утверждение: для целых n > 2 уравнение a^n + b^n = c^n не имеет решений в положительных целых числах. Ферма утверждал, что знает доказательство, но полей книги для него недостаточно.

Первое принятое математическим сообществом доказательство появилось лишь в 1995 году. Работа Эндрю Уайлса, завершённая вместе с Ричардом Тейлором после обнаружения проблемы в первоначальном варианте, заняла 129 страниц, а её проверка потребовала месяцев работы математиков.

Теперь Anthropic сообщила о другом рубеже: Claude создал первое полное компьютерно проверенное доказательство Великой теоремы Ферма.

Но здесь принципиально важно различать открытие доказательства и его формализацию.

Claude не придумал альтернативу Уайлсу. Система формализовала существующую математическую линию доказательства — в частности, используя упрощённое изложение Анри Дармона, Фреда Даймонда и Ричарда Тейлора, — переведя огромную цепочку математических рассуждений в код Lean, где каждый логический переход может быть проверен компьютером.

11 дней, 13 миллионов строк

Масштаб эксперимента необычен даже по меркам современных AI-систем.

Claude работал в основном автономно около 11 дней. За это время система написала около 13 млн строк Lean, получила компьютерно проверяемые доказательства примерно 30 300 теорем, из которых около 29 500 использованы в финальном доказательстве.

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

Финальный результат проверил Lean. В доказательстве не осталось недоказанных заглушек, а используется только три стандартные аксиомы Lean. Отдельный comparator подтвердил, что формулировка доказываемой теоремы соответствует формулировке Великой теоремы Ферма в Mathlib.

Самого Claude оказалось недостаточно

Наиболее значимым оказалось другое.

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

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

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

Получилась уже не просто LLM, решающая математическая задачу, а целая архитектура:

Claude → десятки агентов → граф задач и общая память → Lean → формальная проверка.

И именно эта архитектура, возможно, важнее самой теоремы Ферма.

Как не пропустить ошибку ИИ

Главная проблема LLM хорошо известна: модель способна построить длинное, убедительное и при этом неверное рассуждение.

Обычно эту проблему пытаются решать улучшением самой модели или использованием другой модели в качестве проверяющей.

Формальная верификация предлагает принципиально иной подход.

ИИ не обязательно должен быть безошибочным. Нужно создать среду, в которой его ошибка не сможет пройти проверку.

Получается замкнутый цикл:

ИИ предлагает решение → формальная система проверяет → ошибка отклоняется → ИИ исправляет → проверка повторяется.

В финале значение имеет только одно: проходит ли созданная Claude конструкция независимую формальную проверку.

Почему это выходит далеко за пределы математики

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

Тогда меняется сама постановка проблемы надёжности AI.

Сегодня мы в значительной степени пытаемся создать модель, которая ошибается всё реже.

Другой путь — строить системы, где AI может ошибаться сколько угодно в процессе поиска, но ошибочный конечный результат невозможно принять.

Это гораздо более реалистичная инженерная цель, чем абсолютная безошибочность модели.

Формализация — ещё не открытие

И здесь важно не смешивать два разных достижения Anthropic.

В случае Великой теоремы Ферма новое достижение — прежде всего автоматическая формализация и верификация уже существующей математики. Anthropic прямо подчёркивает это различие.

В другом эксперименте Claude работал уже над проблемой, связанной с гипотезой Римана, и получил новый математический результат: улучшил известную нижнюю границу доли нетривиальных нулей дзета-функции на критической прямой с примерно 41,6% до 67,2%. Саму гипотезу Римана Claude не доказал.

Разница фундаментальная:

Ферма — AI формализует существующее знание.

Риман — AI участвует в создании нового знания.

Соединение этих двух возможностей — генерации новой математики и её последующей машинной верификации — и представляет, пожалуй, наиболее интересную перспективу.

Автоматическая формализация всей современной математической литературы пока не наступила. Сам результат Anthropic опирается на Mathlib и на ранее созданные открытые наработки проектов Imperial College London и flt-regular. Это не «11 дней вместо нескольких столетий человеческой математики».

Но граница явно сдвинулась.

Возможно, следующий этап развития ИИ — машина, результат которой можно автоматически доказать правильным.

---

Источники:

• Anthropic — Formalizing Fermat's Last Theorem

• Полный Lean-код доказательства — GitHub Anthropic

• Prove2Me — Scaling Math Formalization

• Anthropic — результаты Claude по дзета-функции Римана