Axiom Math julkaisee 43,1 miljoonan rivin Lean-todistuksen ryhmien luokittelusta

Axiom Math kertoi 27. lokakuuta 2026 julkaisevansa sen mukaan ensimmäisen täydellisen tietokoneella tarkistetun todistuksen äärellisten yksinkertaisten ryhmien luokittelulle. Todistus tuotettiin 24 päivässä insinöörien ja matemaatikkojen ohjaamien kymmenien tekoälyagenttien parvilla, jotka kirjoittivat Lean-todistusavustimella noin 43,1 miljoonaa koodiriviä.

”Julkaisemme tänään ensimmäisen täydellisen tietokoneella tarkistetun todistuksen äärellisten yksinkertaisten ryhmien luokittelulle (CFSG)”, yhtiö kirjoitti tiedotteessaan. Luokittelu määrittää äärellisten ryhmien perusrakennuspalikat. Alkuperäinen todistus ulottuu noin 15 000 sivulle, jotka jakautuvat yli 500 artikkeliin noin sadalta matemaatikolta. Todistuksen mittakaavan vuoksi se on saanut lempinimen valtava lause.

Mitä Axiom julkaisi

CFSG:n mukaan jokainen äärellinen yksinkertainen ryhmä on joko syklinen ja kertalukuaan alkuluku, vähintään viidellä symbolilla määritelty alternoiva ryhmä, jokin kuudentoista äärettömän Lie-tyyppisen ryhmäperheen ryhmistä, jotka on rakennettu äärellisten kuntien päälle, tai yksi täsmälleen 26 erillisestä sporadisesta ryhmästä. Tiedotteessa huomautetaan, että jotkut kirjoittajat laskevat Tits-ryhmän 27:nneksi ryhmäksi. Suurimman sporadisen ryhmän, Monsterin, rakensi Robert Griess vuonna 1980 käyttäen 196 884-ulotteista algebraa.

Todistuksen laatiminen ihmistyönä kesti vuosikymmeniä. Vuonna 1963 Walter Feit ja John Thompson todistivat, että jokaisen epäabelisen äärellisen yksinkertaisen ryhmän kertaluku on parillinen. Heidän 255-sivuinen artikkelinsa täytti kokonaisen Pacific Journal of Mathematics -lehden numeron. Daniel Gorenstein esitti vuonna 1972 kuusitoistavaiheisen ohjelman luokittelun saattamiseksi valmiiksi ja julisti sen valmiiksi vuonna 1983. Kvasiohut tapaus perustui kuitenkin Geoffrey Masonin keskeneräiseen käsikirjoitukseen, kunnes Michael Aschbacher ja Stephen Smith julkaisivat vuonna 2004 aiheesta 1 221-sivuisen käsittelyn. Näin saatiin päätökseen se, mitä alettiin kutsua ensimmäisen sukupolven todistukseksi. Gorensteinin ja Richard Lyonsin aloittama järjestelmällisempi toisen sukupolven todistus, johon myöhemmin liittyivät Ronald Solomon ja Inna Capdeboscq, on yhä keskeneräinen, joten Axiom formalisti ensimmäisen sukupolven todistuksen.

Hankkeen sivulla formalisaation kerrotaan seuraavan ensimmäisen sukupolven todistusta siten, että Lean-ytimen tarkistettavissa on jokainen päättelyaskel. Sivulla ilmoitetaan myös, että kokonaisuuteen kuuluu 43,1 miljoonaa Lean-koodiriviä, 2,05 miljoonaa deklarointia sekä 715 artikkelia ja kirjaa. Axiomin mukaan todistuskartta pohjautui toisen sukupolven teoksiin, ja formalisaatioon sisältyy noin 1,2 miljoonaa koodiriviä aiemmasta Qiuzhen-CFSG-hankkeesta. Se rakentuu myös Mathlibin varaan, jonka kehityksestä yhtiö kiittää satoja osallistujia. Hankkeen keskeisiksi osallistujiksi nimetään Dean Cureton, Vasily Ilin, Bhavik Mehta ja Niels Voss, ja päätutkijana toimii Letong Hong.

