Anthropic опубликовала доказательство теоремы Ферма в Lean 4

Компания Anthropic опубликовала на GitHub репозиторий с полным, машинно проверенным доказательством Великой теоремы Ферма на языке формальной верификации Lean 4 поверх библиотеки Mathlib (Lean 4.33.1, Mathlib v4.33.0, версия зафиксирована коммитом в lakefile.lean). Доказательство следует классической схеме Фрея, Серра, Рибета, Уайлса, Тейлора-Уайлса. Файл PROOF-PATH.md называет каждый шаг доказательства и соответствующую Lean-теорему, а папка html/ (около 390 МБ) представляет весь материал как автономный сайт, который открывается офлайн без сервера: 29 511 страниц теорем (с точной Lean-формулировкой, связями с другими теоремами и графом зависимостей), 1450 страниц модулей с определениями и поиск по всем именам.

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

Итоговая теорема сформулирована в терминах встроенных в Lean натуральных чисел и операций +, ≤, <, ≠; единственный элемент, взятый из Mathlib, возведение в степень на натуральных числах, которое там определено как встроенная операция Lean. Это подтверждает инструмент comparator, сверяя, что все упомянутые в формулировке определения совпадают со стандартной библиотекой Mathlib, поэтому доверять остальной Mathlib не нужно: всё, что лежит под самим утверждением, заново проверяет ядро Lean.

Корректность подтверждена тремя независимыми способами. Во-первых, сама сборка (lake build) на Lean 4.33.1 с исправлениями корректности ядра 2026 года: собраны все 60 475 модулей репозитория, каждое утверждение проверено ядром Lean, и сборка целенаправленно падает, если доказательство опирается не ровно на три стандартные аксиомы Lean, propext, Classical.choice и Quot.sound, то есть без sorry, без добавленных аксиом и без native_decide. Во-вторых, инструмент leanprover/comparator версии v4.33.0 сверил результат сборки с отдельно сформулированным контрольным утверждением (Challenge.lean, использующим только Mathlib) и подтвердил, что доказанное утверждение и все упомянутые в нём константы совпадают с контрольным, что не используется никаких иных аксиом и что всё доказательство целиком, включая Mathlib, заново проходит через ядро Lean; итоговый вердикт инструмента, «Ваше решение верно!». В-третьих, независимое Lean-ядро nanoda версии 0.4.13, написанное на Rust, приняло экспорт того же окружения и проверило 1 052 234 утверждения без ошибок; авторы применили к nanoda четыре собственных патча (один добавляет вывод прогресса, три ускоряют поиск на определяющее равенство) и подчёркивают, что ни один из патчей не добавляет, не убирает и не ослабляет ни одно правило типизации.

Ресурсоёмкость подтверждена цифрами: сама сборка заняла у авторов 5 ч 32 мин при 96 параллельных потоках с пиковой памятью 153 ГБ, проверка comparator, 14 ч 46 мин с пиковой памятью 230 ГБ (авторы советуют закладывать 300 ГБ), а запись 37,8-гигабайтного экспорта окружения для nanoda и сама проверка nanoda заняли вместе ещё около полутора часов. Под саму сборку нужно около 67 ГБ места на диске плюс временные C-файлы объёмом около 220 ГБ, которые можно удалять по ходу дела.

Репозиторий выпущен под лицензией Apache 2.0; часть кода переиспользует три открытых Apache-2.0 проекта, проект FLT Имперского колледжа Лондона под руководством Кевина Баззарда (пакет Frey, теория представлений Галуа, деформационная теория и другое), проект flt-regular (теорема Куммера) и саму Mathlib. Файл ATTRIBUTION.md перечисляет 106 файлов с материалом из первых двух проектов и 23 файла, воспроизводящих текст Mathlib. Источник не утверждает, что Баззард или проект Имперского колледжа как-то участвовали в этой работе или одобрили её, только что часть их кода использована с указанием авторства.

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

