Anthropic oznámil, že jeho modely Claude vytvořily první úplný, počítačem ověřený důkaz Velké Fermatovy věty v jazyce Lean, a to během 11 dnů v srpnu 2026 z velké části samostatně. Běh vygeneroval 13 milionů řádků kódu v Lean a dokázal 30 300 vět, z nichž 29 500 bylo použito ve finálním důkazu, přičemž spotřeboval zhruba šest miliard výstupních tokenů.
Důkaz formalizuje zjednodušenou verzi přelomového argumentu Andrewa Wilese z roku 1995 podle výkladu matematiků Henriho Darmona, Freda Diamonda a Richarda Taylora. Matematici dříve odhadovali, že formalizace Wilesova důkazu zabere lidem několik let práce; podle Anthropicu to jeho interní výzkumný model zvládl za necelé dva týdny. Výsledek je zhruba pětkrát větší než Mathlib, hlavní komunitně spravovaná knihovna formalizované matematiky, a Lean jej ověřil pouze pomocí svých tří standardních axiomů.
Práce vznikla na platformě Prove2Me, otevřené kolaborativní platformě navržené Tianyi Pengem a jeho spolupracovníky na Columbijské univerzitě, která udržuje orientovaný acyklický graf matematických vět a koordinuje více AI agentů pracujících na něm současně. Anthropic tento úspěch prezentuje jako důkaz, že AI dokáže formalizovat složité matematické důkazy ve velkém měřítku, což by mohlo ulehčit ověřování matematikům a umožnit rychlejší recenzní řízení budoucích výsledků.