Axiom Math zveřejňuje důkaz klasifikace grup v Lean o 43,1 milionu řádků

Společnost Axiom Math 27. října 2026 oznámila, že zveřejňuje to, co označuje za první úplný počítačově ověřený důkaz klasifikace konečných jednoduchých grup. Inženýři a matematici na něm pracovali 24 dní a řídili roje desítek agentů umělé inteligence, kteří v asistentu dokazování Lean napsali přibližně 43,1 milionu řádků kódu.

„Dnes zveřejňujeme první úplný počítačově ověřený důkaz klasifikace konečných jednoduchých grup (CFSG),“ napsala společnost ve svém oznámení. Tato klasifikace určuje základní stavební kameny konečných grup. Původní důkaz má přibližně 15 000 stran ve více než 500 článcích, jejichž autory je zhruba 100 matematiků. Díky tomuto rozsahu si vysloužil přezdívku obrovská věta.

Co Axiom zveřejnil

CFSG dokazuje, že každá konečná jednoduchá grupa je buď cyklická prvočíselného řádu, alternující na alespoň pěti prvcích, patří do jedné ze šestnácti nekonečných rodin grup Lieova typu konstruovaných nad konečnými tělesy, nebo je jednou z přesně 26 izolovaných sporadických grup. Oznámení uvádí, že někteří autoři počítají Titsovu grupu jako 27. sporadickou grupu. Největší sporadickou grupu, Monstrum, zkonstruoval Robert Griess v roce 1980 pomocí algebry dimenze 196 884.

Lidské úsilí o důkaz trvalo desítky let. V roce 1963 Walter Feit a John Thompson dokázali, že každá neabelovská konečná jednoduchá grupa má sudý řád. Jejich článek o 255 stranách zaplnil celé číslo časopisu Pacific Journal of Mathematics. Daniel Gorenstein v roce 1972 předložil šestnáctikrokový plán dokončení klasifikace a v roce 1983 prohlásil, že je hotova. Případ kvazitenkých grup se však opíral o nedokončený rukopis Geoffreyho Masona, dokud Michael Aschbacher a Stephen Smith v roce 2004 nezveřejnili zpracování o 1 221 stranách a neuzavřeli tak to, čemu se začalo říkat důkaz první generace. Systematičtější důkaz druhé generace, jehož přípravu zahájili Gorenstein a Richard Lyons a k nimž se později připojili Ronald Solomon a Inna Capdeboscq, zůstává nedokončený, proto Axiom formalizoval důkaz první generace.

Stránka projektu uvádí, že formalizace vychází z důkazu první generace a že každý logický krok kontroluje jádro Lean. Zmiňuje také 43,1 milionu řádků kódu v Lean, 2,05 milionu deklarací a korpus čítající 715 článků a knih. Axiom uvádí, že mapa důkazu vycházela ze svazků důkazu druhé generace a že formalizace zahrnuje přibližně 1,2 milionu řádků kódu z dřívějšího projektu Qiuzhen-CFSG. Navazuje také na Mathlib, k jehož tvorbě podle společnosti přispěly stovky lidí. Mezi hlavní přispěvatele projektu patří Dean Cureton, Vasily Ilin, Bhavik Mehta a Niels Voss; hlavním řešitelem je Letong Hong.

Veřejný repozitář na GitHubu popisuje výsledek jako důkaz v Lean4, který neobsahuje žádné použití příkazu sorry, je připnutý k verzi 4.35.0-rc3, vychází z Mathlib a projektu TauCeti a používá pouze standardní axiomy Classical.choice, propext a Quot.sound, nikoli native_decide. Formální tvrzení klasifikace převzaté z TauCeti zní: „Každá konečná jednoduchá grupa je izomorfní některé z výslovně zkonstruovaných grup uvedených v klasifikačním seznamu.“ README uvádí, že příkaz lake build kontroluje celý vývojový celek a že veřejně dostupné změny nástroje Lake pro sestavování spolu s optimalizacemi, které tým plánuje předat zpět do původního projektu, zkrátily dobu sestavení na méně než 24 hodin. Kód je šířen pod licencí Apache-2.0.

24denní práce roje

Dne 1. října 2026 Axiom otevřel kanál na Slacku, aby koordinoval projekt. Dřívější práce v Lean a interní mapa důkazu sestavená na základě publikované literatury rozdělily úsilí na 108 milníků a přibližně 380 menších úkolů. První roj byl spuštěn 2. října 2026; agenti si přebírali milníky prostřednictvím problémů na GitHubu a hotovou práci hlásili na Slacku. Vedoucí agenti rozkládali obtížné argumenty na dílčí části a kontrolovali tvrzení, zatímco ostatní hledali existující výsledky nebo psali důkazy v Lean. Agent také mohl zadat chybějící předpoklady dalším agentům, jejichž výsledky se pak ukládaly do sdíleného repozitáře.

