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

Для тих, хто будує AI-агентів для наукової чи інженерної роботи, сам факт застосування LLM до формальної верифікації важливіший за конкретний результат. Формальна верифікація — це не «Claude написав доведення», а перевірка того, чи вже існуюче математичне доведення коректне крок за кроком, у мові, яку може перевірити машина (наприклад, Lean чи Coq). Це принципово інша задача, ніж генерація тексту: тут немає місця для правдоподібної, але хибної відповіді — верифікатор або приймає доведення, або відхиляє його.

Ось чому цей кейс цікавий не як ще одна демонстрація можливостей LLM, а як маркер зрілості: доведення теореми Ферма (Ендрю Вайлз, 1994) — сотні сторінок складної алгебричної геометрії. Формалізація такого обсягу тексту вручну займає роки; якщо модель здатна суттєво прискорити цей процес, це змінює економіку формальної верифікації в математиці й криптографії.

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

За даними TLDR AI, Claude використали для формальної верифікації доведення теореми Ферма — тобто для перетворення чи перевірки математичного доведення у форматі, придатному для автоматизованого контролю коректності. Джерело подає це стисло, без розшифровки конкретного стеку інструментів чи версії моделі, тому деталі методики (який саме варіант доведення, який формальний верифікатор, скільки кроків) з дайджесту не випливають.

Чому формальна верифікація складна навіть для сильних LLM?

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

Саме тому формальна верифікація — один із найжорсткіших тестів на здатність LLM утримувати структуру довгого міркування, суворіший за більшість публічних математичних бенчмарків.

До чого тут AI-дослідник і чіп Z1?

У тому ж дайджесті TLDR AI побіжно згадує автоматизованого AI-дослідника та новий енергоефективний чіп Z1 — без розкриття, хто саме їх випустив і що вони роблять. За такою скупою згадкою джерела ми не будемо домислювати зв'язок між цими трьома темами: ймовірно, дайджест просто зібрав кілька окремих новин AI-тижня в один випуск, а не описав єдиний проєкт. Якщо цікаво отримати повну картину по AI-дослідникам та енергоефективному залізу, варто читати оригінальний випуск TLDR AI, а не покладатися на короткий переказ.

Висновок AiiN

Наша теза: застосування LLM саме до формальної верифікації, а не до генерації нового доведення з нуля, — це ознака того, що індустрія переходить від «моделі, які пишуть правдоподібний текст» до «моделі, яким можна доручити задачі з жорстким, машинно-перевіреним критерієм правильності». Для AI-білдерів це сигнал: якщо ваш продукт працює з областями, де є формальний критерій істинності (код з тестами, математика з верифікаторами, конфігурації з валідаторами схем), варто дивитися саме на такі pipeline — генерація плюс незалежна формальна перевірка — а не на голу генерацію відповіді моделлю. Схожу обережність щодо сліпої довіри до математичних AI-агентів ми вже розбирали, коли DeepMind зафіксував reward hacking у математичних AI-агентах — формальний верифікатор саме і закриває цю діру, бо не приймає нічого, крім строго коректного доведення.

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

Ні. За даними TLDR AI, йдеться про застосування моделі до верифікації вже існуючого доведення (Ендрю Вайлза, 1994), а не про створення нового математичного результату з нуля.

Що таке формальна верифікація доведення?

Це процес перевірки математичного доведення спеціальним програмним асистентом (наприклад, Lean або Coq), який крок за кроком підтверджує логічну коректність, не покладаючись на людську інтуїцію чи авторитет автора.

Чому це важливо для AI-білдерів поза математикою?

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