Математику заплатили за доказательство Ферма вручную, а он говорит, что Claude справился за 11 дней

У математика есть пятилетний грант на формализацию Великой теоремы Ферма. За него это сделали за одиннадцать дней, и он говорит, что этот результат ничего не сообщает нам о математике.

Компания Anthropic опубликовала доказательство в пятницу. Десятки агентов Claude написали 13 миллионов строк кода на Lean и доказали 30 300 промежуточных теорем. 29 500 из них они использовали в полном, проверенном компьютером доказательстве гипотезы, которую Пьер де Ферма набросал на полях около 1637 года.

Кевин Баззард (Kevin Buzzard) из Имперского колледжа Лондона с 2024 года руководил общественным проектом по формализации той же теоремы при финансовой поддержке Британского совета по исследованиям в области инженерии и физических наук (EPSRC). Он самостоятельно скомпилировал код Anthropic и запустил на нем стандартный инструмент проверки. Затем он описал это в своем блоге под заголовком «Anthropic опередила меня».

Что он сказал об этом на самом деле

Вердикт Баззарда четко делится на две части, однако большинство новостных ресурсов осветили лишь первую.

Что касается математики: она не меняется никак. Он оценивает вероятность того, что доказательство Уайлса верно, в 99,9%, и говорит, что большинство специалистов по теории чисел дают все 100%. По его словам, формализация «просто добросовестно следует ранней литературе по доказательству и ничего не добавляет».

Что касается того, что это демонстрирует, в другом вопросе он категоричен. ИИ-рой только что от начала и до конца формализовал тысячи страниц литературы за одиннадцать дней. Если теперь это возможно, написал он, формализация современных исследований начнет происходить на лету.

Он добавил одну фразу, которую не опубликует ни один пресс-релиз. Ему выделили 1 миллион фунтов стерлингов на пятилетний проект. Anthropic справилась за одиннадцать дней, и он задается вопросом, не потратили ли они больше.

Арифметика этого вопроса

В Anthropic заявляют, что на этот прогон ушло около шести миллиардов выходных токенов. Они были получены от внутренней исследовательской модели, которую описывают как примерно сопоставимую с Claude Fable 5.1.

Fable 5.1 стоит 50 долларов за миллион выходных токенов — ту же цену Anthropic установила в сентябре. Шесть миллиардов выходных токенов по этому тарифу составляют 300 000 долларов.

Это скорее иллюстрация, чем реальные затраты. Модель была внутренней, поэтому никто не выставлял счета, а собственные расходы компании на инференс ниже прейскурантных. Тем не менее, это единственная доступная публичная арифметика, и она сопоставляется с пятилетним грантом в 1 миллион фунтов.

Первая попытка провалилась

Anthropic на удивление откровенна в этом вопросе, и это самая полезная часть публикации.

Сначала агенты делали успехи, но затем потеряли понимание текущего состояния проекта и прекратили сотрудничество. Те неудачные запуски все равно внесли свой вклад — около 7% строк кода, не являющихся шаблонными, вошли в итоговое доказательство.

Проблему решила не более совершенная модель. Ею стала Prove2Me — открытая платформа, созданная исследователем Anthropic Тяньи Пэном (Tianyi Peng) в сотрудничестве с Колумбийским университетом. Она поддерживает граф утверждений теорем, чтобы агенты могли видеть, к чему приступить дальше. Она разбивает утверждения и доказательства на отдельные файлы для ускорения компиляции. Кроме того, она сохраняет описание каждого утверждения на естественном языке, благодаря чему можно находить и повторно использовать наработки.

Добавьте к этому мультиагентную обвязку на базе Claude Code, и те же модели завершили работу менее чем за две недели.

Мы утверждали два дня назад, что именно инфраструктура вокруг модели теперь определяет ее достижения. Вот тот же урок с другой стороны, озвученный самой лабораторией. Те же агенты, те же веса, неудача, а затем успех — и все это при единственной переменной в виде платформы координации.

Человеческий вклад свелся к двум предложениям

Инструкции Пэна рою, как сообщает Anthropic, сводились к обрывкам фраз. «Якобиан как схема звучит как высокий приоритет». «Добейтесь скорейшего завершения работы с Мазуром».

Доказательство следует изложению аргумента Уайлса 1995 года, сделанному Дармоном, Даймондом и Тейлором. Это не тот современный путь, который формализовал Баззард. Здесь используются лишь три стандартные аксиомы Lean, а компаратор подтвердил, что доказываемая им теорема совпадает с утверждением в Mathlib — математической библиотеке сообщества.

При объеме в 13 миллионов строк код более чем в пять раз превышает размер самой Mathlib. Баззард намерил 13,4 миллиона строк и говорит, что на 96-ядерном компьютере компиляция занимает почти в двадцать раз больше времени.

Он занялся поисками мошенничества

В Lean недавно были обнаружены ошибки корректности, и достаточно целеустремленный агент в принципе мог бы воспользоваться одной из них, чтобы доказать что угодно. Баззард проверил это.

Он попросил агента пометить каждую строку репозитория, которая не являлась определением или доказательством. Вернулось около 100 строк, и он их изучил. В них определялся вспомогательный тактический прием. Он также сообщает, что модели OpenAI изучили кодовую базу Lean и не нашли никаких проблем с корректностью в использованной версии.

Его собственное резюме таково: вероятность того, что задача была решена с помощью какого-то хака, крайне мала, и код явно развивает математику, необходимую для доказательства.

Узкое место сместилось, а не исчезло

В нынешнем виде ни одна из этих 13 миллионов строк не может попасть в Mathlib.

Баззард, являющийся мейнтейнером Mathlib, говорит, что библиотека в настоящее время не принимает обзоры ИИ. Рецензенты также неохотно берутся за рецензирование сгенерированного ИИ кода, поскольку большинство поступающих от ИИ материалов имеют низкое качество. В репозитории уже около 3 000 открытых пулл-реквестов, причем более 600 из них активно ожидают проверки.

Таким образом, ограничение сместилось с написания доказательств на их чтение. Это ровно та проблема, которую, по словам Anthropic, решает формализация, поднимаясь на один уровень выше.

Кроме того, у Баззарда по-прежнему есть работа. Его грант обязывает его передать фундаментальную теорию чисел в Mathlib и создать документ, позволяющий людям исследовать современное доказательство. Он сомневается, что Anthropic займется последним.

Как это соотносятся с остальными событиями года

В августе мы сообщали об аргументах Тимоти Гауэрса (Timothy Gowers) о том, что прорывы в математике ИИ, о которых все говорят, — это контрпримеры, а не доказательства. Полное проверенное машиной доказательство — это иной объект, и именно его появление упомянутый аргумент отрицал.

Кроме того, это не новая математика — именно на этом различии настаивает Баззард. В августе OpenAI заявила, что Astra решила десять открытых проблем. В июле Claude обнаружил изъяны в двух криптографических алгоритмах, которые экспертная проверка упустила из виду. То были заявления об открытиях. Это же заявление о верификации, а верификация — более легкая половина задачи.

Еще одно число из той же публикации. Три исследователя, использовавшие личные подписки на Claude, формализовали теорему Виноградова о трех простых числах за три дня.

Баззард узнал о результатах по Великой теореме Ферма с опозданием. Он находился на музыкальном фестивале с плохой связью. От незнакомца пришло письмо под названием «Сквозная формализация Великой теоремы Ферма в Lean», и он списал отправителя со счетов как чудака.