Claude, модель Anthropic, за 11 днів роботи в агентному режимі сформулював формальний доказ Великої теореми Ферма мовою Lean — і зробив це, за словами компанії, майже без втручання людини. За даними Techmeme, це один з найамбітніших публічних тестів агентних можливостей Claude у сфері формальної верифікації математики.

Велика теорема Ферма — твердження, яке Ферма записав на полях книги 1637 року і яке не мало повного доведення 358 років, поки Ендрю Вайлз не опублікував доказ у 1994-му, спираючись на теорему модулярності еліптичних кривих. Сам доказ Вайлза займає сотні сторінок складної алгебричної геометрії. Перевести таку конструкцію в Lean — мову, де кожен крок мусить бути перевірений комп'ютером формально, без жодних логічних пропусків, — це окрема, самостійно важка інженерна задача, яка традиційно вимірюється роками роботи спільноти математиків, а не днями роботи одного агента.

Саме тому 11 днів — цифра, яка привертає увагу і водночас вимагає контексту: наскільки самостійним був процес, що саме довелося виправляти людям-рецензентам і чи витримає результат зовнішню перевірку lean-спільнотою.

Що саме зробила модель, за версією Anthropic?

За описом компанії, Claude сформулював (formalized) доказ теореми Ферма мовою Lean практично автономно за 11 днів роботи. Це означає, що модель самостійно вела ланцюжок формальних lean-тверджень (tactics/lemmas), які покроково відтворюють логіку математичного доказу так, щоб їх міг автоматично перевірити tactic-чекер Lean — без ручного написання коду людиною на кожному кроці.

Anthropic подає це як демонстрацію того, наскільки далеко зайшла агентна модель у довгих, багатокрокових задачах, де немає миттєвого фідбеку «правильно/неправильно» від людини, а є лише сам компілятор Lean, що приймає або відхиляє кожен крок.

Чому формалізація в Lean — це не те саме, що «розв'язати задачу»?

Формальна верифікація в Lean суворіша за звичайний математичний доказ на папері: кожне твердження треба звести до базових аксіом і вже перевірених лем, і жодна «інтуїтивно очевидна» деталь не проходить без явного обґрунтування. Це причина, чому формалізація готових доказів історично відстає від їх первинного відкриття на роки чи десятиліття.

Для контексту: ще 2024 року математик Кевін Баззард із Імперського коледжу Лондона публічно анонсував проєкт формалізації доказу Ферма в Lean, розрахований на роки колективної роботи спільноти математиків і розробників. Це не той самий проєкт, що згаданий Anthropic, але він добре ілюструє, яким є типовий людський таймлайн для задачі такого масштабу — і чому 11-денний автономний прогін одного агента виглядає різким відхиленням від норми.

Наскільки самостійним був цей прогін насправді?

Anthropic описує процес як такий, що відбувався «майже автономно» — формулювання, яке залишає простір для втручання людини на окремих етапах (постановка підзадач, перевірка проміжних лем, виправлення тупикових гілок). За нашою оцінкою, саме ступінь цього втручання — а не сам факт «Claude довів теорему Ферма» — стане головним предметом дискусії серед lean-розробників, коли вони отримають доступ до самого коду доказу.

Це той самий тип питання, що виникає навколо будь-яких довгих агентних прогонів: чим довша автономна сесія, тим складніше зовнішньому спостерігачу відстежити, де саме модель ухвалювала рішення, а де просто виконувала підказки з попередніх ітерацій. Схожу проблему прозорості нещодавно визнавала й OpenAI, коли заявила, що не може прочитати все мислення Astra під час довгих ланцюжків міркувань — і це загальна риса великих агентних систем, а не специфіка одного розробника.

Висновок AiiN

Наша теза: значення цієї новини не в тому, що «AI довів математичну теорему» — сам доказ Ферма існує з 1994 року і належить Ендрю Вайлзу, Claude лише переклав його логіку у формальну, машинно-перевірювану форму. Значення в іншому: якщо результат витримає незалежну перевірку lean-спільнотою, це буде перший публічний доказ того, що агентна модель здатна самостійно тримати в контексті багатотижневу формальну конструкцію без деградації якості на пізніх кроках. Для AI-білдерів, що працюють з довгими агентними ланцюжками, головний сигнал — не в математиці, а в тому, що межа «скільки кроків агент може протримати послідовно і коректно» зрушилася далі, ніж вважалося ще рік тому. Anthropic тим часом продовжує нарощувати ставки на подібні демонстрації на тлі власного зростання — компанія, що готується до IPO на $2 трильйони, зацікавлена показувати саме такі приклади агентної автономності.

Що таке формалізація доказу мовою Lean?

Формалізація — це переклад математичного доказу в мову, яку може механічно перевірити комп'ютерний асистент доведень, такий як Lean. На відміну від доказу «на папері», тут кожен крок зводиться до формальної логіки й перевіряється tactic-чекером, а не переконує читача-людину аргументацією.

Чи означає це, що AI тепер може самостійно доводити нові теореми?

Ні, в описі Anthropic йдеться саме про формалізацію вже відомого доказу Вайлза, а не про відкриття нового математичного результату. Це різні задачі: перша — інженерна перевірка існуючої логіки, друга — пошук нової математичної істини, і поки що новина стосується тільки першої.