Доказательство без пробелов: как выглядит Великая теорема Ферма на языке Lean 4

Великая теорема Ферма почти четыре века простояла как заметка на полях книги, а потом ещё почти сорок лет — как доказательство, которое понимали от силы несколько десятков человек на планете. Работа Уайлса и Тейлора-Уайлса 1994-1995 годов опиралась на модулярность эллиптических кривых, гипотезу Таниямы-Шимуры-Вейля и целый этаж алгебраической геометрии, который проверяли рецензенты, а не компьютеры. Репозиторий anthropics/fermats-last-theorem переносит этот же аргумент — Фрея, Серра, Рибета, Уайлса, Тейлора-Уайлса — в среду, где доказательство проверяет не редколлегия журнала, а ядро языка Lean 4.

Это не переизложение теоремы для широкой публики и не учебный пример. В файле Theorems/Thm_fermat_last_theorem.lean лежит формальное утверждение: для натурального n не меньше трёх и положительных a, b, c сумма a^n + b^n никогда не равна c^n. Строка кода выглядит буднично, но за ней — 60 475 модулей репозитория, которые собираются с нуля вместе с Mathlib, огромной библиотекой формализованной математики для Lean, скомпилированной из исходников, а не подключённой готовым бинарником.

Самое строгое место в проекте — не сама теорема, а файл FinalCheck.lean, который выполняет над готовым доказательством ещё одну проверку: печатает список аксиом, на которые оно опирается. Если бы кто-то тайком добавил вспомогательную аксиому, вставил sorry вместо недоделанного куска доказательства или использовал native_decide — способ ускорить вычисления ценой доверия к внешнему коду, — сборка проекта просто не прошла бы. Вывод, который требует FinalCheck.lean, — ровно три стандартные аксиомы Lean: propext, Classical.choice и Quot.sound. Ничего лишнего. Это тот минимум, на котором держится вся классическая математика, оформленная в Lean, и авторы явно фиксируют, что доказательство FLT не потребовало ни одного дополнительного допущения.

Проверено дважды, разными способами

Одной сборки авторам показалось мало. Build прогнали через инструмент comparator от leanprover — он сверяет итоговую сборку с отдельно сформулированным «вызовом» (Challenge.lean), написанным только средствами Mathlib, и подтверждает, что доказанное утверждение и все упомянутые в нём константы совпадают с условием задачи слово в слово, что не используется никаких посторонних аксиом и что весь код, включая саму Mathlib, действительно проходит через кернел Lean. Вердикт инструмента — простая фраза «Your solution is okay!», без затей.

Но и это не конец. Готовое окружение экспортировали через lean4export и скормили независимой реализации кернела Lean — nanoda, написанной на Rust отдельной командой (ammkrn/nanoda_lib), которая ничего не знает про сам Lean и его внутреннюю кухню. Nanoda проверила 1 052 234 объявлений и не нашла ни одной ошибки. Чтобы это стало возможным за разумное время, авторы репозитория внесли в nanoda четыре небольших патча: один добавляет вывод прогресса, три остальных ускоряют поиск определительного равенства — без них отдельные декларации этого доказательства могли занимать немодифицированную nanoda много часов. Идея простая и по-хорошему параноидальная: если одно и то же доказательство независимо признают верным два разных кернела, написанных разными людьми на разных языках, вероятность того, что оба ошиблись одинаково, стремится к нулю.

Что это на самом деле

Авторы прямо называют проект research artifact — исследовательским артефактом, а не библиотекой и не продуктом. Он не принимает контрибьюшенов и не поддерживается на постоянной основе: это снимок одного конкретного достижения, зафиксированный на конкретных версиях Lean 4.33.1 и Mathlib v4.33.0, закреплённых по коммиту в lakefile.lean. Для тех, кто хочет пройти доказательство шаг за шагом, а не только увидеть финальную теорему, в репозитории есть файл PROOF-PATH.md, который называет каждый этап рассуждения и соответствующую Lean-теорему, а также папка html/, где всё доказательство можно листать в браузере офлайн, без установки Lean и Mathlib.

Важно понимать, что здесь формализовано именно доказательство, а не новое открытие: математическое содержание принадлежит Фрею, Серру, Рибету, Уайлсу и Тейлору с Уайлсом, работавшим тридцать лет назад. Ценность проекта — в переводе этого рассуждения на язык, где каждый логический шаг явный и проверяемый механически, без доверия к человеческой внимательности рецензента. Формализация такого масштаба — редкость: большинство формализованных теорем в Mathlib на порядки скромнее по объёму зависимостей. То, что теорема уровня FLT вообще уместилась в проверяемое ядром доказательство без единого sorry, — само по себе демонстрация того, куда сегодня дошли инструменты формальной верификации математики.

742 звезды и 57 форков на GitHub — цифры скромные по меркам популярных фреймворков, но для проекта на Lean, языке узкого сообщества математиков и computer scientists, это заметный отклик. Он говорит не столько о хайпе, сколько о том, что формальная математика перестаёт быть нишевым развлечением энтузиастов и превращается в инструмент, которым можно закрыть один из самых знаменитых открытых вопросов теории чисел — точнее, теперь уже закрытый и дважды перепроверенный.