Claude за 11 дней подготовил доказательство математической задачи. Ее не могли решить 350 лет

Агенты 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

— Anthropic (@AnthropicAI) September 4, 2026

Великая теорема Ферма утверждает: равенство 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 не относился к полной десятираундовой версии шифра.

https://forklog.com/exclusive/ai/kak-ii-agenty-nauchilis-otravlyat-drug-druga