Axiom Math lanserer Lean-bevis på 43,1 millioner linjer for klassifikasjonen av grupper

Axiom Math opplyste 27. oktober 2026 at selskapet lanserer det det omtaler som det første fullstendige dataverifiserte beviset for klassifikasjonen av endelige enkle grupper. Beviset ble utviklet på 24 dager av ingeniører og matematikere som ledet svermer av flere titalls KI-agenter, som skrev omtrent 43,1 millioner linjer med kode i bevisassistenten Lean.

«I dag lanserer vi det første fullstendige dataverifiserte beviset for klassifikasjonen av endelige enkle grupper (CFSG)», skrev selskapet i kunngjøringen sin. Klassifikasjonen identifiserer de grunnleggende byggesteinene i endelige grupper. Det opprinnelige beviset strekker seg over rundt 15 000 sider fordelt på mer enn 500 artikler skrevet av omtrent 100 matematikere – et omfang som har gitt det tilnavnet det enorme teoremet.

Hva Axiom har lansert

CFSG fastslår at enhver endelig enkel gruppe er syklisk av primtallsorden, alternerende på minst fem symboler, tilhører én av seksten uendelige familier av grupper av Lie-type konstruert over endelige legemer, eller er én av nøyaktig 26 isolerte sporadiske grupper. Kunngjøringen bemerker at noen forfattere regner Tits-gruppen som en 27. gruppe. Den største sporadiske gruppen, Monstergruppen, ble konstruert av Robert Griess i 1980 ved hjelp av en algebra med dimensjon 196 884.

Arbeidet med det menneskeskapte beviset strakte seg over flere tiår. I 1963 beviste Walter Feit og John Thompson at enhver ikke-abelsk endelig enkel gruppe har partallsorden. Beviset sto i en artikkel på 255 sider som fylte et helt nummer av Pacific Journal of Mathematics. Daniel Gorenstein la i 1972 fram et program i seksten trinn for å fullføre klassifikasjonen og erklærte den fullført i 1983, men det kvasitynne tilfellet bygde på et uferdig manuskript av Geoffrey Mason helt til Michael Aschbacher og Stephen Smith publiserte en framstilling på 1 221 sider i 2004. Dermed ble det som senere ble kjent som førstegenerasjonsbeviset, avsluttet. Et mer systematisk andregenerasjonsbevis, påbegynt av Gorenstein og Richard Lyons og senere videreført med Ronald Solomon og Inna Capdeboscq, er fortsatt ufullstendig. Derfor formaliserte Axiom førstegenerasjonsbeviset.

Prosjektsiden beskriver formaliseringen som en gjengivelse av førstegenerasjonsbeviset der hvert logiske trinn kontrolleres av kjernen i Lean, og oppgir at den omfatter 43,1 millioner linjer Lean-kode, 2,05 millioner erklæringer og 715 artikler og bøker i korpuset. Axiom sier at beviskartet bygde på bindene fra andregenerasjonsbeviset, og at formaliseringen inneholder rundt 1,2 millioner kodelinjer fra det tidligere Qiuzhen-CFSG-prosjektet og bygger på Mathlib, som selskapet gir hundrevis av bidragsytere æren for. Prosjektet oppgir Dean Cureton, Vasily Ilin, Bhavik Mehta og Niels Voss som sentrale bidragsytere, med Letong Hong som hovedansvarlig forsker.

Det offentlige GitHub-arkivet beskriver resultatet som et Lean4-bevis uten «sorry», låst til versjon 4.35.0-rc3, bygget på Mathlib og TauCeti-prosjektet og med bare standardaksiomene Classical.choice, propext og Quot.sound, uten native_decide. Den formelle formuleringen av klassifikasjonen, hentet fra TauCeti, lyder: «Enhver endelig enkel gruppe er isomorf med én av gruppene som er uttrykkelig konstruert på klassifikasjonslisten.» I README-filen står det at lake build kontrollerer hele utviklingen, og at åpne endringer i Lake-byggverktøyet og optimaliseringer som teamet planlegger å bidra tilbake til prosjektet, reduserte byggetiden til under 24 timer. Koden har en Apache-2.0-lisens.

En 24-dagers innsats med KI-agenter

1. oktober 2026 opprettet Axiom en Slack-kanal for å koordinere prosjektet. Eksisterende Lean-arbeid og et internt beviskart satt sammen på grunnlag av publisert litteratur delte innsatsen inn i 108 milepæler og rundt 380 mindre oppgaver. Den første agentflokken ble satt i drift 2. oktober 2026. Agentene tok på seg milepæler via GitHub-saker og rapporterte fullført arbeid i Slack. Ledende agenter delte opp vanskelige argumenter og gjennomgikk utsagn, mens andre agenter lette etter eksisterende resultater eller skrev Lean-bevis. En agent kunne også delegere manglende forutsetninger til andre agenter, og resultatene deres ble lagt inn i et felles arkiv.

