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