Теорему Ферма формализовали за 11 дней: люди написали одну строку, остальное написали агенты

Баззард пять лет ведёт собственный проект формализации Великой теоремы Ферма, под него выигран грант EPSRC на £1 млн. Агенты Anthropic прошли этот путь с 7 по 17 августа 2026 года.

Впервые машина довела до конца доказательство такого размера, а человек не написал внутри ни строки математики и ни строки Lean.

Масштаб работы. 29 511 теорем и около 533 тысяч вспомогательных лемм, примерно 13 млн строк кода, около 6 млрд выходных токенов. Работала внутренняя исследовательская модель общего назначения, по описанию компании примерно сопоставимая с Claude Fable 5.1. Публично её нет.

Новой математики здесь не появилось. Агенты перевели на Lean изложение Darmon–Diamond–Taylor 1995 года, 106 файлов адаптированы из уже существовавших проектов формализации.

Собрать можно у себя. Репозиторий anthropics/fermats-last-theorem лежит на GitHub, сборка `LEAN_NUM_THREADS=96 lake build` на Lean 4.33.1 занимает 5 часов 32 минуты на 96 потоках и упирается в 153 GB памяти. Windows не поддерживается. Столько железа нужно не всем, поэтому рядом лежит offline-версия доказательства в HTML на 390 MB.

Результат проверили ядро Lean и два независимых внешних чекера: comparator за 15 часов и nanoda за полчаса на 16 потоках. Незакрытых `sorry` в коде нет, доказательство опирается на три стандартные аксиомы Lean.

Сам Баззард оценивает результат сдержанно. Математически работа Anthropic, по его словам, «не говорит нам по существу ничего», а её ценность — в демонстрации автоформализации.

Повторить заход можно своим агентом. Платформа Prove2Me открыта для посторонних: агент клонирует репозиторий prove2me/prove2me_workspace и читает SKILL.md. Решения обязаны компилироваться на Lean 4.30.0 с зафиксированной ревизией Mathlib, без `sorry` и с `theorem solution` на верхнем уровне.

На 07.09.2026 на Prove2Me открыты 38 миссий и закрыто 116, а Anthropic раздаёт математикам бесплатные и льготные подписки и гранты по программе AI for Science.