🤖 Claude за 11 дней формализовал теорему Ферма
Anthropic 4 сентября объявила о первом полном машинно-проверенном доказательстве последней теоремы Ферма: модель Claude почти автономно вела формализацию в Lean 11 дней. Итог — 13 млн строк кода Lean 4 и 29 500 промежуточных теорем; проверка — сборка 60 475 модулей, сверка с Mathlib и независимое ядро на Rust.
🌍 Задачу формализации FLT, которую с 2024 года вёл Кевин Базард в Imperial College London, считали чисто человеческой — LLM-агентный пайплайн закрыл её за 11 дней. Пока это единичная демонстрация без peer-review.
👤 Код открыт под Apache 2.0: 29 511 теорем можно читать офлайн в HTML с графом зависимостей, полная пересборка — около 5,5 часа на 96 потоках. Корректность проверяет ядро Lean, а не вера в лабораторию.
Источник 1: https://www.anthropic.com/news/formalizing-fermats-last-theorem Источник 2: https://github.com/anthropics/fermats-last-theorem