Anthropic: Claude за 11 днів написав перевірений комп'ютером доказ Великої теореми Ферма
Anthropic оприлюднила перший повний доказ Великої теореми Ферма, перевірений комп'ютером: Claude писав його мовою Lean переважно автономно 11 днів — 13 млн рядків коду.
Що сталося
Anthropic опублікувала перший повний, перевірений комп'ютером доказ Великої теореми Ферма. За даними компанії, Claude переважно автономно працював 11 днів, щоб записати доказ мовою Lean — мовою програмування для формальної верифікації — і створив 13 мільйонів рядків коду та 29 500 проміжних теорем.
Роботою керував дослідник Anthropic Тяньї Пен, чия група в Колумбійському університеті створює інструменти для формалізації за допомогою ШІ. Доказ відкрито опубліковано на GitHub.
Чому це важливо
Твердження Ферма — жодні додатні цілі a, b і c не задовольняють aⁿ + bⁿ = cⁿ для n > 2 — з'явилося близько 1637 року; Ендрю Вайлз довів його лише 1995-го: 129 сторінок, перевірка яких зайняла місяці. На відміну від недавньої роботи ШІ над гіпотезою Рімана, де з'явилася нова математика, тут новизна в перевірці: формалізований доказ перевіряє машина.
Що кажуть експерти
Кевін Баззард з Імперського коледжу Лондона, який очолює багаторічний проєкт формалізації теореми, назвав це «надзвичайним досягненням автоформалізації»: теорему доведено без жодних припущень, крім аксіом математики. За словами Anthropic, результат указує на майбутнє, у якому математичні знання буде легше перевіряти — і легше їм довіряти.