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

Важливо розрізняти два різні завдання. Саме доведення Великої теореми Ферма належить Ендрю Вайлсу і існує з 1994 року — Claude його не «придумував» і не переоткривав. Мова про інше: чи здатен сучасний AI-асистент допомогти перетворити багатосторінковий, писаний людською мовою математичний текст на формальний артефакт, який машина може автоматично звірити крок за кроком. Раніше такі проєкти формальної верифікації забирали в математиків роки ручної праці.

Що саме зробили в Anthropic?

Команда дослідників використала Claude як інструмент для формалізації вже наявного доведення теореми Ферма в системі перевірки формальних доведень — на кшталт тих, де кожен логічний крок кодується явно і автоматично перевіряється комп'ютером. Ми вже розбирали, як Claude впорався з подібною формалізацією в Lean за 11 днів — і матеріал SiliconANGLE AI лише підтверджує масштаб цього напрямку: складні математичні доведення, які досі формалізувалися роками командами фахівців, тепер можна перевести в машинно-читабельний вигляд істотно швидше за участі AI-моделі.

Формальна верифікація в математиці — це процес перекладу доведення на мову, яку розуміє комп'ютерна система перевірки (proof assistant), після чого програма механічно підтверджує, що кожен логічний крок справді випливає з попереднього без прихованих припущень чи помилок. На відміну від рецензування людьми, такий процес не залишає простору для суб'єктивної інтерпретації.

Чому формалізація доведення Ферма — окремо складна задача?

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

Що це говорить про рівень Claude у формальній верифікації?

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

Висновок AiiN: що це означає для AI-білдерів?

Наша теза проста: формальна верифікація — одна з небагатьох областей, де відповідь AI-моделі можна перевірити автоматично й безкомпромісно, без «на око» оцінки людиною. Саме тому такі результати важать більше, ніж бенчмарки на кшталт олімпіадних задач: тут немає місця для галюцинацій, що виглядають переконливо, — proof assistant або приймає доведення, або ні. Якщо ви будуєте продукти для наукових команд, юридичної перевірки контрактів чи аудиту коду, варто придивитися саме до задач із бінарним, механічно перевірюваним критерієм успіху — це та ніша, де сучасні моделі вже показують надійність, придатну для продакшену, а не лише для демо.

Що таке proof assistant і навіщо він потрібен?

Proof assistant (система перевірки доведень) — це програма, яка приймає формально записане математичне твердження та доведення і автоматично перевіряє кожен логічний крок на коректність. Найвідоміші приклади — Lean, Coq та Isabelle; вони використовуються не лише в чистій математиці, а й для верифікації критичного програмного коду та протоколів безпеки.

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

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