Axiom Math, společnost se sídlem v San Francisku, která buduje systémy umělé inteligence pro matematiku, vydala první kompletní počítačově ověřený důkaz klasifikace konečných jednoduchých grup (CFSG), široce popisovaný jako nejdelší důkaz v historii matematiky. Podle oznámení společnosti inženýři a matematici řídili zástupy desítek agentů umělé inteligence během pouhých 24 dnů, aby vytvořili přibližně 43,1 milionu řádků kódu v nástroji Lean proof assistant, čímž ověřili výsledek, který dříve zahrnoval zhruba 15 000 stránek ve více než 500 článcích v časopisech napsaných asi 100 matematiky za několik desetiletí.
Úspěch přichází ve chvíli, kdy se strojově podporovaná matematika rychle zrychluje a prodejny sledující zprávy z výzkumu AI sledovaly, jak se formální ověřování posouvá ze specializované praxe na hraniční schopnosti. Co dělá toto vydání neobvyklé, je rozsah: formalizace obsahuje zhruba 2,05 milionu deklarací uspořádaných do 100 milníků, z nichž každá je kontrolována jádrem Lean, malým důvěryhodným jádrem, které ověřuje každý logický krok.
Co vlastně říká klasifikace
Konečné jednoduché grupy jsou nedělitelnými stavebními kameny konečné symetrie a klasifikace – přezdívaná „obrovská věta“ – poskytuje jejich úplný seznam. Podle dokumentace projektu je každá konečná jednoduchá grupa jedním ze čtyř druhů: cyklická grupa prvořadého řádu, alternující grupa na alespoň pěti symbolech, jedna z šestnácti nekonečných rodin grup typu Lie konstruovaných na konečných polích nebo jedna z přesně 26 sporadických grup, které nezapadají do žádné rodiny.
Dokázat, že tento seznam vyčerpává všechny možnosti, zabralo větší část století společného úsilí. John Thompson, jehož práce byla ústředním bodem klasifikace, obdržel Fieldsovu medaili v roce 1970 a Abelovu cenu v roce 2008. Důkaz byl tak dlouhý a tak distribuovaný napříč články a generacemi matematiků, že přetrvávající pochybnosti o jeho úplnosti přetrvávaly po celá desetiletí – pochybnosti tato formalizace nyní formálně rozptyluje.
Roje agentů napříč 500 zdroji
Původní důkaz je rozptýlen ve více než 500 článcích a knihách, z nichž mnohé byly napsány před desítkami let v neslučitelných zápisech. Inženýr Axiom popsal metodu v diskuzi Hacker News o vydání: roj agentů měl za úkol projít všechny tyto zdroje, přičemž nejtěžší částí bylo sestavit vše do koherentního celku, protože stejný neformální koncept může být formalizován mírně odlišnými, ale matematicky nekompatibilními způsoby.
Blogový příspěvek společnosti uvádí, že úsilí trvalo 24 dní od začátku do vydání, přičemž lidští inženýři a matematici řídili roje agentů spíše než aby pracovali řádek po řádku. Výsledek následuje dřívější významné milníky automatické formalizace v roce 2026, včetně Lean důkazů hlavních klasických teorémů vytvořených pomocí hraničních modelů, ale v měřítku, kterému se žádný předchozí projekt nepřiblížil.
34 Odchylky od publikovaného záznamu
Převedení publikovaného důkazu do strojově ověřitelné formy odhalilo skutečné problémy v matematické literatuře. Axiom hlásí, že většina problémů byla menších – typografické chyby, chyby v tabulkách nebo vypuštěné hypotézy. Bylo však 34 pozoruhodných odchylek od zveřejněného záznamu, které bylo třeba vyřešit, než projde formalizace.
Nejpodstatnější se týkala věty o nevyvážené grupě. Při formalizaci cesty první generace k výsledku tým našel protipříklady k závěrečnému tvrzení použitému v publikovaném argumentu. Po konzultaci s teoretiky expertních skupin vytvořili alternativní cestu postavenou na strukturálních technikách z éry Daniela Gorensteina – konkrétně teorii maximálních 2 komponent ze 70. let – a opravu publikovali jako nový 35stránkový dokument o teorii skupin, zveřejněný jako preprint 2610.00575. Společnost říká, že ve prospěch matematické komunity uvolní dlouhý seznam chyb, sestavený po konzultaci s teoretiky skupin, na jejichž práci klasifikace spočívá.
Proč je strojově kontrolovaná matematika důležitá
Hodnota formalizace nespočívá jen v tom, že počítač schválil důkaz. Formalizace Lean redukuje důvěryhodnou základnu na jádro asistenta důkazu – malý, těžce auditovaný program – namísto nahromaděné spolehlivosti tisíců stránek přečtených roztroušenými specialisty. Komentátoři ve vláknu Hacker News, kde příběh získal stovky kladných hlasů, poznamenali, že empirickým znalostem o tom, proč klasifikace platí, hrozilo, že doslova vymřou, protože původní generace matematiků odešla do důchodu, protože nikdo nedokázal udržet celý argument v hlavě.
Praktické ohlasy jsou i jinde ve fyzice. Největší z 26 sporadických skupin, skupina Monster, se objevuje v programu „monstrózního měsíčního svitu“ spojujícím konečnou symetrii s modulárními funkcemi – práce, která Richardu Borcherdsovi vynesla Fieldsovu medaili v roce 1998 – a v návrhu Edwarda Wittena z roku 2007 spojujícím symetrie Monster s entropií černé díry v trojrozměrném vesmíru. Ověřená klasifikace staví základní strukturální matematiku na pevnější půdu pro přesně tyto druhy mezioborových aplikací.
Co přijde dál
Axiom říká, že vedle projektu errata jsou na cestě další dokumenty odvozené z formalizace. Pro komunitu formálních metod nastavuje vydání nové měřítko toho, o co se ověřovací projekty řízené agenty mohou pokusit; pro matematiku převádí rozlehlý, půl století trvající společný úspěch do jediného artefaktu, který může zkontrolovat každý počítač. Klasifikaci se již jen nevěří. Nyní je to v tom nejdoslovnějším slova smyslu prokázáno – a důkaz je k dispozici každému, kdo si jej může stáhnout a ověřit.