Ключевые факты

• Anthropic опубликовала на GitHub полное машинно-проверенное доказательство Великой теоремы Ферма на Lean 4 поверх Mathlib, по классической схеме Фрея, Серра, Рибета, Уайлса, Тейлора-Уайлса.
• Lean-код писали ИИ-агенты поверх открытого кода людей; собрано 60 475 модулей репозитория, и сборка проходит только если доказательство опирается ровно на три стандартные аксиомы Lean (без sorry, без добавленных аксиом, без native_decide).
• Результат независимо перепроверили инструмент comparator (вердикт «Ваше решение верно!») и отдельное Lean-ядро nanoda на Rust, проверившее 1 052 234 утверждения без ошибок.
• Полная проверка ресурсоёмка: сборка заняла 5 ч 32 мин, а проверка comparator, почти 15 часов, с пиковым потреблением памяти до 230 ГБ.
• Репозиторий включает офлайн-сайт из 29 511 страниц теорем и 1450 страниц определений, выпущен под Apache 2.0 с указанием заимствований из проекта FLT Кевина Баззарда и flt-regular.

Почему это важно

Это не просто ещё одна формализация: доказательство целиком, включая теорему Ферма и лежащую под ней часть Mathlib, написано ИИ-агентами и при этом полностью проверяемо машиной, от него не требуется доверие к тому, что написали агенты, а требуется только доверие к ядру Lean. Сборка технически не может завершиться успехом, если в доказательстве осталась хотя бы одна недоказанная заглушка (sorry) или лишняя аксиома: это встроенная проверка, а не обещание авторов. Плюс к этому результат независимо переподтверждён двумя разными инструментами, comparator и полностью отдельным ядром nanoda на Rust, так что ошибка одного инструмента проверки не осталась бы незамеченной.

Кому это важно

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

Как это применить

Репозиторий открыт: его можно склонировать, собрать локально командой lake build (нужны Linux или macOS, elan и сетевое подключение, Mathlib компилируется из исходников) и прогнать через собственные скрипты verification/comparator и verification/nanoda, повторив всю цепочку проверки самостоятельно. Для тех, кто хочет просто посмотреть на структуру доказательства без сборки, в репозитории лежит папка html/, статический сайт объёмом около 390 МБ, который открывается прямо в браузере офлайн и позволяет пройти доказательство шаг за шагом, посмотреть формулировку любой из 29 511 теорем и граф её зависимостей.

Можно ли доверять

Технической части, да, в измеримой степени: результат подтверждён тремя независимыми проверяющими (ядро Lean при сборке, comparator, ядро nanoda), а не только заявлением авторов, и авторы прямо публикуют, на каких именно трёх аксиомах держится итоговое утверждение. Но у доверия есть чётко названная граница: ни один из этих инструментов не проверяет, что промежуточная лемма с машинно сгенерированным именем действительно доказывает то, что по смыслу должна доказывать, это, по словам самих авторов, остаётся на суд человека, читающего PROOF-PATH.md. Источник также не даёт ни академической публикации, ни рецензии математического сообщества, только сам репозиторий.

Риски и подводные камни

Код написан ИИ-агентами и, по признанию авторов, не предназначен для чтения человеком: имена машинно сгенерированы, комментарии в основном удалены, а значит независимый содержательный аудит логики (а не только формальной корректности) затруднён физически. Полная независимая перепроверка доступна не каждому: авторам она потребовала сотни гигабайт оперативной памяти и около суток машинного времени. Источник, только GitHub-репозиторий без даты завершения работы, без указания конкретной использованной ИИ-системы и без научной публикации, что затрудняет проверку контекста и приоритета. Наконец, сам репозиторий помечен как исследовательский артефакт, который не поддерживается и не принимает вклад со стороны.

«Ваше решение верно!»

— вывод инструмента leanprover/comparator по итогам проверки доказательства