První pokrok odhalil slabá místa. Za některými zdánlivě zvládnutelnými milníky se skrývaly obrovské předpoklady, které agenti pokládali za platné, místo aby je dokázali. Tým proto odstranil desítky tisíc řádků založených na těchto předpokladech a začal znovu podle spolehlivějšího plánu. Jeden z prvních milníků se týkal věty o funktoru signalizátoru; navržený důkaz se opíral o strukturální předpoklady, které ještě bylo třeba zdůvodnit. Úzkým hrdlem se stala také doba sestavování, protože agenti vytvářeli důkazy rychleji, než je Lean dokázal znovu ověřovat. Axiom uvádí, že jeho inženýři rozdělovali výsledky sestavení uložené v mezipaměti mezi pracovní uzly, spouštěli nezávislé kontroly paralelně a náročné konečné výpočty přesouvali do samostatně ověřitelných certifikátů. Podle společnosti tyto změny zrychlily ověřování o řády.

Dne 10. října 2026 oznámila zpráva na kanálu, že agenti dokázali jednoduchost Monstra, uvádí společnost. Agenti také formalizovali existenci Monstra pomocí Griessovy algebry a dokázali větu, která ztotožňuje grupy typu Monstrum s Monstrem. Dne 13. října 2026 byl dokončen pouze jeden milník a inženýři zahájili nové plánování. Nedokončené milníky rozdělili na menší, přesně formulované věty; u každého rozdělení bylo nutné ukázat, jak lze z dílčích částí krátkým důkazem v Lean odvodit původní milník.

Nedostatky v publikovaném důkazu

Převod důkazu do Lean odhalil problémy v publikovaných argumentech, uvádí Axiom. Většina z nich byla drobná — typografické chyby, chyby v tabulkách nebo vypuštěné předpoklady — společnost však eviduje 34 významných odchylek od publikovaného záznamu; nejzávažnější se týká věty o nevyvážené grupě (Unbalanced Group Theorem, UGT).

Jeden příklad se objevil ve svazcích Aschbachera a Smithe o kvazitenkých grupách, kde lemma tvrdilo, že dvě číselné hodnoty jsou si rovny. Agenti našli protipříklad týkající se grupy SL₂(5), v němž jedna hodnota byla 1, ačkoli podle tvrzené rovnosti měla být 2. Nahrazení rovnosti nerovností lemma opravilo, pozdější argumenty však rovnost používaly k vyloučení určitých případů, takže tým rozšířil dřívější argument tak, aby zahrnoval i tyto konfigurace.

UGT pomáhá určit celou grupu na základě informací o jejích podgrupách: podle abstraktu doprovodného článku platí, že za indukčních předpokladů klasifikace netriviální podgrupa lichého řádu, která je normální v centralizátoru involuce, vynucuje, aby okolní jednoduchá grupa byla grupou Lieova typu v liché charakteristice nebo alternující grupou určitého stupně. Axiom přistoupil k UGT prostřednictvím monografie Johna Waltera z roku 1986 a při formalizaci tohoto argumentu jeho agenti našli konkrétní protipříklady k tvrzení o uzavřenosti, které argument používal: operace, o níž se předpokládalo, že udrží příslušné jednoduché grupy v určité třídě, mohla vytvořit grupu, která byla z této třídy výslovně vyloučena.

Podle popisu společnosti se vychází z PSL₂(49), jejíž tělesná involuce má centralizátor PGL₂(7); operace vede k jednoduché komponentě PSL₂(7), která je z dané třídy vyloučena, protože 7 je Mersennovo prvočíslo. Axiom upozorňuje, že tyto protipříklady nevyvrátily samotnou UGT, ani závěr Walterova tvrzení II.5.9(ii).

Oprava vycházela ze Solomonovy teorie maximálních 2-komponent z roku 1976, která podle Axiom poskytla hlavní myšlenky pro alternativní argument, jejž systém AxiomProver vytvořil a formalizoval. Klíčový krok, uvedený v článku jako věta 2.3 (zachování jednoduchých vrcholů), popisuje Axiom jako nový výsledek v teorii grup, který dokázal AxiomProver; ve spojení s redukcemi Gilmana a Solomona a větami o rozpoznávání Footea a Harrise poskytuje podobu UGT pro jednoduché grupy, kterou klasifikace vyžaduje. Po formalizaci matematici z Axiom našli kratší odvození pomocí metod první generace, zaznamenané jako poznámka 9.5, které vede ke stejnému závěru bez věty 2.3.

Tento článek, The Unbalanced Group Theorem, jehož autory jsou Colin Defant a Ken Ono, vyšel na preprintovém serveru Hexagon jako verze 1 dne 27. října 2026 pod licencí CC BY 4.0; stránka projektu uvádí rozsah 35 stran. Axiom uvádí, že spolupracuje s teoretiky grup na sestavení seznamu oprav nalezených v odborné literatuře a zveřejní je na stránce s opravami projektu. Konzultace ohledně opravy UGT proběhly s Lyonsem a Solomonem, jejichž práce je základem klasifikace, a společnost uvádí, že bude opravy nadále shromažďovat a řešit společně s poradním sborem, jehož členy jsou i oni a externí poradce Dan Nakano. Axiom svou roli popisuje jako zpřístupnění důkazu pro mechanické ověření, zdokumentování nalezených překážek a poskytnutí formalizovaných argumentů, které je řeší; zároveň uvádí, že zásluha za klasifikaci nadále patří matematikům, kteří příslušné grupy objevili a rozvinuli argumenty.