Anthropic представила полное компьютерно проверенное доказательство Великой теоремы Ферма. Несколько десятков агентов Claude перевели существующее математическое доказательство на язык Lean за 11 дней.
Lean — это система, которая проверяет каждый логический шаг. Агенты написали около 13 млн строк кода и доказали 30,3 тыс. промежуточных теорем. В итоговой работе использованы 29,5 тыс. из них.
Результат проверил Кевин Баззард, математик Имперского колледжа Лондона и один из сопровождающих библиотеки Mathlib. С 2024 года он руководит отдельным пятилетним проектом по формализации той же теоремы, получившим грант на £1 млн. Баззард самостоятельно собрал код Anthropic и запустил стандартную проверку Lean.
Это не новое доказательство и не математическое открытие. Работа следует изложению доказательства Эндрю Уайлса, опубликованному в 1995 году Анри Дармоном, Фредом Даймондом и Ричардом Тейлором. По словам Баззарда, формализация точно воспроизводит известную литературу и ничего не добавляет к самой математике.
Первый запуск агентов провалился. Они потеряли представление о состоянии проекта и перестали согласовывать работу. Проблему решила платформа Prove2Me, созданная исследователем Anthropic Тяньи Пэном и его коллегами из Колумбийского университета. Она хранит граф теорем, разделяет формулировки и доказательства для быстрой сборки и добавляет к ним понятные текстовые описания.
Anthropic сообщила, что агенты сгенерировали около 6 млрд выходных токенов. По публичной цене сопоставимой модели это соответствовало бы $300 тыс., хотя реальные внутренние расходы компании неизвестны.
Баззард также проверил, не использовали ли агенты уязвимость Lean. Подозрительных обходов он не нашёл и назвал такой сценарий крайне маловероятным.
Теперь узкое место переместилось с написания доказательств на их проверку людьми. Mathlib пока не принимает рецензии от ИИ, а в очереди проекта уже более 600 активных запросов на добавление кода. Все 13 млн строк Anthropic остаются за пределами основной математической библиотеки.
