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

Внутренняя модель Anthropic, работавшая через платформу prove2.me, собрала в Lean полное доказательство Великой теоремы Ферма и закрыла последний открытый пункт в списке Фрека Видейка из 100 задач на формализацию. Компания объявила об этом официально, разбор результата опубликовал блог Xena Project на Wordpress; часом ранее новость появилась в Instagram кофейни в Ислингтоне.

Коротко

• Формализовано изложение Дармона, Даймонда и Тейлора 1995 года для аргумента Уайлса, Тейлора и Уайлса: через теорему Ленглендса и Таннелла и теорему Рибета о понижении уровня, с теорией Фонтена в основании.
• Кодовая база превышает 13,4 млн строк и компилируется почти в 20 раз дольше математической библиотеки Lean на машине с 96 ядрами; автор блога прогнал на ней comparator, результат сходится.
• Проект автора блога по той же теореме идёт по гранту EPSRC в 1 млн фунтов на пять лет и обещает лишь сведение теоремы к результатам 1980-х, тогда как репозиторий доказывает её целиком.

Ценность события лежит не в математике: доказательство теоремы Ферма в сообществе теории чисел под сомнение не ставят. Показателен масштаб операции: тысячи страниц литературы, переведённые в машинно проверяемый код за одиннадцать дней, выглядят как заявка на то, что автоформализация современных работ перестаёт быть умозрительной перспективой. Для практики рецензирования и для проверки того, что в статьях принимается на веру, это, вероятно, значит больше, чем для самой теоремы.

В основе лежит изложение Дармона, Даймонда и Тейлора 1995 года

Anthropic формализовала не современный вариант доказательства, а изложение Дармона, Даймонда и Тейлора 1995 года для аргумента Уайлса, Тейлора и Уайлса. Путь идёт через теорему Ленглендса и Таннелла и теорему Рибета о понижении уровня; современное доказательство вслед за идеями Хара и Тейлора автор блога формализует сам.

В репозитории развита теория Фонтена, нужная для изучения плоских деформаций галуа-представлений, и часть работы Мазура об эйзенштейновом идеале. Второе даёт заключение, что у кривой Фрея не может быть точки соответствующего простого порядка. Именно на этом шаге доказательство теряет часть показателей: оно работает не для всех простых.

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

Кодовая база превышает 13,4 млн строк, а формализация заняла 11 дней

Автор блога скомпилировал кодовую базу и прогнал на ней comparator: проверка сошлась. Объём превышает 13,4 млн строк, а сборка на машине с 96 ядрами занимает почти в 20 раз больше времени, чем компиляция математической библиотеки Lean. Вычислительные ресурсы для проверки предоставила Anthropic, вся формализация заняла у компании 11 дней.

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

Об окончании работы автор узнал с недельной задержкой: письмо с темой «End-to-end Lean formalization of Fermat's Last Theorem» пришло, когда он был на фестивале Green Man в Уэльсе, и он принял неизвестного отправителя за чудака. Новость он прочитал только через неделю, разбирая около тысячи накопившихся писем.

Математически работа ничего не добавляет, считает автор Xena Project

Формализация, как он пишет, точно следует ранней литературе о доказательстве и ничего к ней не прибавляет. Он и раньше говорил, что уверен в корректности доказательства Ферма на 99,9%; большинство специалистов по теории чисел, по его словам, уверены в нём полностью, а его собственная осторожность связана с опытом формализации.

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

Чего в работе Anthropic нет

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