Агенты Claude за 11 дней формализовали доказательство Ферма
Anthropic сообщила 4 сентября, что агенты Claude за 11 дней подготовили первую полностью проверенную компьютером формализацию доказательства Великой теоремы Ферма в системе Lean.
Anthropic объявила 4 сентября, что искусственные агенты Claude за 11 дней подготовили первую полностью проверенную компьютером формализацию доказательства Великой теоремы Ферма, основанную на доказательстве Эндрю Уайлса 1995 года. Работа перевела математическое рассуждение в проверяемый код для системы доказательств Lean.
Эксперимент возглавлял исследователь Anthropic Тяньи Пэн. Люди задали целевую формулировку теоремы и иногда приоритеты; агенты разделяли задачу на промежуточные утверждения, формулировали леммы и строили доказательства. Для проверки шагов использовались библиотека Mathlib и материалы проектов Imperial College London FLT и flt-regular. Координацию нескольких агентов обеспечивала платформа Prove2Me, которая позволила параллельную работу над связанными утверждениями.
Итоговый набор кода занимает около 13 миллионов строк и состоит из 106 файлов, адаптированных из указанных проектов с сохранением авторства. По данным Anthropic, агенты сгенерировали примерно 30 300 промежуточных теорем, из которых около 29 500 вошли в окончательную формализацию. Эксперимент потребовал примерно 6 миллиардов выходных токенов и использовал внутреннюю исследовательскую модель, сопоставимую по возможностям с Claude Fable 5.1.
Полный код и инструкции для повторной проверки опубликованы на GitHub. Доказательство прошло автоматическую проверку в Lean и проверку независимым ядром nanoda; инструмент comparator подтвердил соответствие итогового утверждения формулировке из Mathlib. В репозитории указано, что в формализации использованы только три стандартные аксиомы Lean и не выявлено незавершённых заглушек. Документация отмечает, что надёжность результата зависит от доверия к проверяющим программам.
Кевин Баззард из Имперского колледжа Лондона в своём блоге указал, что скомпилировал кодовую базу и запустил comparator; проверка прошла. Он также описал практическое применение автоматической формализации для проверки научных статей и поиска пропусков в рассуждениях и сообщил о продолжении собственной работы по формализации и пополнению Mathlib.
В июле Anthropic уже использовала агенты Claude для помощи в поиске криптоаналитических атак на отдельные версии криптографических схем, что отражает предыдущие эксперименты с применением моделей к задачам формализации и анализа.
Материалы на GNcrypto предоставляются исключительно в информационных целях и не являются финансовой рекомендацией. Мы стремимся публиковать точные и актуальные данные, однако не можем гарантировать их абсолютную достоверность, полноту или надёжность. GNcrypto не несёт ответственности за возможные ошибки, упущения или финансовые потери, возникшие вследствие использования данной информации. Все действия вы совершаете на свой страх и риск. Всегда проводите собственный анализ и консультируйтесь с профессионалами. Подробнее см. в наших страницах Условия, Политика конфиденциальности и Отказ от ответственности.
Статьи этого автора
