Як Claude, за повідомленням Anthropic, формалізував Велику теорему Ферма в Lean за 11 днів

Не нове доведення, а формалізація відомого

Anthropic повідомляє, що Claude створив перше повне наскрізне машинно перевірене формальне доведення Великої теореми Ферма (FLT) мовою Lean. Важливе уточнення: Claude не відкрив нового доведення теореми. Система переклала вже відомий сучасний шлях доведення на формальну мову, де кожен крок може механічно перевірити ядро Lean. За даними Anthropic, робота тривала близько 11 днів і дала приблизно 13 млн рядків коду Lean. 215

Велика теорема Ферма стверджує: для натуральних чисел і показника степеня (n \geq 3) рівняння (a^n+b^n=c^n) не має нетривіальних розв’язків. У бібліотеці Mathlib це записано еквівалентно: якщо такий розв’язок існує, то принаймні одне з чисел (a), (b) або (c) дорівнює нулю. 31

Проєкт ішов за викладом Дармона—Даймонда—Тейлора, що спирається на стратегію Вайлса / Тейлора—Вайлса, а не шукав принципово інший математичний маршрут. Подібний сучасний варіант цього підходу описував і проєкт формалізації FLT в Імперському коледжі Лондона. 511

Чому знадобилося 13 млн рядків

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

Anthropic повідомляє, що в процесі було отримано приблизно 30 300 комп’ютерно перевірених теорем; близько 29 500 з них увійшли до фінального ланцюга залежностей. Формалізація охоплює алгебру, геометрію, гармонічний аналіз і теорію чисел. 215

Тому «11 днів» не означає, що ШІ за 11 днів замінив багаторічну інтелектуальну історію доведення теореми. За даними Anthropic, система згенерувала приблизно 6 млрд токенів. Значна частина цієї роботи — це спроби, перевірки Lean, виправлення помилок і технічна організація великого проєкту. 5

Ключовий елемент — координація багатьох агентів

За повідомленням Anthropic, ранні запуски просувалися вперед, але мали проблему зі збереженням спільного стану роботи. Успішний запуск використовував інфраструктуру на основі Prove2Me — платформи для спільної формалізації математики. 529

Її центральна ідея — орієнтований граф залежностей:

• вузли — це ще не завершені означення, леми або теореми;
• ребра показують, які результати потрібні для доведення наступних;
• агенти можуть брати відкриті корисні задачі, доводити їх у Lean і передавати перевірені результати іншим агентам;
• система поступово рухається від базових компонентів до остаточної теореми.

Prove2Me описує такий процес як запуск «місій» з формалізації, у яких агенти додають повторно придатні формальні доведення. 29 Фактично граф перетворює одну крихку гігантську задачу на багато менших задач із чіткою перевіркою та забезпечує зовнішню «пам’ять» проєкту, не покладаючись на контекст окремого запуску моделі.

Що насправді означає «перевірено комп’ютером»

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

Це суттєво сильніше, ніж переконливий текст доведення, згенерований ШІ. Ядро Lean перевіряє, чи випливає кожен закодований крок із правил логіки, аксіом та імпортованих залежностей. Anthropic також повідомляє про перевірку того, що кінцеве твердження відповідає усталеному формулюванню FermatLastTheorem у Mathlib. 531

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

Чому Кевін Баззард назвав це надзвичайним досягненням

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

Якщо такий підхід стане відтворюваним і економічно доступнішим, він може посилити математику у кількох напрямах:

• ретельніша верифікація: формальні системи здатні виявляти пропущені умови, некоректні перетворення та несумісні означення;
• повторне використання інфраструктури: формалізовані леми можна імпортувати в наступні проєкти, не відбудовуючи їх щоразу з нуля;
• доповнення до рецензування: машинно перевірювані доведення можуть зменшити навантаження під час перевірки довгих технічних аргументів, хоча оцінка змісту, важливості та стратегії лишається за математиками.

Це можливі переваги, а не автоматична заміна математичного судження. Формальне доведення може бути логічно бездоганним, але описувати не те твердження, яке автори мали на увазі. До того ж артефакт на 13 млн рядків коду та мільярди згенерованих токенів має значну обчислювальну й інженерну ціну.

Як правильно оцінювати заяву

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

Це не новий розв’язок Великої теореми Ферма. Наступні принципові питання — чи зможуть незалежні дослідники відтворити збірку, перевірити відповідність формалізації математичному змісту, використати її компоненти в інших роботах і повторити результат для інших складних теорем. Саме ці перевірки покажуть, чи був це одиничний інженерний прорив, чи початок стійкої зміни у способі створення та перевірки сучасних математичних доведень.