4 сентября 2026 г.
Великую теорему Ферма проверила машина: Claude написал 13 млн строк на Lean
Anthropic выложила на GitHub формальное доказательство великой теоремы Ферма: Claude собрал его за 11 дней вместо проекта, рассчитанного до 2029 года.
Anthropic
@anthropicai
Проверить, что крупное математическое доказательство верно, можно годами. Помогает формализация: математическое рассуждение переводят в форму, которую умеют проверять компьютерные пруф-ассистенты вроде Lean. В прошлом месяце Claude завершил первое формальное доказательство великой теоремы Ферма, одной из самых знаменитых теорем в истории. Эксперты считали, что на такой проект уйдут годы. Это самое большое доказательство, когда-либо написанное на Lean. Впервые великую теорему Ферма доказал сэр Эндрю Уайлс в 1995 году, больше чем через 350 лет после того, как её сформулировали. Наше доказательство занимает свыше 13 миллионов строк кода и даёт машинную проверку. Важнее другое: попутно оно доказывает больше 29 000 теорем, которые для него нужны, во многих областях математики, которые раньше никто не формализовал. Мы считаем это важным шагом долгого пути к укреплению ядра математического знания, и он опирается на три века работы математиков и на сотни людей, вложившихся в Lean и Mathlib. Мы смотрим с оптимизмом: проверка доказательств с помощью ИИ снизит нагрузку на рецензирование в математике, а доказательств сейчас выходит больше, чем когда-либо. О том, как всё было устроено, можно прочитать в нашем научном блоге: https://www.anthropic.com/research/formalizing-fermats-last-theorem А полное доказательство лежит на GitHub: https://github.com/anthropics/fermats-last-theorem
· 114 тыс. просмотров
Великую теорему Ферма теперь проверяет машина. Claude собрал формальное доказательство за 11 дней.
Ручной проект формализации под руководством Кевина Баззарда из Imperial College London шёл с 2024 года и планировался минимум до 2029-го. Машинная версия открыта 04.09.2026.
Что именно проверено. Ядро Lean 4.33.1 собрало все 60 475 модулей доказательства. Comparator сверил формулировки с библиотекой Mathlib, а сторонний Rust-кернел nanoda 0.4.13 прогнал 1 052 234 декларации без ошибок. Аксиом всего три стандартных: propext, Classical.choice, Quot.sound.
Размер работы: 13 млн строк Lean, впятеро больше всей библиотеки Mathlib. По дороге доказано 30 300 теорем и определений, 29 500 из них вошли в финальную цепочку. Claude писал 11 дней и потратил около 6 млрд токенов на выходе, причём работала не публичная модель, а внутренняя research-версия, которую Anthropic называет примерно сопоставимой с Claude Fable 5.1.
Посмотреть можно сегодня. Репозиторий anthropics/fermats-last-theorem открыт под Apache 2.0: клон и lake build воспроизводят проверку на Linux или macOS за 5,5 часа при 96 потоках, под .lake нужно 67 ГБ диска. Без сборки доказательство читается офлайн, в репозитории лежит папка html на 390 МБ с 29 511 страницами теорем и разбором всего доказательства текстом.
Агентов координировала платформа Prove2Me Тяньи Пэна и коллег из Columbia. Она держит DAG формулировок теорем и ищет готовые теоремы по описанию обычными словами, открыта на prove2.me. Через неё теорему Виноградова о трёх простых формализовали за три дня на трёх личных подписках Claude Max.
Баззард, внешний рецензент работы, формулирует итог так: если автоматическая формализация теоремы Ферма возможна уже сейчас, значит сделан большой шаг к автоматической формализации всей современной математической литературы.
Anthropic открыла математикам гранты и research credits на формализацию следующих теорем.
Первоисточник