Anthropic повідомила, що Claude завершив перше повне формалізоване доведення Великої теореми Ферма. Це не відкриття теореми знову, а переписування існуючого доведення у вигляді логічного коду, який комп’ютер може перевірити рядок за рядком. Компанія зазначила, що на цю роботу було витрачено 11 днів, і в результаті було отримано близько 13 мільйонів рядків.
Значення формалізованого доведення полягає у тому, щоб записати математичні міркування мовою, зрозумілою для машини. Традиційні публікації з доведеннями часто вимагають тривалої перевірки колегами; якщо деякий крок містить прогалину, виправлення може тривати місяці або навіть роки. Велика теорема Ферма була доведена британським математиком Ендрю Вайлзом у 1995 році, але перетворення цього доведення на повністю машинно-перевірювану версію завжди вважалося надзвичайно складним інженерним завданням.
11 днів для досягнення довгострокової цілі
Математик Лондонського імперського коледжу Кевін Баджард з 2024 року продовжує проект, метою якого є переписування доведення Вайлза у системі Lean. За початковим планом, ця робота вимагатиме довгострокової співпраці, а фінансування забезпечено до 2029 року.
Anthropic зазначила, що Claude виконала це завдання раніше, ніж інші подібні цілі. Після перевірки Buzzard зазначив, що цей доказ може бути підтверджений без використання додаткових припущень, тобто лише на основі найбазовіших аксіом математики.
Виконується паралельно кількоми агентами
За словами Anthropic, команда дослідників з Колумбійського університету під керівництвом Тяньї Пенг застосувала кілька агентів Claude для паралельної роботи: кожен відповідав за написання визначень та доведення менших висновків, а потім поступово з’єднував їх у більш складні структури доведень. Людська інтервенція була мінімальною і зводилася переважно до визначення пріоритетів на кожному етапі.
Початковий прогрес був не дуже гладким. Anthropic зазначила, що деякі агенти тимчасово не могли ділитися завершеними матеріалами та повторювали роботу. Пізніше команда використала інструмент під назвою Prove2Me, щоб надати кожному агенту єдиний список завдань та спосіб організації файлів, а також зберегти зауваження мовою натуральної мови, щоб допомогти їм повторно використовувати результати один одного.
- Підтримуюча теорема понад 30 000
- Загальний обсяг споживання досяг десятків мільярдів токенів
- Остаточно підтверджено близько 13 мільйонів рядків
Зробіть акцент на перевірності, а не на нових теоремах
Головна досягнення цього результату полягає не у відкритті нових математичних тверджень, а у перетворенні вже існуючих важливих доведень на версії, які можна поступово перевірити за допомогою комп’ютера. Зі зростанням кількості математичних статей та контенту, згенерованого ШІ, витрати на ручну перевірку доведень зростають, тому формальні інструменти отримують все більше уваги.
Anthropic також зазначила, що обсяг цього доведення перевищує в п’ять разів загальнодоступну математичну бібліотеку Mathlib, яку використовують математики. Повний файл завантажено на GitHub, і дослідники можуть продовжувати поетапний аналіз його структури та коректності.