Модель Anthropic формализовала теорему Ферма в Lean

Внутренняя модель Anthropic за 11 дней собрала в Lean полное формальное доказательство Великой теоремы Ферма. Модель работала на платформе prove2.me, компания объявила результат 4 сентября. Теорема оставалась последней в списке Фрека Видейка из 100 задач на формализацию, и с ней этот бенчмарк, которому 20 лет, закрыт целиком.

Первой новость выложила в Instagram кофейня в Ислингтоне, официальное объявление Anthropic появилось часом позже. Так описывает события Кевин Баззард из Imperial College London, который сам формализует ту же теорему. В посте в блоге Xena Project на Wordpress он поздравляет Anthropic и разбирает, что именно сделала модель и чего она не делала.

Какое доказательство формализовали

Модель взяла изложение аргумента Уайлса и Тейлора - Уайлса, которое в 1995 году опубликовали Анри Дармон, Фред Даймонд и Ричард Тейлор. Оно идёт через теорему Ленглендса - Таннелла и теорему Рибета о понижении уровня. Проект Баззарда устроен иначе. Как сказано в репозитории проекта на GitHub, его маршрут почти целиком спланировал Ричард Тейлор: это современный вариант исходного доказательства, который многое берёт из идей Кхаре и Винтенберже.

В репозитории Anthropic развита теория Фонтена, которая нужна для изучения плоских деформаций представлений Галуа. Кроме того, там развито достаточно из работы Мазура об идеале Эйзенштейна, чтобы заключить, что у кривой Фрея не может быть точки нужного порядка. Кривую Фрея строят из гипотетического решения уравнения Ферма, и доказательство сводится к тому, что такой кривой быть не может.

Поэтому формализация Anthropic работает не для всех простых показателей. Остальные случаи закрывает более ранняя формализация для нечётных регулярных простых, её сделали Бест, Биркбек, Браска и Родригес. Наименьшее иррегулярное простое число равно 37, и Баззард заключает, что «всё в порядке».

13,4 млн строк на 96 ядрах

Баззард сам скомпилировал кодовую базу и прогнал на ней comparator. Проверка проходит. Доказательство занимает больше 13,4 млн строк и компилируется почти в 20 раз дольше, чем Mathlib, математическая библиотека Lean. Это на машине с 96 ядрами.

Такой объём объясняется устройством Lean. Каждый шаг рассуждения нужно записать на формальном языке, а потом его механически проверяет небольшое доверенное ядро. Абзац из человеческой статьи в Lean может растянуться на несколько страниц.

Работать с таким репозиторием тяжело даже на мощном железе. Anthropic дала Баззарду доступ к машине с 500 ГБ оперативной памяти, но и там Lean подтормаживает при переходах между файлами. Поэтому компания приложила HTML-документы, по которым, как пишет Баззард, на практике проще ориентироваться: репозиторий клонируют и открывают в браузере. Работу Баззард назвал «необычайным достижением автоформализации».

С первого раза не вышло

Получилось не сразу. Как рассказывает Tech Times, в начале августа Тяньи Пэн (Tianyi Peng), исследователь Anthropic, чья группа в Колумбийском университете делает инструменты для ИИ-формализации, решил проверить, сможет ли Claude продвинуться в этом проекте. Первую попытку он провёл на стандартной мультиагентной обвязке Claude Code, и она провалилась. Поначалу агенты продвигались, но потом потеряли из виду общее состояние проекта и перестали нормально работать вместе.

Итоговый результат получен уже на prove2.me. Баззард описывает исполнителя как «некий рой ИИ», который за 11 дней формализовал от начала до конца тысячи страниц математической литературы.

Что остаётся Баззарду

Проект Баззарда финансирует британский исследовательский совет EPSRC, как указано в репозитории проекта, до сентября 2029 года. Казалось бы, после новости работы у него не осталось. Сам он с этим не согласен. Работа Anthropic выполняет часть целей гранта и в объёме формализованного даже заходит дальше: EPSRC он обещал только свести теорему Ферма к результатам 1980-х, а в репозитории доказано всё целиком.

Но в заявке были и другие обещания. Первое - пул-реквесты в Mathlib с фундаментальными объектами современной теории чисел, эта работа продолжается. Второе Баззард считает, пожалуй, главным: динамический документ, по которому люди смогут разбираться в современном доказательстве. Он полагает, что Anthropic вряд ли за это возьмётся: свою задачу компания будет считать выполненной, да и современное доказательство она не формализовала.

Деньги и сроки Баззард сопоставляет сам. На свой проект он получил 1 млн фунтов на пять лет, Anthropic понадобилось 11 дней, «но интересно, не потратили ли они больше».

Математике как таковой работа, по его словам, «практически ничего не говорит». Баззард уверен в доказательстве теоремы Ферма на 99,9%, большинство специалистов по теории чисел уверены на все 100. Сам он из-за формализации стал подозрительнее к математической литературе, чем большинство коллег. Формализация, насколько он понимает аргумент, добросовестно повторяет ранние публикации и ничего к ним не добавляет.

Зато она показывает, чего уже можно добиться в автоформализации. Баззард ждёт, что в будущем современные исследования станут формализовать сразу по ходу работы. Заодно выяснится, обоснованы ли его сомнения в нынешнем состоянии программы Ленглендса: машины будут проверять аргументы и безжалостно отмечать неполные.

Рецензирование математических статей, по его мнению, станет намного менее мучительным. И честнее: есть статьи, которые опираются на результаты, «известные специалистам», и Баззарду любопытно, что именно предполагается в доказательствах важных теорем его области. Прецедент есть и у самой теоремы Ферма. Tech Times напоминает, что доказательство Уайлса 1995 года заняло 129 страниц, а пробел, найденный при рецензировании, Уайлс и Ричард Тейлор закрывали год.

Пост Баззард заканчивает историей. В 1993 году Уайлс объявил о доказательстве в Институте Ньютона в трёх лекциях. Баззард, тогда аспирант второго года, сходил на первую, ничего не понял, пропустил две следующие и уехал с новой девушкой в Ирландию. О том, что теорема доказана, он узнал через неделю, когда вернулся в Кембридж. Письмо Anthropic застало его на музыкальном фестивале Green Man в Уэльсе, с той же девушкой и почти без связи. Поймав на минуту 4G, он увидел письмо от незнакомого отправителя с темой «End-to-end Lean formalization of Fermat’s Last Theorem» и решил, что пишет фрик. Прочитал он его только через неделю, разбирая почти 1000 непрочитанных писем.