Anthropic опубликовала машинно проверенную формализацию Великой теоремы Ферма в Lean 4 4 сентября; по данным GitHub API, репозиторий был создан в 14:21:04 UTC. Широко разошедшееся утверждение звучало так: Claude доказал Великую теорему Ферма за 11 дней. Однако собственные файлы репозитория описывают нечто более узкое и, в одном отношении, более интересное.
Что говорит файл атрибуции
В репозитории есть ATTRIBUTION.md, где зафиксированы 106 файлов, содержащих материалы из проекта FLT Imperial College London под руководством Кевина Баззарда и из проекта flt-regular — «54 в Definitions/, 52 в P2M/Sol/; и 23 файла, воспроизводящие текст Mathlib». В десятках строк указано «whole file (100%)». В файле NOTICE датируется заимствование: «Material was taken from the project's main branch as of 2026-05-21». При переносе инструментария на Lean 4.33 в файле атрибуции отмечено, что он «left the other 41 byte-identical».
Проверка реальна
Ничто из этого не отменяет проверки. В README указано, что собраны все 60 475 модулей, что #print axioms fermat_last_theorem ограничен тремя стандартными аксиомами и что в ни одном модуле нет axiom, sorry, native_decide, unsafe или partial def. Сборка заняла 5 часов 32 минуты при 96 jobs при пиковом потреблении 153 GB памяти. Собственные оценки Anthropic: 13 миллионов строк Lean, 29 500 промежуточных теорем, использованных в финальном доказательстве, и около шести миллиардов выходных токенов.
В чем ошибочна принятая подача
В трех вещах. Claude не доказал ничего нового — это автоформализация экспозиции Дармона–Даймонда–Тейлора 1995 года аргумента Уайлса–Тейлора–Уайлса, доказательства, завершенного людьми 31 год назад. Это не сделано без участия человека: по собственной оценке Anthropic, девятая часть репозитория содержит человеческий текст Lean, местами дословно. А Баззард, математик, на чью рецензию ссылается Anthropic, написал в тот же день в своем блоге, что «математически эта работа Anthropic говорит нам по сути ничего» и что формализация «просто добросовестно следует ранней литературе по доказательству и ничего не добавляет». Несколько изданий также назвали это самым большим файлом такого рода; на деле это 60 475 модулей, а не файл.
Честное утверждение все равно масштабно
Теперь машины способны переводить тысячи страниц уже существующей математической литературы в форму, проверяемую ядром, менее чем за две недели, опираясь на несколько лет добровольной работы в Lean. Это реальный результат в скорости перевода. Но это не результат математического открытия, и README прямо признает оставшийся разрыв: «What no tool can check is that each intermediate theorem means what its name suggests.»