Lean přijal formální důkaz Fermatovy věty

Lean, software pro ověřování důkazů používaný matematiky po celém světě, přijal úplný formální důkaz Velké Fermatovy věty. Formalizaci vytvořil systém Claude společnosti Anthropic a firma ji zveřejnila v otevřeném repozitáři. Neobsahuje nevyřešené mezikroky, dodatečné axiomy ani výpočetní zkratky nad rámec standardních základů Leanu (repository). Projekt nezávisle zkompiloval také matematik Kevin Buzzard z Imperial College London, který vedl vlastní pokus o formalizaci věty. Potvrdil, že kontrolou prošel, a výsledek označil za „mimořádný úspěch automatické formalizace“ (Buzzard).

Samotný matematický problém je dávno vyřešený. Andrew Wiles větu dokázal v roce 1995 a mezi seriózními matematiky o její platnosti nebyly pochybnosti. Chyběl však přepis důkazu do podoby instrukcí pro doslovně pracující kontrolní program, kterému je nutné dodat každou definici i všechny mezikroky, jež mohl autor původního důkazu ponechat nevyslovené. Podle Anthropic zvládly desítky agentů umělé inteligence tento převod během jedenácti srpnových dnů. Souběžně pracovaly prostřednictvím platformy Prove2Me (Anthropic).

Uváděných jedenáct dní ovšem popisuje proces, který nelze zvenčí zopakovat. Součástí zveřejněných materiálů nejsou interní model, infrastruktura pro řízení agentů, rozhodnutí operátorů ani spotřebovaný výpočetní výkon. Opakovaně ověřit lze hotový výsledek: kdo má dostatečně výkonný hardware, může projekt v Leanu zkompilovat a zkontrolovat platnost důkazu. Tentýž formální zápis prověřil také samostatný kontrolní program, který Anthropic napsal v jazyce Rust. Podle firmy potvrdil konzistenci všech 1 052 234 deklarací (technical report). Jde však o druhé přečtení stejného textu, nikoli o nezávislé zopakování celé jedenáctidenní práce.

Jak agenti pracovali

Při formalizaci se matematický argument přepisuje tak, aby každý logický krok dokázal ověřit program bez matematické intuice. Samotné tvrzení působí prostě: pro žádný celočíselný exponent od tří výše neexistují tři kladná celá čísla, která by splňovala rovnici aⁿ + bⁿ = cⁿ. Důkaz však vede přes hluboké oblasti teorie čísel a v běžném matematickém zápisu zabírá stovky stran.

Claude novou matematiku neobjevil. Do formální podoby převedl známý řetězec výsledků vedoucí k Wilesovu důkazu, přičemž vycházel z výkladu matematiků Henriho Darmona, Freda Diamonda a Richarda Taylora (Anthropic, technical report). Tvůrčí matematické myšlenky pocházejí od Wilese a jeho předchůdců. Claude je přeložil do přibližně 10,5 milionu řádků kódu, jehož správnost může ověřit stroj (technical report).

Platforma Prove2Me, kterou navrhl výzkumník Anthropic Tianyi Peng spolu se spolupracovníky z Columbia University, rozdělila důkaz do grafu závislostí tvořeného zhruba 29 511 samostatnými tvrzeními (technical report). Agenti si vybírali tvrzení, pro něž už byly splněny všechny předpoklady, zapisovali jejich důkazy v Leanu a navzájem kontrolovali navržené formulace. Celý běh spotřeboval přibližně šest miliard výstupních tokenů interního výzkumného modelu (technical report).

Podle Anthropic během práce nenapsali lidští operátoři v Leanu žádný kód. Vybrali však dokazovanou větu, poskytli známou cestu k důkazu, navrhli infrastrukturu agentů a občas upravili priority (Anthropic). Úplný záznam zásahů operátorů ani náklady na výpočetní výkon firma nezveřejnila.

Výsledek stojí na letech lidské práce

Formalizace se opírá o Mathlib, rozsáhlou komunitně spravovanou knihovnu formální matematiky, a přímo využívá výsledky dvou starších projektů. Buzzardův tým na Imperial College London pracoval na formalizaci Velké Fermatovy věty v Leanu od konce roku 2023. Projekt s plánovaným trváním do roku 2029 získal od EPSRC grant ve výši jednoho milionu liber (EPSRC award). Jiný komunitní projekt už dříve formalizoval větu pro část případů. V souboru s přehledem použitých zdrojů uvádí Anthropic 106 souborů, které obsahují materiál převzatý nebo upravený z těchto projektů (attribution).

Díky souběžné práci agentů nelze jedenáct kalendářních dnů porovnávat s počtem člověkohodin, které projektu věnoval Buzzardův tým. V době zahájení Claudeova běhu za sebou měl přibližně 22 měsíců financované práce (EPSRC award). Anthropic nezveřejnil počet hodin provozu grafických procesorů ani spotřebu energie.

Před zveřejněním tohoto výsledku zůstávala Velká Fermatova věta poslední neformalizovanou položkou na seznamu sta významných matematických vět, který sestavil Freek Wiedijk a který už dvě desetiletí slouží jako měřítko pokroku v oboru (Buzzard).

O skutečné obecnosti této metody rozhodnou až pokusy formalizovat novější a hůře zdokumentovanou matematiku, pro niž neexistuje podrobný návod, vyzrálé knihovny ani předchozí formální práce. V tomto případě dostali agenti slavnou větu, známou cestu k důkazu a podstatnou část potřebné infrastruktury. Výsledek ukazuje, že za těchto podmínek dokážou vytvořit úplnou formalizaci, kterou Lean přijme a kterou mohou nezávisle překontrolovat i další lidé. Samotný proces jejího vytvoření však ze zveřejněných materiálů zopakovat nelze.