Anthropic Claude формализовала доказательство Великой теоремы Ферма
Компания Anthropic объявила о достижении, которое математическое сообщество считало делом не ближайших лет: исследовательская модель Claude формализовала доказательство Великой теоремы Ферма. Речь идет не о новом доказательстве, а о преобразовании уже существующего, созданного Эндрю Уайлсом в 1995 году, в формат, который способен проверить компьютер. Оригинальный труд занимает 129 страниц, и на его валидацию у экспертов уходят месяцы кропотливой работы. Теперь же эта проверка может стать вопросом чисто технической процедуры.
Формализованное доказательство — это код на языке программирования Lean, объем которого достиг 13 миллионов строк. Это самый крупный подобный проект в истории. Сложность задачи заключалась в том, что человеческие математические доказательства лаконичны: они опускают огромное количество логических связок, которые для человека очевидны, но для машины — нет. Каждый такой пропуск приходится восстанавливать вручную, а ошибка в одной строке способна обрушить всю последующую конструкцию, поскольку аргументы в доказательстве вытекают друг из друга.
Примечательна не только техническая возможность формализации, но и скорость. Математики прогнозировали, что на эту работу уйдут годы. Модель Anthropic справилась за 11 дней, используя ограниченный объем высокоуровневых данных. В процессе работы она запустила несколько десятков агентов, которые суммарно сгенерировали 6 миллиардов токенов и доказали 29 500 промежуточных теорем. Любопытно, что первая попытка провалилась — прорыв произошел лишь после того, как алгоритму открыли доступ к специализированной платформе Prove2Me.
Математик Кевин Баззард, чьи наработки легли в основу проекта, прокомментировал результат так: «Мы увидели автоформализацию алгебры, гармонического анализа, геометрии и теории чисел и поняли, что средства автоформализации теперь достаточно надёжны, чтобы с ними можно было работать; доказательство многоуровневое». Показательно, что это достижение стало вторым значимым успехом Anthropic за месяц: незадолго до этого компания добилась прогресса в работе над гипотезой Римана. Похоже, ИИ перестает быть просто инструментом для вычислений и начинает выступать в роли полноценного партнера в фундаментальной науке, беря на себя рутинную, но критически важную работу по проверке сложнейших логических построений.
