ИИ перевел доказательство Великой теоремы Ферма в код всего за 11 дней
Модель Claude формализовала доказательство Великой теоремы Ферма «в основном автономно» всего за 11 дней, сообщила компания-разработчик Anthropic. Полученный результат представляет собой 13 миллионов строк кода на Lean — специальном математическом инструментарии.
Великая теорема Ферма веками не давала покоя математикам, пока в 1995 году ее не доказал Эндрю Уайлс. Она гласит, что не существует таких целых чисел a, b и c, которые удовлетворяли бы уравнению aⁿ + bⁿ = cⁿ, где n — целое число больше 2.
Теорема, хоть и проста в формулировке, оказалась невероятно сложной для доказательства. Математик Пьер де Ферма сформулировал эту задачу еще в XVII веке и, как известно, намекал на найденное им доказательство, утверждая, что оно слишком велико, чтобы поместиться на полях учебника, где он делал свои записи.
Многие математики пытались найти доказательство и терпели неудачу. Уайлс работал над задачей семь лет втайне, прежде чем объявить о прорыве в 1993 году. Доказательства часто представляют собой длинные цепочки логических рассуждений, которые опираются друг на друга. Если на каком-то шаге закралась ошибка, все рушится. Именно это и случилось с Уайлсом, когда в его доказательстве нашли пробел, на устранение которого у него и его соавтора Ричарда Тейлора ушло около года.
Формализация математических теорем переносит их из области «бумаги и пера» в компьютерный код, что позволяет машинам работать с ними, шаг за шагом проверяя логику и выявляя любые изъяны. В центральном репозитории Mathlib уже хранится 2 миллиона строк формализованной математики.
Профессор Кевин Баззард из Имперского колледжа Лондона пять лет трудился над формализацией 100-страничного доказательства Уайлса и Тейлора на языке программирования Lean. В начале этого года он уже предполагал, что прогресс в ИИ поможет закончить эту работу гораздо быстрее.
Объявление Anthropic поставило точку в задаче. По приведенным в нем словам Баззарда, доказательство «не опирается ни на что, кроме аксиом математики». Проще говоря, проблема решена.
«Попутно мы видим автоматическую формализацию алгебры, гармонического анализа, геометрии и теории чисел, и понимаем, что артефакты автоформализации ИИ теперь достаточно надежны, чтобы их можно было использовать как основу; доказательство получилось многоуровневым. Если автоматическая формализация ВТФ возможна уже сейчас, значит, мы сделали большой шаг к автоматической формализации современной математической литературы», — сказал профессор.
По данным Anthropic, работу разделили на подзадачи, каждую из которых выполнял отдельный ИИ-агент. Время от времени им давали «общие указания», поскольку иногда агенты «теряли нить проекта и переставали эффективно взаимодействовать». Любопытно, что к прорыву привело внедрение инструмента Prove2Me, предназначенного изначально для сотрудничества живых математиков — он помогал разным агентам отслеживать свою работу и принимать решения о следующих шагах.
Формализация Anthropic насчитывает 13 миллионов строк кода на Lean и включает примерно 29 500 промежуточных теорем, которые стали необходимыми ступенями на пути к завершению всей работы. Таким образом, доказательство стало в пять раз больше по объему, чем все предыдущие работы в Mathlib, а также самым большим доказательством из когда-либо написанных на Lean.
