Lean прие доказателството на Claude за Ферма

Lean, софтуерът за проверка на доказателства, използван от математици по целия свят, прие пълна формална версия на последната теорема на Ферма. Формализацията е създадена от системата Claude на Anthropic и публикувана в отворено хранилище. В нея няма нерешени стъпки, оставени като временни заместители, допълнителни аксиоми или изчислителни съкращения извън стандартните основи на Lean (хранилище). Кевин Бъзард, математикът от Imperial College London, който ръководеше собствен проект за формализиране на теоремата, независимо компилира кода и потвърди, че проверката е успешна. Той определи резултата като „изключително постижение в автоматичната формализация“ (Бъзард).

Самият математически въпрос е решен отдавна. Андрю Уайлс доказва теоремата през 1995 г. и сред сериозните математици няма съмнения в резултата. Незавършена остава задачата доказателството да бъде пренаписано като инструкции за буквално следваща правилата машина, с всички определения и междинни стъпки, които авторът може да остави подразбиращи се. Според Anthropic десетки агенти с изкуствен интелект са извършили тази работа за единадесет дни през август, като са действали паралелно чрез платформа, наречена Prove2Me (Anthropic).

Този срок обаче се отнася до процес, който външни изследователи не могат да повторят. Вътрешният модел, инфраструктурата за координиране на агентите, решенията на операторите и вложените изчислителни ресурси не са част от публично достъпните материали. Възпроизводим е крайният резултат: всеки с достатъчно мощен хардуер може да компилира проекта в Lean и да потвърди, че доказателството издържа проверката. Отделна система за проверка, написана на Rust от Anthropic, е потвърдила същия формален продукт и съгласуваността на всичките 1 052 234 декларации (технически доклад). Това е втора проверка на един и същ текст, а не независимо възпроизвеждане на единадесетдневната работа.

Как са работили агентите

Формализирането на доказателство означава математическият аргумент да бъде пренаписан така, че програма без математическа интуиция да може да потвърди всяка логическа стъпка. Самата теорема звучи просто: при всеки цял показател, равен или по-голям от три, не съществуват три положителни цели числа, за които aⁿ + bⁿ = cⁿ. Доказателството обаче преминава през сложни области на теорията на числата и заема стотици страници.

Claude не е открил нова математика. Системата е формализирала вече установената поредица от резултати, водеща до доказателството на Уайлс, като е следвала изложение на математиците Анри Дармон, Фред Даймънд и Ричард Тейлър (Anthropic, технически доклад). Творческият пробив принадлежи на Уайлс и неговите предшественици. Приносът на Claude е превръщането му в около 10,5 млн. реда код, който може да бъде проверен от машина (технически доклад).

Платформата Prove2Me, разработена от изследователя на Anthropic Тиани Пън и негови сътрудници от Columbia University, е разделила доказателството на граф от около 29 511 взаимозависими и самостоятелно формулирани твърдения (технически доклад). Агентите са избирали твърдения, за които необходимите предходни стъпки вече са били готови, писали са доказателства в Lean и взаимно са проверявали предложените формулировки. Паралелната работа е изразходвала около шест милиарда изходни токена от вътрешен изследователски модел (технически доклад).

По данни на Anthropic човешките оператори не са писали код на Lean по време на изпълнението. Те обаче са избрали теоремата, предоставили са известния път към доказателството, проектирали са инфраструктурата за агентите и понякога са променяли приоритетите (Anthropic). Пълният запис на действията им и разходите за изчислителни ресурси не са публикувани.

Върху основа, градена от хора с години

Резултатът зависи от Mathlib, голямата библиотека с формализирана математика, поддържана от общност, и използва пряко материали от два по-ранни проекта. От края на 2023 г. екипът на Бъзард в Imperial работи по формализация на последната теорема на Ферма в Lean с финансиране от 1 млн. британски лири по грант на EPSRC, планиран до 2029 г. (грант на EPSRC). Друг общностен проект вече е формализирал теоремата за част от възможните случаи. Файлът на Anthropic за произхода на използваните материали посочва 106 файла, които съдържат съдържание, взето или адаптирано от тези начинания (източници).

Паралелното изпълнение прави единадесетте календарни дни несъпоставими с човешкия труд, вложен от екипа на Бъзард. Когато работата на Claude започва, проектът му вече се финансира от около 22 месеца (грант на EPSRC). Anthropic не е обявила нито броя часове работа на графичните процесори, нито потреблението на енергия.

Преди тази публикация последната теорема на Ферма е последният неформализиран резултат в списъка на Фрек Вейдейк със 100 важни теореми. Този показател проследява напредъка във формализацията от две десетилетия (Бъзард).

По-сериозната проверка за приложимостта на метода ще бъде формализирането на по-нова и по-слабо документирана математика, за която липсват готов план, развити библиотеки и предишна формална работа. В този случай е избрана известна теорема със значителна вече изградена инфраструктура. Резултатът показва, че при известен път към доказателството и налична предходна работа агенти с изкуствен интелект могат да създадат пълна формализация, която Lean приема, а външни изследователи могат да проверят. От публикуваните материали обаче самият процес на създаването ѝ не може да бъде възпроизведен.