Агенты Claude за 11 дней подготовили первую полностью проверенную компьютером версию доказательства Великой теоремы Ферма. Об этом 4 сентября рассказали в Anthropic.
Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat’s Last Theorem, one of… pic.twitter.com/pdT8zwlV4A
Великая теорема Ферма утверждает: равенство aⁿ + bⁿ = cⁿ невозможно для положительных целых чисел a, b и c при целом n больше двух. Пьер Ферма сформулировал это утверждение в 1637 году.
Результат касается формализации уже известного доказательства, опубликованного Эндрю Уайлсом в 1995 году. Claude перевел математические рассуждения в код, который система проверки доказательств Lean может проверить шаг за шагом.
Как работали агенты Claude
Эксперимент организовал исследователь Anthropic Тяньи Пэн, чья группа в Колумбийском университете разрабатывает инструменты формализации математики. Согласно техническому отчету , люди задали формулировку целевой теоремы и иногда указывали приоритеты.
Агенты самостоятельно записывали промежуточные утверждения, проверяли формулировки друг друга и строили доказательства.
Система использовала библиотеку Mathlib и материалы проектов Imperial College London FLT и flt-regular. В итоговом коде 106 файлов адаптированы из двух последних проектов с указанием авторства.
Координировать агентов помогла платформа Prove2Me. В статье ее разработчиков описан принцип совместной работы: большую задачу разбивают на связанные промежуточные утверждения, а участники добавляют доказательства и используют уже полученные результаты. Общая структура позволяет нескольким агентам работать параллельно.
По данным Anthropic, Claude доказал около 30 300 промежуточных теорем, из которых примерно 29 500 вошли в итоговую работу. Объем кода достиг 13 млн строк.
Компания назвала результат крупнейшим доказательством на Lean, уточнив, что код, вероятно, значительно длиннее необходимого.
В эксперименте использовали внутреннюю исследовательскую модель, примерно сопоставимую с Claude Fable 5.1. Работа потребовала около 6 млрд выходных токенов.
Как проверили результат
Полный код и инструкции для повторной проверки опубликованы на GitHub . Согласно документации, доказательство прошло проверку Lean и независимого проверяющего ядра nanoda. Инструмент comparator подтвердил соответствие итогового утверждения формулировке теоремы Ферма из Mathlib.
Авторы также установили, что доказательство использует только три стандартные аксиомы Lean и не содержит недоказанных заглушек. В репозитории уточняется: надежность результата предполагает доверие к проверяющим программам.
Математик Имперского колледжа Лондона Кевин Баззард, который ведет собственный проект формализации теоремы, отдельно подтвердил результат в своем блоге .
«Я скомпилировал кодовую базу и запустил на ней comparator — проверка прошла», — написал он.
Значение работы Баззард связал с возможностями автоматической формализации. По его мнению, такие инструменты помогут проверять научные статьи и выявлять пропуски в рассуждениях.
Исследователь продолжит собственный проект. Помимо формализации, его задачи включают пополнение Mathlib и создание документа, который позволит людям изучать современную версию доказательства. Claude работал с изложением более раннего подхода.
Напомним, в июле Claude Mythos Preview помог исследователям Anthropic найти криптоаналитические атаки на постквантовую схему подписи HAWK и сокращенную семираундовую версию AES-128. Результат по AES не относился к полной десятираундовой версии шифра.
Подписывайтесь на ForkLog в социальных сетях
