ИИ проверил доказательство Великой теоремы Ферма из 13 миллионов строк кода
Суть в двух словах: Anthropic впервые получила полностью машинно-проверенное доказательство Великой теоремы Ферма, написанное агентами Claude.
Разбор по пунктам:
Что сделано. Сама теорема (уравнение xⁿ + yⁿ = zⁿ не имеет целочисленных решений при n > 2) доказана Эндрю Уайлсом ещё в 1995 году — человеческий математический факт давно не оспаривается. Не хватало формализации: перевода доказательства в код, который компьютер проверяет шаг за шагом. Рой агентов Claude сделал это за 11 дней в системе Lean: 13 млн строк кода, ~29 500 промежуточных теорем. Формализована упрощённая версия доказательства Уайлса (по Дармону—Даймонду—Тейлору), код выложен открыто, компилируется и проверяется любым желающим.
Почему это трудно. «Человеческое» доказательство опускает «очевидные» шаги и опирается на века публикаций; Lean требует явного кода для каждого шага, а формализована пока лишь малая часть математики. Эксперты закладывали на это годы — ср. проект Кевина Баззарда в Imperial College, профинансированный до 2029 года, чей черновик занимает 86 страниц.
Важные оговорки.
- Новой математики нет: это проверка старого доказательства, а не новое доказательство. Сам Баззард, посмотревший работу, говорит то же самое — но называет её большим шагом к автоматической формализации всей современной матлитературы.
- Успех — не заслуга одной модели. Первые попытки агентов провалились (теряли общую картину и переставали сработаться); прорыв дал переход на платформу Prove2Me (Колумбийский университет), которая ведёт граф утверждений и распределяет задачи между агентами. Т.е. ключевое — инфраструктура оркестрации, а не «умная модель сама по себе».
- Цена вопроса: ~6 млрд выходных токенов, по оценке статьи — 100–300 тыс. долларов.
Контекст. Статья ставит это в ряд похожих новостей (AlphaProof, разовый промпт GPT-5.4 Pro, решивший открытую задачу, опровержение 80-летней гипотезы моделью OpenAI) и напоминает, что баланс таких «КИ-успехов» смешаннее, чем заголовки. Независимой оценки работы Anthropic пока нет — есть только самопроверка Lean и компиляция у Баззарда.
Смысл для практики: доказательство — это, по сути, большой инженерный проект с верификацией, и ИИ-агенты впервые довели такой проект «под ключ» до состояния, где проверка не требует доверия к человеку — только к ядру Lean и его трём аксиомам.