Машины проверяют математику: что значит формализация Великой теоремы Ферма

Есть особый вид тщеславия у математиков: доказать теорему — это одно, а убедить весь мир, что доказательство верно, — совсем другое. Эндрю Уайлс закрыл Великую теорему Ферма в 1995 году, после почти четырёхсот лет попыток и одного громкого провала годом ранее, когда в первой версии доказательства нашли дыру. С тех пор текст Уайлса читали, перепроверяли, преподавали на аспирантских курсах — но полностью формально, шаг за шагом, машиной его никто не верифицировал. Теперь этим занялись в Anthropic вместе с проектом Xena, который давно специализируется на переводе сложной математики на язык формальных доказательств.

Сама новость пришла с двух сторон: исследовательская заметка Anthropic и пост в блоге Xena project, где математики, участвующие в работе, описывают процесс изнутри. Это существенно, потому что задача — не переоткрыть доказательство и не найти в нём ошибку. Оно давно признано верным сообществом теоретиков чисел. Цель другая: закодировать рассуждение Уайлса (и последующие упрощения, сделанные другими математиками) в системе формальной верификации так, чтобы каждый логический шаг был проверяем компьютером без пробелов, без «это очевидно» и без доверия к репутации автора.

Почему это трудно

Доказательство Уайлса — не короткая элегантная выкладка на одну страницу. Оно опирается на модулярные формы, эллиптические кривые, гипотезу Таниямы-Шимуры-Вейля (тогда ещё гипотезу, теперь теорему) и целый аппарат алгебраической геометрии, который сам по себе строился десятилетиями. Формализовать такое — не значит просто «перевести с английского на язык программирования». Нужно сначала формализовать саму теорию, на которой доказательство держится: определения, леммы, вспомогательные теоремы, которые в обычных учебниках воспринимаются как данность.

Именно поэтому в этой работе участвует Xena project — многолетняя инициатива по формализации современной математики в системе Lean. Её участники годами переводили в машиночитаемый вид куски алгебры, теории чисел, топологии — и постепенно выстраивали фундамент, на который теперь можно опереться. Без этой подготовительной работы браться за Ферма было бы почти невозможно: пришлось бы формализовать полматематического образования с нуля.

Роль моделей Anthropic

Участие Anthropic в проекте — это не благотворительность в сторону чистой математики, а испытание собственных моделей на задаче, где ошибка видна сразу и без всяких оговорок. Формальная верификация — редкий случай, когда результат работы модели можно проверить механически: либо доказательство прошло тайпчекер, либо нет, третьего не дано. Это выгодно отличается от большинства бенчмарков, где качество ответа модели оценивают люди, часто субъективно. Здесь же компьютер либо принимает цепочку логических шагов, либо отвергает её.

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

Зачем вообще формализовывать то, что уже доказано

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

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

Что дальше

Процесс далёк от завершения — судя по тому, как построена подобная работа в прошлом, формализация такого объёма материала занимает месяцы, если не годы, и требует постоянной сверки между математиками-людьми и инструментами. Но сам факт, что за задачу такого масштаба взялись всерьёз, а не в качестве демонстрационного трюка, говорит о смене фазы. Формальная верификация долго существовала на периферии математической культуры — как занятие для тех, кто любит доказывать, что дважды два четыре, с абсолютной строгостью. Сейчас она подбирается к центру дисциплины, к результатам, которые определили математику XX века.

Если формализация доказательства Уайлса будет доведена до конца, это не изменит статус теоремы Ферма — она останется доказанной так же, как была доказана в 1995 году. Но изменится то, с какой степенью уверенности мы можем об этом говорить: не «доказательство прочитали и одобрили эксперты», а «каждый логический шаг проверен машиной, не способной на снисходительность». Для математики, которая веками держалась на доверии к авторитету и коллективной проверке, это не косметическое, а довольно глубокое изменение правил игры.