ИИ Anthropic формально доказал Великую теорему Ферма на Lean

Математик Кевин Баззард, ведущий проект Xena по формализации математики, сообщил в своём блоге: одна из внутренних моделей Anthropic на платформе prove2.me построила полную формализацию доказательства Великой теоремы Ферма (FLT) на языке Lean. Тем самым закрыт последний, остававшийся неприступным пункт знаменитого списка Фрика Видейка из ста формализационных задач — бенчмарка, которому уже двадцать лет.

Что именно доказано

Модель формализовала не «современное» доказательство, над которым работает сам Баззард, а классическую версию — изложение Дармона, Даймонда и Тейлора 1995 года аргумента Уайлса—Тейлора, через теорему Ленглендса—Таннелла и теорему Рибета о понижении уровня. В репозитории развита теория Фонтэна и достаточная часть работ Мазура об идеале Эйзенштейна. Формально доказательство работает для простых p ≥ 5, но это не пробел: для нечётных регулярных простых FLT уже была формализована ранее (Best—Birkbeck—Brasca—Rodriguez), а наименьшее нерегулярное простое — 37. Так что все случаи покрыты.

Масштаб впечатляет: свыше 13,4 миллиона строк кода, компиляция почти в двадцать раз дольше, чем у математической библиотеки mathlib, — даже на машине с 96 ядрами и 500 ГБ оперативной памяти. Баззард лично собрал код, прогнал верификатор comparator — сходится.

Работа не окончена

Сам Баззард финансируется грантом EPSRC (миллион фунтов на пять лет) именно на формализацию FLT, и первая мысль — что делать теперь ему нечего. Но это не так. Anthropic формализовала старое доказательство целиком; учёный же обещал грантодателю иное: во-первых, вносить в mathlib фундаментальные объекты современной теории чисел, во-вторых — и это важнее — создать «живой документ», позволяющий людям исследовать современное доказательство. Едва ли Anthropic возьмётся за это: для них задача выполнена.

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

В комментариях приводят любопытную цифру: по заявлению Anthropic, доказательство обошлось в 6 миллиардов выходных токенов — около 300 тысяч долларов по тарифам API. Сам Баззард иронично замечает: ему дали миллион на пять лет, компания уложилась в одиннадцать дней, но, вероятно, потратила больше.

Завершает он личным анекдотом: о доказательстве Уайлса в 1993 году он узнал с опозданием, уехав в отпуск в Ирландию; и теперь письмо от Anthropic застало его на музыкальном фестивале в Уэльсе — послание с темой «End-to-end Lean formalization of Fermat's Last Theorem» он поначалу принял за спам от чудака.

Источник: Lobsters