Anthropic випустила згенерований ШІ-агентами доказ великої теореми Ферма в Lean 4
Anthropic опублікувала повний машинно верифікований доказ великої теореми Ферма на Lean 4. Репозиторій, згенерований ШІ-агентами на базі Mathlib, містить 29 511 теорем і проходить перевірку ядрами Lean та Rust без сторонніх аксіом.
Вплив: Середній
Чому це важливо
Дослідіть наскрізний пайплайн агентної формальної верифікації та запустіть незалежну перевірку ядрами локально.
TL;DR
- 01ШІ-агенти синтезували формальний доказ із 29 511 теорем без використання сторонніх аксіом.
- 02Коректність підтверджено незалежно як рідним ядром Lean, так і Rust-ядром nanoda без заповнювачів sorry.
- 03Повна перевірка вимагає значних ресурсів: до 300 ГБ оперативної пам'яті та 15 годин роботи одного ядра.
Ключові факти
- Перевірено теорем
- 29 511
- Всього верифіковано декларацій
- 1 052 234
- Версія тулчейну
- Lean 4.33.1 (Mathlib v4.33.0)
- Пікове споживання пам'яті
- 300 ГБ (comparator replay)
- Вторинне ядро верифікації
- nanoda 0.4.13 (Rust)
Архітектура машинної верифікації
Репозиторій містить 60 475 модулів, які доводять fermat_last_theorem у середовищі Lean 4.33.1 з Mathlib v4.33.0. Ціль збірки FinalCheck.lean перевіряє, що доказ спирається виключно на три стандартні аксіоми Lean: propext, Classical.choice та Quot.sound. У коді відсутні конструкції sorry, axiom, native_decide, unsafe, extern чи partial def.
Незалежна валідація двома ядрами
Команда Anthropic підтвердила коректність двома верифікаторами. Спочатку leanprover/comparator зіставив збірку із файлом verification/comparator/Challenge.lean за 14 годин 46 хвилин на одному ядрі при піковому споживанні 230 ГБ оперативної пам'яті. Потім стороннє ядро nanoda версії 0.4.13, написане на Rust, перевірило всі 1 052 234 експортовані декларації за 30 хвилин на 16 потоках при 40 ГБ RAM.
Пайплайн та інструкція з відтворення
Вихідні тексти Lean згенеровано ШІ-агентами з використанням конвеєрних міток (таких як P2M та шістнадцяткових суфіксів) і оптимізовано для перевірки машиною, а не читання людиною. Для відтворення потрібні Linux або macOS, утиліта elan та компіляція Mathlib із сирців. Паралельна збірка потребує близько 5 ГБ RAM на потік (до 36 ГБ на окремих модулях) і 67 ГБ диску під .lake/. Для локального перегляду графа залежностей надається директорія html/.
Спробуй за 2 хвилини
git clone https://github.com/anthropics/fermats-last-theorem flt && cd flt
LEAN_NUM_THREADS=96 lake build
verification/comparator/run.sh
verification/nanoda/run.shbash
✓ Коли використовувати
- Використовуйте для дослідження методів генерації формального коду агентами під компіляторний контроль.
- Використовуйте як стрес-тест для альтернативних ядер Lean, валідаторів типів та інфраструктури Lake.
✕ Коли НЕ варто
- Не використовуйте як робочу математичну бібліотеку: репозиторій позначено як дослідницький і закритий для правок.
- Не запускайте повну збірку на комп'ютерах із менш ніж 64 ГБ RAM без жорсткого обмеження паралельних потоків.
Що зробити сьогодні
- Склонуйте репозиторій та вивчіть lakefile.lean для фіксації тулчейну Lean 4.33.1.
- Відкрийте html/index.html локально, щоб переглянути згенеровані графи залежностей теорем.
- Ознайомтеся з verification/comparator/Challenge.lean, щоб побачити приклад формування критеріїв верифікації.
Що каже спільнота
“I have never seen an AI or a human produce a false proof without explicitly using weird meta programming tricks that are very suspicious. No 'good faith' Lean proofs have every been shown faulty”
“Much of the value of proof is in the development of math definitions and intermediate theorems needed to get you there... I wonder if AI could develop this skill too through a process of efficiently refactoring”
Джерела