Теорему Ферма формалізовано в Lean
4 вересня 2026 року Anthropic оприлюднила, за її словами, перше повне машинно перевірене доведення Великої теореми Ферма в Lean: Claude, діючи здебільшого самостійно, написав його за 11 днів, 13 мільйонів рядків Lean. Це формалізація доведення Вайлса 1995 року, а не нова математика. Репозиторій каже, що ядро Lean, інструмент Comparator і друге ядро (nanoda) прийняли доведення, лише з трьома стандартними аксіомами.
Чому це важливо
Раніше такий проєкт вважали роботою на роки (спільнота під керівництвом Баззарда веде його з 2024 року); тут він закритий за 11 днів. Anthropic сама наголошує, що нове — перевірка, не математика. Стан твердження: заявлено й формалізовано; перегляд Баззарда наведено зі слів Anthropic.
Стан твердження. Заявлено: допис Anthropic «Formalizing Fermat’s Last Theorem» від 4 вересня; прочитано повністю. Формалізовано в Lean: репозиторій github.com/anthropics/fermats-last-theorem (створено 4 вересня 14:21 UTC, остання зміна 24 вересня); його README: Lean 4.33.1, Mathlib v4.33.0, зібрано 60 475 модулів; Comparator v4.33.0 каже «Your solution is okay!»; друге ядро, nanoda 0.4.13 (авторам довелося внести чотири невеликі зміни, які, за ними, не додають і не послаблюють жодного правила типізації), прийняло експорт — 1 052 234 оголошення без помилок; жоден модуль не містить axiom, sorry чи native_decide; лише propext, Classical.choice, Quot.sound. Збирання зайняло 5 год 32 хв, Comparator — 14 год 46 хв на машині авторів. Прохід репозиторій не збирав. README каже й про межу: жоден інструмент не перевіряє, чи кожна проміжна теорема означає те, що називає її ім’я. PROOF-PATH.md у розділі про точну силу кроків каже, що названі класичні теореми (Мазур, Ленглендз — Таннелл, підняття модулярності, Вайлс, Рібет) доведено в тій силі, якої потребує аргумент, а не в загальному вигляді; доведено твердження з формулювання Mathlib FermatLastTheorem. 106 файлів містять матеріал із проєкту Імперського коледжу (Баззард) і flt-regular. Перевірено людьми: Anthropic наводить слова Кевіна Баззарда, що доведення «доводить Велику теорему Ферма без жодних припущень, окрім аксіом математики», і дякує йому за перегляд; його власного тексту не знайдено. Оскарження в прочитаному не знайдено. Роль ШІ. Дослідник Anthropic Тяньї Пен, чия група в Колумбійському університеті створює інструменти формалізації, вирішив перевірити, чи просунеться в цьому Claude; людські вказівки обмежувалися окремими високорівневими розпорядженнями; Claude працював із десятками агентів на платформі Prove2Me, близько шести мільярдів вихідних токенів «універсальної внутрішньої дослідницької моделі, приблизно порівнянної з Claude Fable 5.1». Чого запис не стверджує: що доведено щось нове про теорему Ферма; що проєкт Баззарда завершено; що прохід збирав доведення.