Структура гигантского репозитория
Anthropic опубликовала первое формализованное доказательство Великой теоремы Ферма на языке Lean. В центре внимания оказался размер кодовой базы: 13 499 380 строк в 60 478 файлах. Однако ключевой вопрос — что именно занимает этот объем. Анализ структуры (коммит aa2d8b3 от 7 сентября 2026 года) показал, что 88,5% репозитория — это тела доказательств (каталог P2M/Sol), а не определения или утверждения теорем.
Архитектура решения строго разделена: каждая из 29 511 целевых теорем имеет отдельный файл утверждения в каталоге Theorems/ и соответствующий файл решения в P2M/Sol. При этом 99,7% файлов решений содержат декларацию, буквально названную theorem solution. Это указывает на то, что Claude генерирует огромное количество новых утверждений, а не переиспользует существующие из Mathlib.
Сравнение с человеческим кодом: плотность против количества
Главный инсайт анализа заключается в сравнении «плотности» шагов доказательства. Вопреки ожиданиям, машинный код не является чрезмерно многословным на уровне отдельного шага. Медианное количество строк на одну декларацию у Claude составляет всего 8 строк против 4 строк у человеческих авторов в Mathlib. Разница в два раза, а не в десятки раз, как можно было бы предположить, глядя на общий объем.
Проблема масштаба кроется в количестве шагов. Для закрытия одной теоремы Claude сгенерировал 562 341 декларацию, тогда как в базовой библиотеке Mathlib (на том же коммите) всего 185 411 декларация. Машине потребовалось в три раза больше промежуточных шагов, чтобы достичь результата, который люди выводили десятилетиями.
Метрики детализации
Ниже приведено сравнение статистических показателей длины шага доказательства между решением Anthropic и библиотекой Mathlib:
| Метрика | Anthropic (Fermat Proof) | Mathlib (Human-written) |
|---|---|---|
| Количество деклараций | 562 341 | 185 411 |
| Медианная длина шага (строк) | 8 | 4 |
| Средняя длина шага (строк) | 17.2 | 6.2 |
| Длина шага на уровне p99 (строк) | 166 | 33 |
| Максимальная длина шага (строк) | 3 123 | 256 |
Технические детали и верификация
Рабочая директория репозитория занимает 1,9 ГБ. В коде присутствует ровно одна конструкция sorry (заглушка для недоказанного утверждения), которая является намеренной частью тестового файла компаратора, как указано в его заголовке. Это подтверждает, что само доказательство Ферма является полным и верифицируемым.
Результаты анализа показывают, что «огромность» доказательства обусловлена структурными особенностями генерации ИИ: необходимостью выводить каждое логическое следствие явно, а не стилистической избыточностью. Для машины, закрывающей теорему, требующую человеческих усилий на протяжении веков, удвоение verbosity на шаг является узким разрывом, а не критическим недостатком.
Источник: Towards AI pub ↗