Firma Axiom Math zveřejnila strojově ověřený důkaz klasifikace konečných jednoduchých grup. Kód v Leanu má 43,1 milionu řádků a vznikl za 24 dní, většinu napsali AI agenti. Při překladu do formálního jazyka tým narazil na chybu v publikovaném argumentu z roku 1986. Nikdo mimo firmu výsledek dosud nepřepočítal.
Patnáct tisíc stran, víc než sto matematiků, několik desetiletí práce. Tak vypadá klasifikace konečných jednoduchých grup, nejdelší důkaz, jaký kdy lidé sepsali. Firma Axiom Math ho podle oznámení z 26. října celý přeložila do jazyka Lean a nechala projít strojovou kontrolou. Trvalo to 24 dní.
Zajímavé na tom není samotné číslo. Lean má jádro, které každý logický krok buď přijme, nebo odmítne, a výsledek leží veřejně na GitHubu pod licencí Apache 2.0. U tak velkého projektu se tedy poprvé dá změřit, co agenti dokázali, místo aby se to odhadovalo z benchmarku. Buď lake build projde, nebo neprojde.
Pro čtenáře, který sleduje schopnosti jazykových modelů, je podstatné hlavně zadání. Formalizace takového rozsahu nejde vyřešit jedním dlouhým promptem. Někdo musí důkaz rozsekat na stovky kusů, u každého držet přesné rozhraní s okolím, a pak ty kusy slepit tak, aby na konci prošly jedinou kontrolou. Většina dnešních benchmarků tenhle typ práce vůbec nemapuje, protože se měří na úlohách, které se vejdou do jednoho kontextu. A na rozdíl od benchmarku tady nejde ohnout metriku: jádro Leanu buď důkaz přijme, nebo ne.
Nejdřív mi to přišlo jako exhibice s čísly. Pak jsem si pročetl, co tým našel ve Walterově memoáru z roku 1986.
Co přesně Lean ověřil
Formalizované tvrzení říká, že každá konečná jednoduchá grupa je buď cyklická prvočíselného řádu, nebo alternující na nejméně pěti prvcích, nebo patří do jedné ze šestnácti rodin Lieova typu, nebo je jednou z 26 sporadických grup. Část autorů přitom počítá sporadických grup 27, protože mezi ně řadí i Titsovu grupu. Axiom zpracoval takzvaný důkaz první generace, protože druhá generace dodnes není dokončená. Projektová stránka uvádí 43,1 milionu řádků Lean kódu, 2,05 milionu deklarací a sto milníků; portál Unite.AI mluví o 108 milnících a asi 380 dílčích úkolech. Kód staví na knihovně Mathlib a na projektu TauCeti, odkud tým vzal i cílové tvrzení, a přibližně 1,2 milionu řádků přebírá ze starší formalizace Qiuzhen-CFSG. README v repozitáři slibuje důkaz bez jediného sorry, postavený na Lean 4.35.0-rc3 a na třech standardních axiomech: Classical.choice, propext a Quot.sound. Taktiku native_decide, která by kontrolu zkrátila, tým nepoužil. Celý projekt se dá zkompilovat příkazem lake build, i když autoři přiznávají, že k tomu zatím potřebují nezveřejněné úpravy Lake a že by čas sestavení rádi stlačili pod 24 hodin.
Práci řídil systém AxiomProver, který podle firmy nasadil roje desítek agentů na dekompozici, vyhledávání, psaní důkazů a revizi. Nad nimi stáli inženýři a matematici. Mezi hlavní autory patří Dean Cureton, Vasily Ilin, Bhavik Mehta a Niels Voss, hlavní řešitelkou je Letong Hong, v poradním sboru sedí Lyons a Solomon.
Chyba ve Walterově memoáru
Tahle část mě zajímá víc než počet řádků. Překlad do Leanu odhalil 34 odchylek od publikované literatury, které tým označil za podstatné. Největší se týká věty o nebalancovaných grupách (Unbalanced Group Theorem). Walterův memoár z roku 1986 se opíral o tvrzení o uzavřenosti, ke kterému agenti našli protipříklady, mimo jiné grupu PSL₂(49). Jiné lemma neplatí pro SL₂(5), kde slíbená rovnost padá. Ani jeden z těch nálezů samotnou větu nevyvrátil a nezpochybnil ani závěr Walterovy propozice II.5.9(ii). Chyběl ale funkční argument, takže ho agenti museli postavit znovu. Opírá se o nový výsledek, kterému tým říká zachování jednoduchých vrcholů (Preservation of simple tops) a který prý dokázal rovněž AxiomProver. Stroj tedy našel v padesátileté literatuře díru, kterou generace matematiků přečetly a nevšimly si jí. Jestli ta oprava obstojí, netuším. Příslušná práce visí jako preprint na Hexagonu a recenzí neprošla, errata navíc Axiom pořád sestavuje. Zatím to vypadá, že formalizace začíná fungovat jako debugger lidské matematiky.
Nikdo to zvenku nepřepočítal
Portál RuntimeWire se 27. října zeptal zakladatelky a ředitelky Axiomu Cariny Hong, jestli důkaz už někdo mimo firmu samostatně sestavil a zkontroloval. Odpověděla přes mluvčího: „Ještě ne. Zveřejňujeme sestavovací artefakty, abychom externím stranám pomohli a motivovali je k nezávislé reprodukci.“ Firma zároveň tvrdí, že o platnosti samotné věty nikdy nebyly pochyby.
Tady je potřeba rozlišovat dvě věci. Lean potvrzuje, že odvození plynou ze zakódovaných předpokladů. To, že zakódované tvrzení odpovídá tomu, co si pod klasifikací představuje matematik, musí posoudit člověk. Důkaz pod skrytým dodatečným předpokladem kontrolou projde, a přesto nic neřeší. Formulace „první kompletní strojově kontrolovaný důkaz“ je navíc tvrzení Axiomu, nikoli nezávislý verdikt, a 1,2 milionu přebraných řádků ukazuje, že se nestavělo na zelené louce.
Příkaz na ověření je ale veřejný a repozitář taky, takže kdokoli s dostatkem výpočetního času může zkusit, jestli mu to prolítne. Tím se tenhle případ liší od obvyklých oznámení o schopnostech modelů, u kterých se čtenář musí spolehnout na graf v blogpostu. Replikace nepotřebuje přístup k vahám modelu ani k firemní infrastruktuře, jen Lean, Mathlib a dost hodin na nějakém stroji. Kolik přesně, se zatím neví, protože autoři mluví o cíli pod 24 hodin, ne o aktuálním čase.
Mimochodem, Lean nevznikl na akademii. Napsal ho Leonardo de Moura v Microsoft Research, první verze vyšla v roce 2013, a kolem knihovny Mathlib se od té doby utvořila komunita, která formalizuje matematiku po částech. Axiom tedy nepřišel s novým nástrojem, přišel s tím, že ho obsluhují agenti.
Reálná hodnota projektu se ukáže ve chvíli, kdy někdo zcela mimo Axiom spustí lake build a dostane stejný výsledek.
Do té doby je to 43 milionů řádků, kterým věříme na slovo firmy, která je napsala.
Zdroje
- AxiomMath/CFSG na GitHubu – repozitář s README, licencí a postupem sestavení
- cfsg.axiommath.ai – projektová stránka s čísly, mapou důkazu a seznamem autorů
- Formalizing the Enormous Theorem – metodika a popis nálezů v literatuře
- Axiom’s CEO says no one outside the company has rebuilt its 43-million-line proof yet – RuntimeWire, 27. 10. 2026
- Axiom Math Releases 43.1M-Line Lean Proof of Group Classification – Unite.AI, 27. 10. 2026
- Axiom Says AI System Formalized 15,000-Page Group Theory Proof – TokenPost, 27. 10. 2026
- Lean (proof assistant) – původ jazyka a knihovny Mathlib
