Доказательство теоремы Ферма в Lean показывает, как ИИ может перевести известную математику в код, который проверяет маленькое доверенное ядро. Это не новая теорема и не замена доказательства Эндрю Уайлса. Новизна заявленного результата в масштабе формализации: огромная цепочка промежуточных утверждений дошла до финальной цели и была принята Lean.
4 сентября 2026 года Anthropic сообщила, что команда агентов Claude за 11 дней подготовила сквозную формализацию. По данным самой компании, работа заняла 13 миллионов строк Lean, около 6 миллиардов выходных токенов и 30 300 доказанных промежуточных теорем, из которых 29 500 вошли в финальный результат. Эти числа описывают эксперимент Anthropic и требуют именно такой атрибуции.
Тема вызвала не только восторг, но и подробный спор о доверии: в снимке Hacker News от 8 сентября обсуждение набрало 766 баллов и 509 комментариев. Вопросы сообщества полезны: что именно проверил Lean, совпадает ли формальная формулировка с исходной и можно ли поддерживать такой объём кода?
Доказательство теоремы Ферма в Lean: что именно проверено
Великая теорема Ферма утверждает: для положительных целых a, b, c и натурального n больше 2 уравнение ниже не имеет решений. На простых числах это легко исследовать перебором, но никакой конечный набор примеров не доказывает утверждение для всех возможных чисел.
Уайлс опубликовал принятое математическим сообществом доказательство в 1995 году после исправления найденного ранее пробела. Anthropic пишет, что агенты формализовали упрощённый вариант этого пути, связанный с работой Дармона, Даймонда и Тейлора. ИИ не нашёл теорему заново. Он развернул существующее рассуждение в намного более подробную форму, где пропущенный переход нельзя закрыть словами «очевидно».
Что здесь новое
Скорость и масштаб автоматической формализации, организация тысяч зависимостей и финальная проверка всей цепочки Lean.
Чего здесь нет
Нового доказательства теоремы, независимой проверки всех заявлений Anthropic или человеческого объяснения каждой из 13 миллионов строк.
Почему Lean похож на язык программирования
Официальный сайт Lean описывает его как язык для точного проверяемого кода и формальных доказательств. Утверждение играет роль типа, а доказательство должно дать значение этого типа. Небольшое ядро проверяет, что каждый применённый шаг разрешён правилами. Автоматические тактики могут искать решение, но итоговый объект всё равно проходит через ядро.
example (P : Nat → Prop)
(checked : ∀ n, n < 10 → P n) :
∀ n, P n := by
intro n
exact checked n -- не хватает доказательства n < 10Этот схематичный пример не компилируется. Из того, что свойство проверено для чисел меньше 10, нельзя вывести его для любого натурального числа. Lean остановится на недостающем условии. Обычный математический текст может спрятать такой скачок в длинном абзаце, а формальная система требует закрыть цель точным доказательством.
Интерактивная цепочка: найдите шаг, который не компилируется
Представьте упрощённый аргумент. Сначала прочитайте три карточки, затем запустите проверку. Здесь специально спрятана типичная ошибка обобщения.
Компьютер проверил показатель степени n от 3 до 9.
компилируетсяВ проверенном диапазоне контрпримеров не найдено.
компилируетсяЗначит, контрпримеров нет для всех n больше 2.
проверитьИменно поэтому «проверить много значений» и «доказать теорему» являются разными задачами. Тесты повышают уверенность в программе на выбранных сценариях. Формальное доказательство показывает, что вывод следует из заданных предпосылок по правилам системы.
Как агенты справились с объёмом
По описанию Anthropic, ранние попытки теряли состояние проекта и плохо координировались. Успех пришёл после перехода на Prove2Me. Платформа хранила ориентированный ациклический граф утверждений, разделяла формулировки и доказательства по файлам и помогала искать уже готовые леммы. Это знакомая разработчику идея: большую задачу разбивают на независимые интерфейсы, а сборка показывает, где связь нарушена.
Размер результата одновременно впечатляет и создаёт инженерный вопрос. Код, который прошёл проверку, может оставаться трудным для чтения, повторного использования и независимого аудита. Поэтому машинная проверка и человеческое понимание дополняют друг друга. Первая ловит логический разрыв в формальной записи, второе объясняет, почему выбранный путь содержателен и соответствует исходной математике.
Можно ли теперь удалить человеческое доказательство?
Нет. Оно задаёт идеи, структуру и смысл. Формализация добавляет машинно проверяемый слой и может обнаружить скрытый пробел.
Означает ли «Lean принял» абсолютную истину?
Это означает, что формальный вывод корректен относительно записанных определений, аксиом и доверенной реализации проверяющего ядра. Правильность перевода исходной задачи остаётся отдельным вопросом.
Нужно ли начинающему знать высшую математику, чтобы попробовать Lean?
Нет. Начать можно с логики, натуральных чисел и коротких утверждений. Полная формализация теоремы Ферма находится на совсем другом уровне сложности.
С чего начать ученику Codik
Возьмите не Ферма, а простое утверждение: сумма двух чётных чисел чётна. Сначала запишите его обычными словами, затем перечислите определения и только после этого посмотрите синтаксис Lean. Если система отвергает шаг, не просите ИИ сразу переписать весь файл. Спросите, какая цель открыта, какое предположение доступно и какой тип должен получиться.
Такой подход тренирует ту же дисциплину, что и отладка программы. Материал про алгоритмические задачи поможет раскладывать решение на проверяемые шаги, а статья об обучении с ИИ подскажет, как получать намёки без слепого копирования.
Главный вывод
История с теоремой Ферма важна не потому, что ИИ внезапно заменил математиков. Она показывает масштаб задачи, которую агенты смогли превратить в проверяемый код при подходящей инфраструктуре. Чтобы почувствовать разницу между примером, тестом и доказательством, начните с небольших программ на курсе Python-разработчика и каждый вывод связывайте с наблюдаемой проверкой.