Claude и Великата теорема на Ферма: когато AI помага на компютъра да провери математиката
Claude помогна за пълна Lean формализация на Великата теорема на Ферма с 29 511 машинно проверими теореми.
Понякога най-важната роля на изкуствения интелект не е да измисли нов отговор, а да помогне да проверим стария възможно най-строго.
Anthropic обяви, че Claude е участвал в създаването на първата пълна формализация на Великата теорема на Ферма в Lean 4. Това е една от най-прочутите задачи в историята на математиката. Пиер дьо Ферма я записва през XVII век, а Андрю Уайлс публикува доказателството си през 90-те години на XX век след повече от три века търсене.
Новината не означава, че Claude е открил ново доказателство и не отменя работата на Уайлс. Разликата е във формата. Обикновеното математическо доказателство е текст, който експерти четат, обсъждат и проверяват. Формалното доказателство е преведено на език, при който специализиран софтуер може да провери всяка дефиниция и логическа стъпка.
Публичният проект използва Lean 4 и Mathlib. В хранилището са описани 29 511 теореми, нужни по целия път до крайното твърдение. Авторите посочват, че всичките 60 475 модула са компилирани от нулата и проверени от Lean kernel, а същата среда е приета и от nanoda — отделна реализация на Lean kernel. Това е важна техническа подробност: резултатът не се свежда до уверено твърдение на чатбот, а до артефакт, който може да бъде изтеглен и проверен.
Anthropic описва проекта като повече от 13 милиона реда код и като най-голямото Lean доказателство досега. Тези две оценки идват от самата компания. Публичното хранилище потвърждава наличието на пълна машинно проверима формализация и дава инструкции как тя да бъде възпроизведена.
Защо това има значение? Проверяването на сложни доказателства може да отнеме години работа от малък брой специалисти. Ако AI ускори формализирането, математиците могат по-бързо да откриват липсващи стъпки, скрити предположения и грешки. Това няма да премахне нуждата от човешка интуиция, но може да направи финалната проверка значително по-надеждна.
Истинският пробив тук не е „AI реши Ферма отначало“. По-точното и по-интересно твърдение е, че AI помогна едно гигантско човешко знание да бъде преведено във форма, която машина може да провери до последната логическа връзка.
