Anthropic 4. septembra oznámil, že Claude vytvoril prvý kompletný počítačom overený dôkaz Fermatovej vety — výsledok, na ktorom matematici pracovali vyše 350 rokov, kým ho v roku 1995 vyriešil Andrew Wiles. Model pracoval 11 dní takmer autonómne a výsledkom je formalizácia v programe Lean, ktorá si vystačí iba s tromi štandardnými axiómami matematiky.
Čo presne vzniklo
- 13 miliónov riadkov kódu Lean 4 — viac než päťnásobok veľnosti Mathlib, hlavnej komunitnej knižnice formálnej matematiky.
- 30 300 dokázaných teorémov, z toho 29 500 vstúpilo do finálneho dôkazu.
- Približne 6 miliárd výstupných tokenov z interného výskumného modelu, ktorý Anthropic opisuje ako zhruba porovnateľný s Claude Fable 5.1.
- Dôkaz bol dvakrát overený — jadrom Lean aj nezávislou druhou implementáciou kernelu v jazyku Rust; build odmieta akékoľvek skratky typu dodatočné axiómy či nedokázané kroky.
- Celý artefakt je open-source pod licenciou Apache 2.0 v repozitári anthropics/fermats-last-theorem na GitHube.
Ako sa to podarilo
Prvý multiagentový pokus sa po niekoľkých dňoch rozpadol — agenti strácali prehľad o stave projektu a prestali spolupracovať; zlyhania tvoria asi 7 % riadkov finálneho dôkazu. Zlom prišiel po presune na platformu Prove2Me výskumníka Tianyi Penga (Anthropic a Kolumbijská univerzita): tá vedie orientovaný acyklický graf výrokov teorémov, podľa ktorého si desiatky paralelných agentov vyberali, ktorý čiastočný dôkaz skúsiť ďalej. Ľudský vstup sa obmedzil na príležitostné pokyny typu „Jacobian ako schéma znie ako priorita“.
Anthropic pridal aj „rozpočtovú“ ukážku: trom obyčajným predplatným Claude Max trvalo sformalizovať Vinogradovovu vetu o troch prvočíslach tri dni.
Čo to je — a čo rozhodne nie je
Kľúčové je pomenovať presne, čo sa stalo: Claude neobjavil nový dôkaz. Postupoval zjednodušenou verziou Wilesovej stratégie z roku 1995 v podaní Darmona, Diamonda a Taylora a staval na rokoch predchádzajúcej ľudskej práce — vrátane základov, ktoré v Leane pripravil tím Kevina Buzzarda z Imperial College London. Novinkou je, že AI dokázala preložiť jeden z najzložitejších dôkazov modernej matematiky do formy, ktorú počítač overí riadok po riadku — a za dni, nie za roky.
Reakcia komunity
Buzzard, ktorý od roku 2024 vedie komunitný projekt formalizácie tej istej vety (financovaný do 2029 a stále nedokončený), výsledok preskúmal a hovorí o „mimoriadnom úspechu autoformalizácie“:
„Ak je automatická formalizácia Fermatovej vety možná už dnes, urobili sme veľký krok k automatickej formalizácii modernej matematickej literatúry. Takéto techniky povedú k nástrojom, ktoré odhalia chyby v súčasnej matematickej zásobe a odľahčia recenzentov.“
Prečo na tom záleží aj mimo matematiky
- Dôvera sa presúva na overiteľnosť. Namiesto „verte mi“ prináša agent artefakt, ktorý si vie skontrolovať stroj — vzor, ktorý sa pravdepodobne prenesie do softvérového inžinierstva a vedy.
- Recenzentské bremeno. Nové matematické práce dnes recenzujú ľudia mesiace; formalizácia môže skontrolovať logickú reťaz okamžite.
- Mierna dávka skepticizmu zostáva na mieste. Čísla o 11 dňoch a 6 miliardách tokenov sú firemné údaje Anthropic; overiteľný je najmä samotný repozitár a jeho build, nie náklady. A ani tak zostáva pravda, že íslo o preklad známej matematiky, nie o nový objav — tvorivosť klásť otázky zostáva na ľuďoch.
