[ad_1]
Агенты Claude за 11 дней подготовили первую полностью проверенную компьютером версию доказательства Великой теоремы Ферма. Об этом 4 сентября рассказали в Anthropic.
Результат касается формализации уже известного доказательства, опубликованного Эндрю Уайлсом в 1995 году. Claude перевел математические рассуждения в код, который система проверки доказательств Lean может проверить шаг за шагом.
Эксперимент организовал исследователь 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.
[ad_2]
Источник
