Великую теорему Ферма впервые проверила машина: Claude собрал доказательство за 11 дней

Проверял он 13 млн строк на языке Lean: столько кода Claude написал за 11 дней и закончил к 18 августа 2026 года. Объём больше всей Mathlib, главной библиотеки формальной математики, более чем в 5 раз.

Великая теорема Ферма была последним незакрытым пунктом в списке ста задач Фрика Видейка. Список закрывали 20 лет, последний пункт агент закрыл за 11 дней.

Работал не публичный Claude. Anthropic запускала внутреннюю исследовательскую модель, по её описанию примерно сопоставимую с Claude Fable 5.1, на харнессе поверх Claude Code. Люди вмешивались редко и по-крупному, подсказками уровня «якобиан как схема, высокий приоритет».

Цепочка вышла длинной: 29 500 промежуточных теорем в финальном доказательстве, 30 300 доказанных всего, около 6 млрд выходных токенов. Доказательство опирается только на три стандартные аксиомы Lean, а независимое ядро nanoda на Rust прогнало 1 052 234 объявления без единой ошибки.

Тот же путь снаружи. Формализацию ведут через платформу Prove2Me, её сделал Тяньи Пэн из Columbia University. Сама платформа бесплатна, платите только за подписку агента: одного плана Claude Max за $200 в месяц хватает примерно на целый учебник, недавние миссии стоили одну-две недели подписки. Знание Lean не требуется.

Вход в одну строку: вставить агенту «Fetch https://prove2.me/start.md and follow it to set up and register for me». Работают Claude, Codex, Cursor и OpenCode, подойдёт любой агент с доступом в сеть и к файлам. Три подписки Claude Max через Prove2Me формализовали теорему Виноградова о трёх простых за 3 дня.

Само доказательство Ферма Anthropic выложила открыто на GitHub, вместе с 390 МБ статического HTML для чтения без сети. Для сборки у себя нужны Lean 4.33.1 и Mathlib v4.33.0, Linux или macOS (на Windows пути слишком длинные), 67 ГБ диска. Полный `lake build` на 96 потоках идёт около 5,5 часа.

Список Видейка на этом закончился, а следующие формализации на Prove2Me идут уже на потребительских подписках.