Ферма без права на ошибку: как машина дважды перепроверила доказательство века

Есть доказательства, которые убеждают математиков, и есть доказательства, которые убеждают компьютер. Второе — заведомо более жёсткий стандарт: ядро Lean не читает между строк, не прощает пропущенных шагов и не соглашается с аргументом «это же очевидно». Именно такому стандарту подвергли Великую теорему Ферма в новом репозитории anthropics/fermats-last-theorem — 742 звезды и Lean как единственный язык в статистике репозитория говорят, что сообщество заметило это не случайно.

Суть проекта предельно конкретна: это полное, машинно-проверенное доказательство теоремы Ферма в Lean 4, построенное поверх библиотеки Mathlib (Lean 4.33.1, Mathlib v4.33.0, версии зафиксированы прямо в lakefile.lean). Логика доказательства — не новая математика, а формализация уже известного пути: Фрей, Серр, Рибет, Уайлс и Тейлор-Уайлс. То есть авторы не искали новый способ доказать теорему, а перевели существующее рассуждение на язык, который проверяется автоматически, шаг за шагом, без права на пропуски. Файл PROOF-PATH.md называет каждый этап и соответствующую Lean-теорему, которая его несёт, а папка html/ превращает всё доказательство в веб-страницы — его можно листать офлайн, как обычный текст, только каждое утверждение в нём кликабельно и прослеживаемо до аксиом.

Формулировка, которая ничего не прощает

Центральный файл Theorems/Thm_fermat_last_theorem.lean объявляет теорему в её самой прямой форме: для натурального n не меньше трёх и положительных a, b, c сумма a^n + b^n никогда не равна c^n. Формулировка простая, но проверка того, что стоит за ней, — нет. Целевой файл сборки по умолчанию, FinalCheck.lean, содержит команду #print axioms fermat_last_theorem — и сборка провалится, если доказательство опирается на что-то, кроме трёх стандартных аксиом Lean: propext, Classical.choice и Quot.sound. Никакого sorry (заглушки для недоказанных мест), никаких добавленных аксиом, никакого native_decide, который в Lean позволяет обходить часть проверки через быстрое вычисление вместо формального вывода. Это не декларация честности — это встроенное в сборку условие: если доказательство хоть где-то срезало путь, проект просто не соберётся. Тот же FinalCheck.lean выводит из этой теоремы формулировку FermatLastTheorem, уже существующую в самой Mathlib, — то есть доказанное утверждение состыковано с тем, как теорему определяет сообщество библиотеки, а не сформулировано удобным для авторов образом в стороне.

Два ядра вместо одного

Самая интересная часть — не сам факт доказательства (Уайлс закрыл теорему математически ещё в девяностых), а то, как тщательно здесь выстроена независимая проверка. Сборка с нуля через lake build на Lean 4.33.1 — версии, включающей исправления надёжности ядра 2026 года, — скомпилировала все 60 475 модулей репозитория, и каждое объявление в них прошло через ядро Lean. Дальше в дело вступил инструмент leanprover/comparator: он сверил результат сборки с отдельным файлом-вызовом, Challenge.lean, который формулирует теорему исключительно средствами Mathlib, и подтвердил, что доказанное утверждение и все упомянутые в нём константы идентичны условию вызова, что не используется никаких посторонних аксиом и что вся цепочка, включая саму Mathlib, воспроизводится ядром Lean. Вердикт инструмента — короткое «Your solution is okay!», сухая формула для итога многолетней математической работы, переведённой в формальный код.

Но на этом проверка не остановилась. Экспорт того же самого окружения прогнали через nanoda — независимое ядро Lean, написанное на Rust с нуля другой командой. Оно проверило больше миллиона объявлений без единой ошибки. Чтобы это стало возможным за разумное время, авторы внесли в nanoda четыре небольших патча — один добавляет индикатор прогресса, три ускоряют поиск определяющего равенства, без которого отдельные части доказательства могли занимать немодифицированное ядро много часов. Это тот случай, когда независимая верификация не осталась декларативной фразой в README, а потребовала реальной инженерной работы над сторонним инструментом.

Что это, а что нет

Авторы прямо называют репозиторий исследовательским артефактом: он не поддерживается и не принимает вклады со стороны. Это не библиотека, которую нужно встраивать во что-то, и не живой проект с бэклогом задач. Это зафиксированный во времени результат — доказательство, которое можно открыть, прочитать по шагам через PROOF-PATH.md и проверить любым независимым способом, потому что все аксиомы, на которые оно опирается, названы явно и их всего три.

В этом, пожалуй, и есть главный интерес истории — не в том, что теорему Ферма доказали снова (она доказана), а в том, что доказательство такого масштаба вообще возможно перевести в форму, которую проверяет не один, а два независимых по происхождению инструмента, и оба соглашаются с результатом. Формализация подобной сложности — редкость даже для активно развивающегося сообщества Lean и Mathlib, и то, что она появилась именно сейчас, с явной фиксацией версий и двойной кросс-проверкой, говорит больше о зрелости инструментов формальной верификации, чем о самой теореме.