Julkisessa GitHub-tietovarastossa tulosta kuvataan sorry-vapaaksi Lean4-todistukseksi, joka on lukittu versioon 4.35.0-rc3, rakentuu Mathlibin ja TauCeti-hankkeen varaan ja käyttää vain vakioaksioomia Classical.choice, propext ja Quot.sound — ei native_decide-ominaisuutta. TauCeti-hankkeesta otettu luokittelun formaali väite kuuluu: ”Jokainen äärellinen yksinkertainen ryhmä on isomorfinen jonkin luokitteluluettelossa nimenomaisesti rakennetun ryhmän kanssa.” README-tiedoston mukaan lake build tarkistaa koko kehityskokonaisuuden. Siinä kerrotaan myös, että avoimet muutokset Lake-koontityökaluun ja optimoinnit, jotka tiimi aikoo viedä osaksi työkalua, lyhensivät koontiajan alle 24 tuntiin. Koodin lisenssi on Apache-2.0.

24 päivän työ tekoälyagenttien parvella

Axiom avasi 1. lokakuuta 2026 Slack-kanavan hankkeen koordinointia varten. Aiempi Lean-työ ja julkaistuun kirjallisuuteen perustuva sisäinen todistuskartta jakoivat työn 108 välitavoitteeseen ja noin 380 pienempään tehtävään. Ensimmäinen agenttiparvi käynnistyi 2. lokakuuta 2026: agentit ottivat välitavoitteita työn alle GitHub-ongelmien kautta ja raportoivat valmiista töistä Slackissa. Johtoagentit pilkkoivat vaikeita päättelyketjuja ja tarkastelivat väitteitä, kun taas muut agentit etsivät olemassa olevia tuloksia tai kirjoittivat Lean-todistuksia. Agentti saattoi myös delegoida puuttuvien esitietojen selvittämisen muille agenteille, joiden tulokset lisättiin yhteiseen tietovarastoon.

Alkuvaiheen edistyminen paljasti heikkouksia. Osa näennäisen hallittavista välitavoitteista kätki alleen valtavia esitietovaatimuksia, jotka agentit olivat olettaneet todistamisen sijaan. Tiimi poisti kymmeniä tuhansia rivejä tällaisille oletuksille rakennettua koodia ja aloitti sitten uudelleen vakaammalta pohjalta. Yksi varhainen välitavoite liittyi signaalisaattorifunktiolauseeseen, jonka ehdokastodistus nojasi rakenteellisiin oletuksiin, jotka piti vielä perustella. Myös koontiajat alkoivat muodostua pullonkaulaksi, kun agentit tuottivat todistuksia nopeammin kuin Lean ehti tarkistaa ne uudelleen. Axiomin mukaan sen insinöörit jakoivat välimuistiin tallennettuja koontituloksia työntekijöiden kesken, suorittivat riippumattomia tarkistuksia rinnakkain ja siirsivät raskaat äärelliset laskutoimitukset erikseen tarkistettaviin varmenteisiin. Yhtiö kertoo näiden muutosten nopeuttaneen varmennusta useilla suuruusluokilla.

Yhtiön mukaan kanavalla ilmoitettiin 10. lokakuuta 2026, että agentit olivat todistaneet Monsterin yksinkertaiseksi. Agentit formalisoivat myös Monsterin olemassaolon Griessin algebran avulla sekä lauseen, joka osoittaa Monster-tyyppisiksi ryhmiksi kutsuttujen ryhmien olevan Monsterin kanssa isomorfisia. Lokakuun 13. päivänä 2026 valmistui vain yksi välitavoite, ja insinöörit käynnistivät työn uudelleensuunnittelun. Keskeneräiset välitavoitteet jaettiin pienemmiksi, täsmällisesti muotoilluiksi lauseiksi, ja jokaisessa pilkkomisessa oli osoitettava lyhyellä Lean-todistuksella, miten osat yhdessä toteuttaisivat alkuperäisen välitavoitteen.

Julkaistusta todistuksesta löytyi puutteita

Todistuksen kääntäminen Lean-muotoon paljasti julkaistuissa todisteluissa ongelmia, Axiom kertoo. Useimmat niistä olivat vähäisiä – kirjoitusvirheitä, taulukoissa olevia virheitä tai pois jätettyjä oletuksia – mutta yhtiö laskee julkaistusta aineistosta 34 merkittävää poikkeamaa. Huomattavin niistä liittyy tasapainottomien ryhmien lauseeseen (Unbalanced Group Theorem, UGT).

