Claude údajně formalizoval Fermatovu poslední větu v Leanu za 11 dní

Anthropic tvrdí, že Claude vytvořil první úplnou, od začátku do konce počítačem ověřenou formalizaci Fermatovy poslední věty (FLT) v jazyce Lean. Podstatné je, co tato zpráva neznamená: Claude neobjevil nový důkaz věty. Měl převést již známou moderní důkazovou cestu do mimořádně rozsáhlého formálního zápisu, jehož jednotlivé kroky dokáže Lean mechanicky prověřit. Anthropic uvádí 11 dní převážně autonomní práce a přibližně 13 milionů řádků leanového kódu. 215

Co vlastně bylo formalizováno

Fermatova poslední věta říká, že pro přirozená čísla a exponent alespoň 3 nemá rovnice (a^n+b^n=c^n) žádné netriviální řešení. V definici knihovny Mathlib pro Lean platí, že každé takové řešení musí mít (a=0), (b=0) nebo (c=0). To je ekvivalentní známému tvrzení o neexistenci řešení v kladných celých číslech. 31

Projekt se podle zprávy opřel o podání Darmona, Diamonda a Taylora, tedy o moderní variantu strategie Wilesova a Taylorova–Wilesova důkazu. Nešlo tedy o hledání nové cesty matematikou. Pro formalizaci je ale nutné rozepsat nejen hlavní myšlenku důkazu, nýbrž i definice, předpoklady, pomocné výsledky a spojovací kroky, které odborný text často ponechává nevyslovené. Také dřívější projekt Imperial College popisuje zvolenou trasu jako moderní variantu Wilesova/Taylorova–Wilesova důkazu. 511

Proč má důkaz 13 milionů řádků

Asistent důkazů nepřijme formulaci typu „plyne ze standardního argumentu“. Každý úsudek musí být vyjádřen tak, aby jej systém mohl typově zkontrolovat, a každý výsledek musí stát na již formalizovaných závislostech.

Anthropic uvádí, že projekt vytvořil asi 30 300 počítačem ověřených vět; přibližně 29 500 z nich se objevuje v konečném uzávěru závislostí. Vývoj zasahuje do algebry, geometrie, harmonické analýzy i teorie čísel. 215

Údaj o 11 dnech proto nelze číst jako náhradu za staletí intelektuální historie Fermatovy poslední věty. Anthropic zároveň uvádí přibližně šest miliard vygenerovaných tokenů. Práce zahrnovala mnoho kandidátních důkazů, opakované kontroly Leanem, opravy vyvolané chybami i inženýrské zajištění dlouho běžící formalizace. 5

Klíčový prvek: koordinace mnoha agentů mimo kontext jednoho modelu

Výsledek podle popisu nestál na tom, že by jediný model po celou dobu udržel celý obří důkaz v kontextu. Anthropic uvádí, že rané pokusy sice postupovaly, ale narážely na problém se sdíleným stavem projektu. Úspěšný běh proto využil infrastrukturu založenou na Prove2Me, platformě pro společnou matematickou formalizaci. 529

Základem byl orientovaný graf závislostí:

• uzly představují dosud otevřené definice, lemmata nebo věty;
• hrany vyjadřují, které výsledky potřebují výsledky následující;
• agenti mohou vybírat užitečné otevřené úlohy, dokázat je v Leanu a zpřístupnit výsledné artefakty ostatním agentům;
• systém pak postupuje od základních stavebních bloků k cílové větě.

Prove2Me tento model popisuje jako spouštění formalizačních „misí“, do nichž agenti přispívají znovupoužitelnými formálními důkazy. 29 Graf tak rozděluje jednu dlouhou a křehkou úlohu na množství ověřitelných podúloh a současně vytváří trvalou paměť projektu mimo jednotlivý běh modelu.

Co přesně znamená „počítačem ověřeno“

Anthropic uvádí, že výsledný projekt neobsahuje zástupné značky sorry, jimiž Lean dovoluje tvrzení přijmout bez důkazu, a opírá se pouze o tři standardní axiomy Leanu. 5

To je zásadně více než jazykový model, který napíše věrohodně znějící důkaz v běžném jazyce. Jádro Leanu kontroluje, zda každý zakódovaný krok vyplývá z logických pravidel systému, axiomů a importovaných závislostí. Anthropic také uvádí, že ověřil shodu konečného tvrzení se zavedenou formulací FermatLastTheorem v Mathlibu. 531

Taková kontrola má ovšem přesně vymezenou hranici: ověřuje formální tvrzení, které bylo zapsáno. Lidé stále musejí posoudit, zda formální definice a mezitvrzení věrně vyjadřují zamýšlenou neformální matematiku. Nezávislé zkompilování zveřejněného artefaktu a odborná kontrola jeho řetězce závislostí proto zůstávají podstatnými zkouškami tohoto oznámení.

Proč Kevin Buzzard mluvil o mimořádném úspěchu

Kevin Buzzard podle zprávy Anthropicu označil výsledek za „mimořádný úspěch automatické formalizace“. 21 Význam nespočívá jen v tom, že agenti dokážou dokončit jednotlivé úlohy v Leanu. Závažnější je tvrzení, že sestavili hluboce vrstvený a znovupoužitelný formální vývoj v rozsahu, který se dříve očekával spíše po letech koordinované lidské práce.

Pokud by se podobný postup ukázal jako opakovatelný a ekonomicky únosný, mohl by formalizaci matematiky posunout několika směry:

• Důslednější ověřování: formální systémy mohou odhalit chybějící předpoklady, neplatné transformace nebo nekompatibilní definice, které se v textovém důkazu hledají obtížně.
• Znovupoužitelná infrastruktura: jednou formalizované lemma lze importovat do dalších projektů a spoléhat na kontrolu jádrem systému.
• Doplněk recenzního řízení: strojově ověřitelné důkazy by mohly snížit zátěž při prověřování dlouhých technických argumentů; matematici by přitom dál posuzovali význam, smysl a strategii práce.

Jde však o možné přínosy, ne o automatickou náhradu matematického úsudku. Formální důkaz může být logicky platný, a přesto popisovat nesprávně zvolené tvrzení; vytvoření artefaktu o 13 milionech řádků navíc zůstává nákladné.

Jak zprávu číst správně

Hlásený výsledek je významným měřítkem pro AI asistovanou formalizaci, protože cílí na již prokázanou větu a výsledný artefakt má být nezávisle ověřitelný. Není správné ho prezentovat jako nové vyřešení Fermatovy poslední věty Claudem.

Nejsilnější, ale přesnější interpretace je užší: Anthropic uvádí, že koordinovaný systém agentů převedl zásadní známý důkaz do leanového vývoje v dosud nevídaném měřítku. Využil přitom rozklad úloh pomocí grafu závislostí a formální ověřování jako zpětnou vazbu. 21529

Další otázky jsou praktické: zda budou moci externí badatelé sestavení zopakovat, prověřit, že formalizace odpovídá zamýšlené matematice, znovu využít její části a dosáhnout srovnatelných výsledků i u dalších pokročilých problémů. Teprve tyto testy ukážou, zda šlo o jednorázový inženýrský výkon, nebo o trvalou změnu ve způsobu, jakým se moderní důkazy vytvářejí a ověřují.