Umělá inteligence Claude od firmy Anthropic během jedenácti dní z velké části samostatně vytvořila první kompletní, počítačem ověřený důkaz Fermatovy poslední věty. Nejde ale o to, že by AI vyřešila třistapadesát let starý matematický problém sama od sebe, tu práci už v roce 1995 odvedl britský matematik Andrew Wiles. Úspěch spočívá v něčem jiném, a možná stejně důležitém.
Firma Anthropic výsledek zveřejnila 4. září 2026. Podle oficiálního oznámení na firemním webu celý projekt rozjel Tianyi Peng, výzkumník Anthropic, jehož skupina na Kolumbijské univerzitě vyvíjí nástroje pro takzvanou autoformalizaci matematiky, a chtěl otestovat, jak daleko dokáže Claude s formalizací Fermatovy poslední věty dojít. Výsledek předčil jeho očekávání. Claude během jedenácti dní z velké části samostatné práce v srpnu 2026 vytvořil první důkaz, který od začátku do konce prošel počítačovým ověřením v programovacím jazyce Lean, a napsal přitom přes 13 milionů řádků kódu, tedy víc než pětinásobek velikosti Mathlibu, hlavní komunitní knihovny matematických důkazů, na které celý projekt stavěl.
Na projektu podle stejného zdroje pracovaly desítky agentů Claude souběžně, koordinovaných pomocí nástroje nazvaného Prove2Me a systému postaveného na Claude Code, přičemž dohromady dokázaly ověřit přes 30 300 dílčích matematických vět, z nichž 29 500 se nakonec využilo v samotném finálním důkazu. Celý proces spotřeboval zhruba šest miliard výstupních tokenů. Podle podrobného přehledu na wiki serveru AIWiki šlo o interní výzkumný model, který Anthropic označuje jako přibližně srovnatelný s modelem Claude Fable 5.1.
Průběh práce lze podle stejného zdroje sledovat téměř den po dni. Pátý den, 11. srpna, agenti dokázali klíčový případ Mazurovy věty, zatímco tým ještě ráno odhadoval, že mu zbývající část argumentu zabere jeden až tři týdny. Šestý den bylo hotovo přes deset tisíc vět, osmý den padl centrální krok Ribetova argumentu a devátý den měli agenti na místě všech šestnáct kroků takzvané Eichler-Šimurovy věty, čekajících už jen na jeden otevřený základní výsledek. Jedenáctý den, 17. srpna, byl dokázán potřebný případ Langlandsovy-Tunnellovy věty a týž den večer byla Fermatova poslední věta na interní platformě označena za dokázanou. O dva dny později tým celý strom 29 511 karet znovu zkompiloval ze zdrojového kódu jako jediný ucelený projekt v jazyce Lean.
Důležité je pochopit, co slovo formalizace v tomto kontextu znamená. Wilesův původní důkaz z roku 1995 stavěl na myšlenkách celé řady matematiků, mezi nimi Freye, Serrea, Ribeta, Mazura, Langlandse, Tunnella, Tanijamy, Šimury a Weila, a byl napsaný běžným matematickým jazykem, který ověřují lidští recenzenti. Formalizace znamená převést tuto lidskou argumentaci do podoby, kterou dokáže řádek po řádku zkontrolovat počítač, aniž by musel důvěřovat pouhému slovu matematika. Tento typ práce běžně zabere měsíce až roky ručního úsilí, a podle technologického serveru popisujícího dosažený výsledek na stejném úkolu od roku 2024 pracuje i lidský tým formalizátorů na Imperial College London, který přitom svou práci dosud nedokončil, zatímco Claude ho v tomto konkrétním závodě předběhl.
Výsledek si před zveřejněním ověřil i uznávaný britský matematik Kevin Buzzard z Imperial College London, jeden z klíčových odborníků na formalizaci matematiky v jazyce Lean. Podle jeho hodnocení citovaného v oznámení Anthropic jde o mimořádný výsledek autoformalizace, který dokazuje Fermatovu poslední větu bez jakýchkoli dalších předpokladů kromě základních axiomů matematiky, a cestou k němu vznikla i formalizace algebry, harmonické analýzy, geometrie a teorie čísel, což ukazuje, že nástroje pro automatizovanou formalizaci jsou už dost robustní na to, aby se na nich dalo dál stavět.
Titulky typu umělá inteligence vyřešila třistapadesát let starý matematický problém jsou tedy zavádějící. Jak přesně upozorňuje i kritický komentář na blogu Exploring ChatGPT, problém vyřešil Andrew Wiles, Claude jeho existující řešení převedl do strojově ověřitelné podoby, což je jiný, byť sám o sobě náročný a časově zdlouhavý úkol. Skutečná novinka spočívá v tempu: proces, který lidským matematikům typicky zabere měsíce nebo roky pečlivé ruční práce, dokázal systém agentů zvládnout za necelé dva týdny, a to u jednoho z nejsložitějších matematických důkazů dvacátého století.