Yksi esimerkki löytyi Aschbacherin ja Smithin kvasiohuista ryhmistä käsittelevistä teoksista, joissa eräässä lemmassa väitettiin kahden lukuarvon olevan yhtä suuret. Agentit löysivät vastaesimerkin, jossa esiintyi ryhmä SL₂(5): toinen lukuarvo oli 1, vaikka väitetty yhtäsuuruus edellytti sen olevan 2. Yhtäsuuruuden korvaaminen epäyhtälöllä korjasi lemman, mutta myöhemmissä todisteluissa yhtäsuuruutta oli käytetty tapausten poissulkemiseen. Siksi tiimi laajensi aiempaa todisteluargumenttia kattamaan kyseiset tilanteet.

UGT auttaa tunnistamaan koko ryhmän sen aliryhmiä koskevien tietojen perusteella: oheisen artikkelin tiivistelmän mukaan luokittelun induktiivisten oletusten vallitessa involuution keskittäjässä normaalina oleva epätriviaali paritilauksinen aliryhmä pakottaa ympäröivän yksinkertaisen ryhmän olemaan Lie-tyyppinen ryhmä parittomassa karakteristiikassa tai tietynasteinen vuorotteleva ryhmä. Axiom lähestyi UGT:tä John Walterin vuoden 1986 muistion kautta. Formalisoidessaan tätä todistelua sen agentit löysivät eksplisiittisiä vastaesimerkkejä sen käyttämälle sulkeutuvuutta koskevalle väitteelle: operaatio, jonka oletettiin pitävän siihen liittyvät yksinkertaiset ryhmät tietyssä perheessä, saattoi tuottaa ryhmän, joka oli nimenomaisesti suljettu perheen ulkopuolelle.

Yhtiön kuvauksen mukaan lähtökohtana on PSL₂(49), jonka kuntainvoluution keskittäjä on PGL₂(7). Operaatio tuottaa yksinkertaisen komponentin PSL₂(7), joka ei kuulu kyseiseen perheeseen, koska 7 on Mersennen alkuluku. Axiom huomauttaa, etteivät vastaesimerkit kumonneet UGT:tä eivätkä edes Walterin väitteen II.5.9(ii) johtopäätöstä.

Korjauksessa hyödynnettiin Solomonin vuonna 1976 esittämää maksimaalisten 2-komponenttien teoriaa. Axiomin mukaan se tarjosi keskeiset ideat vaihtoehtoiseen todisteluun, jonka sen AxiomProver-järjestelmä tuotti ja formalisoi. Artikkelissa lauseena 2.3 (yksinkertaisten huippujen säilyminen) esitettyä keskeistä askelta Axiom kuvailee AxiomProverin todistamaksi uudeksi ryhmäteorian tulokseksi. Yhdessä Gilmanin ja Solomonin redusointien sekä Footen ja Harrisin tunnistuslauseiden kanssa se antaa luokittelussa tarvittavan UGT:n yksinkertaisia ryhmiä koskevan muodon. Formalisoinnin jälkeen Axiomin matemaatikot löysivät ensimmäisen sukupolven menetelmien puitteissa lyhyemmän päättelyketjun, joka on kirjattu huomautukseen 9.5 ja johtaa samaan päätelmään ilman lausetta 2.3.

Colin Defantin ja Ken Onon laatima artikkeli The Unbalanced Group Theorem julkaistiin Hexagon-esijulkaisupalvelimella versiona 1 27. lokakuuta 2026 CC BY 4.0 -lisenssillä. Projektisivun mukaan artikkelissa on 35 sivua. Axiom kertoo työskentelevänsä ryhmäteoreetikkojen kanssa kootakseen kirjallisuudessa havaitut virheet ja julkaistakseen ne projektin virheluettelosivulla. Luokittelun perustana olevan työn tehneitä Lyonsia ja Solomonia kuultiin UGT:n korjauksesta. Yhtiö kertoo jatkavansa virheiden kokoamista ja ratkaisemista neuvoa-antavan toimikunnan tuella. Toimikuntaan kuuluvat Lyons ja Solomon sekä ulkopuolinen neuvonantaja Dan Nakano. Axiom kuvaa oman panoksensa todistuksen saattamiseksi koneellisesti tarkistettavaan muotoon, kohdattujen esteiden dokumentoimiseksi ja ne ratkaisevien formalisoitujen todistelujen tarjoamiseksi. Samalla yhtiö toteaa, että luokittelu on niiden matemaatikkojen saavutus, jotka löysivät ryhmät ja kehittivät todistelut.