Den tidlige framgangen avdekket svake punkter. Noen milepæler som tilsynelatende var overkommelige, skjulte enorme forutsetninger som agentene hadde lagt til grunn i stedet for å bevise. Teamet slettet titusenvis av kodelinjer som bygde på disse antakelsene, før arbeidet ble startet på nytt med en mer holdbar plan. En tidlig milepæl gjaldt signalizer-funktorteoremet, der et foreløpig bevis bygde på strukturelle antakelser som ennå måtte begrunnes. Byggetidene ble også en flaskehals etter hvert som agentene produserte bevis raskere enn Lean kunne kontrollere dem på nytt. Axiom sier at ingeniørene distribuerte hurtigbufrede byggresultater mellom arbeidere, kjørte uavhengige kontroller parallelt og flyttet kostbare endelige beregninger ut i sertifikater som kunne kontrolleres separat. Ifølge selskapet økte disse endringene verifiseringshastigheten med flere størrelsesordener.

10. oktober 2026 kunngjorde en melding i kanalen at agentene hadde bevist at Monstergruppen er enkel, forteller selskapet. Agentene formaliserte også eksistensen av Monstergruppen ved hjelp av Griess-algebraen, samt et teorem som identifiserer grupper av Monster-type med Monstergruppen. 13. oktober 2026 ble bare én milepæl fullført, og ingeniørene organiserte en ny planleggingsrunde der uferdige milepæler ble delt opp i mindre, presist formulerte teoremer. Hver oppdeling måtte vise hvordan delene kunne brukes til å etablere den opprinnelige milepælen gjennom et kort Lean-bevis.

Manglende ledd funnet i det publiserte beviset

Oversettelsen av beviset til Lean avdekket problemer i de publiserte argumentene, rapporterer Axiom. De fleste var mindre feil – trykkfeil, feil i tabeller eller utelatte hypoteser – men selskapet teller 34 bemerkelsesverdige avvik fra det publiserte materialet. Det mest omfattende gjelder Unbalanced Group Theorem, eller UGT.

Ett eksempel stammer fra Aschbacher og Smiths bind om kvasi-tynne grupper, der et lemma hevdet at to tallstørrelser var like. Agentene fant et moteksempel som involverte gruppen SL₂(5), der den ene størrelsen var 1, mens den hevdet likheten krevde 2. Å erstatte likheten med en ulikhet rettet opp lemmaet, men senere argumenter hadde brukt likheten til å utelukke tilfeller. Derfor utvidet teamet et tidligere argument slik at det også dekket disse konfigurasjonene.

UGT bidrar til å identifisere en hel gruppe ut fra informasjon om undergruppene dens: Ifølge sammendraget i den tilhørende artikkelen innebærer klassifikasjonens induktive hypoteser at dersom en ikke-triviell undergruppe av odden orden er normal i sentralisatoren til en involusjon, må den omgivende enkle gruppen være av Lie-type i odd karakteristikk eller alternerende av visse grader. Axiom tok utgangspunkt i John Walters memoar fra 1986 om UGT. Under formaliseringen av dette argumentet fant agentene eksplisitte moteksempler til en lukningsegenskap det bygget på: En operasjon som ble antatt å holde de tilhørende enkle gruppene innenfor en bestemt familie, kunne produsere en gruppe som uttrykkelig var utelukket fra familien.

Ifølge selskapets redegjørelse tar man utgangspunkt i PSL₂(49), der kroppsinvolusjonen har sentralisatoren PGL₂(7). Operasjonen gir da den enkle komponenten PSL₂(7), som er utelukket fra familien fordi 7 er et Mersenneprimtall. Axiom understreker at moteksemplene verken motbeviste UGT i seg selv eller konklusjonen i Walters Proposition II.5.9(ii).

Reparasjonen bygget på Solomons teori fra 1976 om maksimale 2-komponenter, som ifølge Axiom ga de sentrale ideene til et alternativt argument som AxiomProver-systemet utarbeidet og formaliserte. Hovedtrinnet, omtalt i artikkelen som Theorem 2.3 (bevaring av enkle topper), beskrives av Axiom som et nytt resultat i gruppeteori bevist av AxiomProver. Sammen med reduksjonene til Gilman og Solomon og gjenkjennelsesteoremene til Foote og Harris gir det den formen av UGT for enkle grupper som klassifikasjonen trenger. Etter formaliseringen fant Axioms matematikere et kortere deduksjonsbevis innenfor førstegenerasjonsmetodene. Det er dokumentert som Remark 9.5 og når samme konklusjon uten Theorem 2.3.

Artikkelen, The Unbalanced Group Theorem, er levert av Colin Defant og Ken Ono og ble publisert som versjon 1 på preprintserveren Hexagon 27. oktober 2026 under lisensen CC BY 4.0. Prosjektsiden oppgir at den er på 35 sider. Axiom sier at selskapet samarbeider med gruppeteoretikere om å samle errata som er funnet i litteraturen, og at de vil bli publisert på prosjektets errataside. Lyons og Solomon, hvis arbeid ligger til grunn for klassifikasjonen, ble rådspurt om reparasjonen av UGT. Selskapet sier at det vil fortsette å samle inn og rette errata i samarbeid med et rådgivende styre som inkluderer dem, samt den eksterne rådgiveren Dan Nakano. Axiom beskriver sitt bidrag som å gjøre beviset mekanisk kontrollerbart, dokumentere hindringene som dukket opp og levere formaliserte argumenter som løser dem, samtidig som selskapet presiserer at klassifikasjonen fortsatt er en prestasjon utført av matematikerne som oppdaget gruppene og utviklet argumentene.