Anthropic zverejnil formálny Lean dôkaz Fermatovej poslednej vety

Anthropic Lean dôkaz Fermatovej poslednej vety je nový verejne dostupný formálny zápis už známeho matematického výsledku, nie nové vyriešenie problému. Spoločnosť Anthropic 4. septembra 2026 oznámila kompletný strojovo overený dôkaz v systéme Lean 4. Prvý ľudský dôkaz vety publikovali Andrew Wiles a Richard Taylor v roku 1995.

Fermatova posledná veta tvrdí, že rovnica xⁿ + yⁿ = zⁿ nemá pre prirodzené čísla x, y, z a celé n väčšie než 2 nenulové riešenia. Jej význam v tomto prípade nespočíva v novom poznatku z teórie čísel, ale v rozsahu a spôsobe strojovej formalizácie moderného dôkazu.

Anthropic Lean dôkaz vznikal s viacagentovým postupom

Podľa Anthropic na projekte prevažne autonómne pracoval systém Claude počas 11 dní. Vytvoril približne 13 miliónov riadkov kódu pre Lean a využil viacagentový postup na platforme Prove2Me. Spoločnosť zároveň uvádza, že systém dostával občasné ľudské pokyny a pracoval aj s existujúcimi ľudskými formalizačnými projektmi.

To je podstatné obmedzenie pri interpretácii výsledku. Mieru autonómie nie je možné nezávisle presne zmerať iba zo zverejnených materiálov. Výsledok preto nemožno stotožňovať so samostatným objavením matematického dôkazu umelou inteligenciou. Ide o prepis a prepojenie známeho argumentu do jazyka, ktorý dokáže overiť proof assistant.

Anthropic zdrojový kód sprístupnil v repozitári GitHub. Dokumentácia projektu deklaruje úspešnú kontrolu jadrom Lean, nástrojom comparator a druhým nezávislým jadrom nanoda. Tieto postupy majú overovať, že formálny objekt zodpovedá pravidlám logiky a typového systému používaného Leanom.

Kontrolu potvrdil aj matematik Kevin Buzzard

Matematik Kevin Buzzard, ktorý stojí za projektom Xena zameraným na výučbu a popularizáciu formalizácie matematiky, uviedol, že repozitár skompiloval a dôkaz overil nástrojom comparator. Podľa jeho vyjadrenia formálny dôkaz kontrolou prešiel.

Takéto overenie je dôležité najmä preto, že verejný repozitár umožňuje ďalším výskumníkom výsledok reprodukovať. Formálna kontrola pritom potvrdzuje logickú platnosť tvrdenia v rámci Leanu pri dôvere v použité kontrolné nástroje. Sama osebe však neznamená, že každý názov, medzikrok alebo ľudský výklad v kóde automaticky vystihuje zamýšľanú matematickú interpretáciu.

Anthropic svoj výsledok označuje za najväčší Lean dôkaz. Označenie „najdlhší matematický dôkaz všetkých čias“ však nemožno spoľahlivo potvrdiť, keďže neexistuje verejne doložený univerzálny rebríček matematických dôkazov podľa dĺžky. Bezpečnejšie je hovoriť o veľmi rozsiahlom formálnom dôkaze a podľa Anthropic o najväčšom projekte svojho druhu v Lean.

Rozdiel medzi objavom a formalizáciou

Formálne dôkazy prevádzajú matematické argumenty do presnej podoby, ktorú môže skontrolovať softvér. Pri rozsiahlych moderných dôkazoch je takýto prepis náročný na čas aj odbornú prácu: treba explicitne zachytiť definície, predpoklady, pomocné tvrdenia a všetky logické kroky, ktoré sú v bežnom odbornom texte často zhrnuté.

Práve preto je zverejnený Anthropic Lean dôkaz míľnikom v autoformalizácii. Verejný artefakt ukazuje, že viacagentový AI systém dokázal v krátkom čase vytvoriť a nechať strojovo overiť rozsiahlu formalizáciu známeho dôkazu. Nehovorí však sám o sebe nič o tom, či systém našiel nový výsledok v teórii čísel.

Ďalšie posúdenie sa bude sústreďovať na nezávislé reprodukcie kompletného buildu a kontrolných skriptov. Odborníci budú môcť preskúmať aj rozsah použitých existujúcich komponentov, kvalitu prepojenia s pôvodným Wilesovým dôkazom a praktickú reprodukovateľnosť projektu pri nižších hardvérových nárokoch.

Overené a aktualizované: 05. 09. 2026 15:25