Lean prijal Claudeov Fermatov dôkaz

Lean, softvér na kontrolu dôkazov, ktorý používajú matematici po celom svete, prijal úplnú formálnu verziu Veľkej Fermatovej vety. Formalizáciu vytvoril systém Claude od spoločnosti Anthropic a zverejnil ju v otvorenom repozitári. Neobsahuje nevyriešené pomocné kroky, dodatočné axiómy ani výpočtové skratky nad rámec štandardných základov systému Lean (repository). Matematik Kevin Buzzard z Imperial College London, ktorý viedol vlastný projekt formalizácie, nezávisle skompiloval celý projekt a potvrdil, že kontrolou prešiel. Výsledok označil za „mimoriadny úspech automatickej formalizácie“ (Buzzard).

Samotná matematická otázka je vyriešená už desaťročia. Andrew Wiles vetu dokázal v roku 1995 a medzi serióznymi matematikmi o jej platnosti neboli pochybnosti. Chýbal však prepis dôkazu do podoby pokynov pre doslovne uvažujúci kontrolný program, ktorému treba dodať každú definíciu aj každý medzikrok, ktorý môže matematik v texte považovať za samozrejmý. Podľa Anthropic zvládli desiatky agentov umelej inteligencie tento prepis za jedenásť augustových dní. Pracovali súbežne prostredníctvom platformy Prove2Me (Anthropic).

Takto uvádzaný čas však opisuje proces, ktorý ľudia mimo Anthropic nedokážu zopakovať. Súčasťou zverejnených materiálov nie sú interný model, infraštruktúra na koordináciu agentov, rozhodnutia operátorov ani množstvo spotrebovaného výpočtového výkonu. Reprodukovať sa dá hotový výsledok: každý s dostatočne výkonným hardvérom môže projekt v systéme Lean skompilovať a overiť, že dôkaz prejde kontrolou. Rovnaký formálny zápis preveril aj samostatný kontrolný program, ktorý Anthropic napísal v jazyku Rust. Potvrdil konzistentnosť všetkých 1 052 234 deklarácií (technical report). Ide však o druhú kontrolu toho istého textu, nie o nezávislé zopakovanie jedenásťdňovej práce.

Ako agenti pracovali

Formalizovať dôkaz znamená prepísať matematický argument tak, aby každý logický krok dokázal overiť program bez matematickej intuície. Samotné tvrdenie pôsobí jednoducho: pri každom celočíselnom exponente od troch vyššie neexistujú tri kladné celé čísla, pre ktoré platí aⁿ + bⁿ = cⁿ. Dôkaz však vedie cez náročné oblasti teórie čísel a v bežnom matematickom zápise zaberá stovky strán.

Claude neobjavil novú matematiku. Do formálneho jazyka prepísal známu postupnosť výsledkov vedúcich k Wilesovmu dôkazu a vychádzal pritom z výkladu matematikov Henriho Darmona, Freda Diamonda a Richarda Taylora (Anthropic, technical report). Tvorivý matematický prínos patrí Wilesovi a jeho predchodcom. Claude ho previedol do približne 10,5 milióna riadkov kódu, ktorý môže skontrolovať stroj (technical report).

Platforma Prove2Me, ktorú navrhol výskumník Anthropic Tianyi Peng s kolegami z Columbia University, rozdelila dôkaz na graf závislostí s približne 29 511 samostatnými tvrdeniami (technical report). Agenti si vyberali tvrdenia, pri ktorých už boli splnené všetky predpoklady, zapisovali k nim dôkazy v systéme Lean a navzájom kontrolovali navrhnuté formulácie. Vďaka tomu mohli pracovať súbežne. Počas projektu vytvoril interný výskumný model približne šesť miliárd výstupných tokenov (technical report).

Podľa Anthropic ľudskí operátori počas projektu nenapísali žiadny kód v systéme Lean. Vybrali však vetu, poskytli známu cestu k dôkazu, navrhli infraštruktúru agentov a príležitostne upravovali priority (Anthropic). Úplný záznam ich zásahov ani náklady na výpočty spoločnosť nezverejnila.

Výsledok stojí na rokoch ľudskej práce

Formalizácia využíva Mathlib, rozsiahlu komunitne spravovanú knižnicu formalizovanej matematiky, a priamo nadväzuje na dva staršie projekty. Buzzardov tím na Imperial College pracoval na formalizácii Veľkej Fermatovej vety v systéme Lean od konca roka 2023. Projekt financoval grant EPSRC vo výške 1 milióna libier, plánovaný až do roku 2029 (EPSRC award). Samostatný komunitný projekt už predtým formalizoval vetu pre časť prípadov. Anthropic vo svojom zozname zdrojov uvádza 106 súborov s materiálom prevzatým alebo upraveným z týchto projektov (attribution).

Jedenásť kalendárnych dní súbežnej práce sa preto nedá priamo porovnávať s časom, ktorý projektu venoval Buzzardov tím. Keď Claude začal pracovať, ľudský projekt mal za sebou približne 22 mesiacov financovaného vývoja (EPSRC award). Anthropic nezverejnil počet hodín práce grafických procesorov ani spotrebu energie.

Pred zverejnením tohto projektu bola Veľká Fermatova veta poslednou nespracovanou položkou v zozname 100 významných viet, ktoré čakali na formalizáciu. Zoznam matematika Freeka Wiedijka slúži ako meradlo pokroku už dve desaťročia (Buzzard).

O tom, či sa tento postup dá všeobecne uplatniť, viac napovie až formalizácia novšej a horšie zdokumentovanej matematiky, pri ktorej neexistuje hotový plán dôkazu, rozvinuté knižnice ani predchádzajúca formálna práca. V tomto prípade dostali agenti známu vetu so značnou časťou potrebnej infraštruktúry. Výsledok ukazuje, že za takýchto podmienok dokážu vytvoriť úplnú formalizáciu, ktorú Lean prijme a ktorú môžu nezávisle skontrolovať aj ľudia mimo Anthropic. Zo zverejnených materiálov však nemožno zopakovať samotný proces jej vytvorenia.