Claude закрыл Ферма за 11 дней: 13,4 миллиона строк Lean и ни одного «очевидно»
4 сентября Anthropic показала первую в истории полную машинную проверку Великой теоремы Ферма. Claude за 11 дней, почти без помощи людей, перевёл доказательство Эндрю Уайлса в язык Lean: 13,4 миллиона строк кода, около 30 тысяч промежуточных теорем, ноль «очевидно из сказанного». Проект, который математики планировали на годы — только чертёж первой фазы у Кевина Баззарда из Имперского колледжа Лондона тянул на 86 страниц, — закрыт за полторы недели.
Сразу уточним, чего тут нет: нового доказательства нет. Модель не придумала собственный путь к теореме. Она сделала другое, и, честно говоря, не менее сложное — взяла человеческое доказательство, где на каждой странице встречаются оговорки вроде «отсюда тривиально следует», и переписала его так, что каждый шаг проверяет компилятор. Математики после 1995 года были уверены в теореме на 99,9%. Теперь можно на все сто: Lean прогнал весь вывод от трёх стандартных аксиом, и сомневаться больше не в чем.
Что именно проверил компьютер
Цифры тут уместнее эпитетов.
- 13,4 миллиона строк на Lean — в пять с лишним раз больше, чем вся Mathlib, главная библиотека формальной математики этой системы.
- Доказано около 30 тысяч промежуточных теорем; в финальном выводе задействовано примерно 29 500.
- Компиляция репозитория на 96-ядерной машине идёт примерно в 20 раз дольше, чем компиляция Mathlib. Баззарду на время проверки дали сервер с 500 ГБ оперативной памяти.
- Опора — только на три стандартные аксиомы Lean. Никаких «допущений для простоты».
Кевин Баззард — тот самый математик, который с 2024 года ведёт сообщества проект формализации Ферма — скачал репозиторий, собрал его и прогнал компаратор: формулировка теоремы на выходе совпадает с эталонной из Mathlib, все проверки зелёные. Его отзыв: «экстраординарное достижение автоформализации».
Одна строчка на полях, три с половиной века работы
Около 1637 года Пьер де Ферма приписал на полях «Арифметики» Диофанта утверждение: для n больше двух уравнение aⁿ + bⁿ = cⁿ не имеет решений в натуральных числах. Ниже — фраза, ставшая легендой: «Я нашёл поистине чудесное доказательство, но поля слишком узки для него». Поколения математиков от Эйлера до Куммера продвигались к результату кусками. В 1908-м за доказательство назначили премию в 100 тысяч золотых марок, и уже за первый год пришло 621 неверное решение.
В июне 1993-го Эндрю Уайлс представил своё доказательство в цикле лекций в Кембридже. Через два месяца рецензент задал вопрос, вскрывший дыру в одной из конструкций. Год Уайлс латал её — сначала в одиночку, потом вместе с бывшим студентом Ричардом Тейлором, — был на грани того, чтобы всё бросить, и в 1995-м опубликовал текст на 129 страниц. Оставался последний, «инженерный» вопрос: можно ли заставить компьютер подтвердить всё это целиком?
Не новое доказательство, а новая возможность
За основу взят разбор Дармона, Даймонда и Тейлора 1995 года — изложение аргумента Уайлса–Тейлора через теорему Ланглендса–Таннелла и спуск уровня Рибета. Идею формализовать Уайлса озвучивал ещё в 2000-е нидерландский информатик Ян Бергстра, но до недавних пор это считалось работой на целое научное направление. Отдельные случаи — четвёртая степень, регулярные простые — в Lean перенесли раньше. С новым репозиторием закрыт весь список Вейдика из 100 задач формализации: бенчмарку, по которому сверялась эта область, двадцать лет.
Баззард, кстати, честно пишет: математически работа не сообщает ничего нового — в Уайлса он и так верил. Ценность в другом. Проверка свежей статьи в математике тянется месяцами, а то и годами; если машину можно попросить формализовать доказательство «на лету», рецензирование сожмётся, а скрытые допущения уровня «известно экспертам» начнут всплывать. Для науки, где всё держится на честности выводов, это серьёзный сдвиг.
Как эти 11 дней выглядели изнутри
Руководил работой Тяньи Пэн — исследователь Anthropic, до этого собравший в Колумбийском университете группу инструментов ИИ-формализации. По его словам, дойти до конца он изначально не планировал: хотел лишь посмотреть, насколько Claude продвинет проект Баззарда. Продвинул до финала.
Работало много агентов параллельно: одни достраивали математические определения, другие штурмовали промежуточные леммы, третьи двигались вверх по дереву теорем, четвёртые собирали части обратно в единый вывод. Первые дни шли криво — агенты теряли общую картину проекта, и от ранних попыток в финальном коде осталось около семи процентов. Разворот случился, когда команду пересадили на платформу Prove2Me: доказательство в ней — граф из узлов-теорем, где видно, что уже доказано, что ждёт предпосылок и что брать следующим. Формулировки отделены от доказательств, компиляция ускорена, у каждой теоремы есть текстовое описание для поиска. Масштаб работы — около шести миллиардов выходных токенов, а человеческие подсказки сводились к высокоуровневым: «это направление приоритетнее».
Где посмотреть
Репозиторий выложен на GitHub — при желании проверку можно запустить самому, если найдётся машина со 96 ядрами и крепкие нервы. Первоисточники: разбор от Anthropic и пост Баззарда в блоге Xena Project.
А если после истории с 13 миллионами строк захочется посмотреть, как современные модели справляются с задачами поменьше — алгоритмами, кодом, расчётами, — загляните в разделы «Код» и «Чат» на NeuralSpace: там можно поэкспериментировать с моделями и подключить их к своим проектам через API.