Axiom Math udsender Lean-bevis på 43,1 millioner linjer for klassifikationen af grupper

Axiom Math oplyste den 27. oktober 2026, at virksomheden offentliggør det, den kalder det første fuldstændige computerkontrollerede bevis for klassifikationen af endelige simple grupper. Beviset blev udarbejdet på 24 dage af ingeniører og matematikere, der styrede sværme af snesevis af AI-agenter, som skrev cirka 43,1 millioner linjer kode i bevisassistenten Lean.

»I dag offentliggør vi det første fuldstændige computerkontrollerede bevis for klassifikationen af endelige simple grupper (CFSG),« skrev virksomheden i sin meddelelse. Klassifikationen identificerer de grundlæggende byggesten i endelige grupper, og det oprindelige bevis strækker sig over cirka 15.000 sider fordelt på mere end 500 artikler af omkring 100 matematikere. Omfanget har givet det tilnavnet det enorme teorem.

Hvad Axiom har offentliggjort

CFSG fastslår, at enhver endelig simpel gruppe enten er cyklisk af primtalsorden, alternerende på mindst fem symboler, tilhører en af seksten uendelige familier af grupper af Lie-typen konstrueret over endelige legemer eller er en af præcis 26 isolerede sporadiske grupper. Meddelelsen bemærker, at nogle forfattere regner Tits-gruppen som en 27. gruppe. Den største sporadiske gruppe, Monster-gruppen, blev konstrueret af Robert Griess i 1980 ved hjælp af en algebra med dimensionen 196.884.

Det menneskelige arbejde med beviset strakte sig over årtier. I 1963 beviste Walter Feit og John Thompson, at enhver ikke-abelsk endelig simpel gruppe har lige orden, i en artikel på 255 sider, der fyldte et helt nummer af Pacific Journal of Mathematics. Daniel Gorenstein fremlagde i 1972 et program i seksten trin til at færdiggøre klassifikationen og erklærede den for fuldendt i 1983, men det kvasitynde tilfælde byggede på et ufærdigt manuskript af Geoffrey Mason, indtil Michael Aschbacher og Stephen Smith udgav en behandling på 1.221 sider i 2004 og dermed afsluttede det, der blev kendt som førstegenerationsbeviset. Et mere systematisk andengenerationsbevis, som Gorenstein og Richard Lyons påbegyndte, og som senere fik følgeskab af Ronald Solomon og Inna Capdeboscq, er stadig ufærdigt, så Axiom formaliserede førstegenerationsbeviset.

Projektets side beskriver formaliseringen som en gengivelse af førstegenerationsbeviset, hvor hvert logisk trin kontrolleres af Leans kerne, og angiver, at den omfatter 43,1 millioner linjer Lean-kode, 2,05 millioner erklæringer samt 715 artikler og bøger i sit korpus. Axiom siger, at virksomhedens bevisoversigt byggede på andengenerationsbindene, og at formaliseringen indeholder cirka 1,2 millioner kodelinjer fra det tidligere Qiuzhen-CFSG-projekt og bygger videre på Mathlib, som virksomheden tilskriver hundredvis af bidragydere. Projektet nævner Dean Cureton, Vasily Ilin, Bhavik Mehta og Niels Voss som centrale bidragydere og Letong Hong som hovedansvarlig forsker.

Det offentlige GitHub-arkiv beskriver resultatet som et Lean4-bevis uden sorry, fastlåst til version 4.35.0-rc3, bygget på Mathlib og TauCeti-projektet og baseret udelukkende på standardaksiomerne Classical.choice, propext og Quot.sound uden native_decide. Den formelle formulering af klassifikationen, som er hentet fra TauCeti, lyder: »Enhver endelig simpel gruppe er isomorf med en af de eksplicit konstruerede grupper på klassifikationslisten.« I README-filen står der, at lake build kontrollerer hele udviklingsarbejdet, og at åbne ændringer af Lake-byggesystemet samt optimeringer, som holdet planlægger at bidrage med til det oprindelige projekt, bragte byggetiden ned under 24 timer. Koden er udgivet under Apache-2.0-licensen.

En sværmindsats på 24 dage

Den 1. oktober 2026 oprettede Axiom en Slack-kanal for at koordinere projektet. Eksisterende Lean-arbejde og en intern bevisoversigt udarbejdet på grundlag af den publicerede litteratur delte indsatsen op i 108 milepæle og omkring 380 mindre opgaver. Den første sværm blev sat i gang den 2. oktober 2026, hvor agenter tog milepæle via GitHub-issues og rapporterede afsluttet arbejde i Slack. Ledende agenter opdelte vanskelige argumenter og gennemgik udsagn, mens andre agenter søgte efter eksisterende resultater eller skrev Lean-beviser. En agent kunne uddelegere manglende forudsætninger til andre agenter, hvis resultater blev lagt ind i et fælles arkiv.

De tidlige fremskridt afslørede svage punkter. Nogle tilsyneladende overkommelige milepæle skjulte enorme forudsætninger, som agenterne havde antaget i stedet for at bevise, og holdet slettede titusindvis af kodelinjer, der byggede på disse antagelser, før det genoptog arbejdet med en mere solid plan. En tidlig milepæl handlede om sætningen om signalizer-funktoren, hvis mulige bevis byggede på strukturelle antagelser, der stadig skulle begrundes. Byggetiderne blev også en flaskehals, fordi agenterne producerede beviser hurtigere, end Lean kunne kontrollere dem igen. Axiom siger, at virksomhedens ingeniører fordelte cachede byggeresultater mellem arbejdere, kørte uafhængige kontroller parallelt og flyttede beregningstunge endelige beregninger ud i certifikater, der kunne kontrolleres separat. Ifølge virksomheden øgede disse ændringer kontrolhastigheden med flere størrelsesordener.

Den 10. oktober 2026 meddelte en besked i kanalen, at agenterne havde bevist, at Monster-gruppen er simpel, fortæller virksomheden. Agenterne formaliserede også Monster-gruppens eksistens via Griess-algebraen samt en sætning, der identificerer grupper af Monster-typen med Monster-gruppen. Den 13. oktober 2026 blev kun én milepæl afsluttet, og ingeniørerne organiserede en ny planlægning, hvor ufærdige milepæle blev opdelt i mindre, præcist formulerede sætninger. For hver opdeling skulle det vises, hvordan delene kunne fastslå den oprindelige milepæl ved hjælp af et kort Lean-bevis.

Huller fundet i det publicerede bevis

Oversættelsen af beviset til Lean afslørede problemer i de offentliggjorte argumenter, oplyser Axiom. De fleste var mindre — typografiske fejl, fejl i tabeller eller udeladte hypoteser — men virksomheden tæller 34 bemærkelsesværdige afvigelser fra det offentliggjorte materiale. Den mest omfattende vedrører Unbalanced Group Theorem, eller UGT.

Et eksempel fandtes i Aschbacher og Smiths værker om kvasitynde grupper, hvor et lemma hævdede, at to numeriske størrelser var ens. Agenterne fandt et modeksempel med gruppen SL₂(5), hvor den ene størrelse var 1, selv om den hævdede lighed krævede 2. Ved at erstatte ligheden med en ulighed blev lemmaet rettet, men senere argumenter havde brugt ligheden til at udelukke tilfælde. Derfor udvidede teamet et tidligere argument, så det også dækkede disse konfigurationer.

UGT gør det muligt at identificere en hel gruppe ud fra oplysninger om dens undergrupper: Ifølge resuméet i den tilhørende artikel medfører en ikke-triviel undergruppe af ulige orden, der er normal i centralisatoren for en involution, under klassifikationens induktive hypoteser, at den omgivende simple gruppe er af Lie-type i ulige karakteristik eller alternerende af visse grader. Axiom tog fat på UGT med udgangspunkt i John Walters memoir fra 1986, og under formaliseringen af dette argument fandt virksomhedens agenter konkrete modeksempler på en lukningsegenskab, som argumentet byggede på: En operation, der antoges at holde de tilhørende simple grupper inden for en bestemt familie, kunne frembringe en gruppe, der udtrykkeligt var udelukket fra familien.

Ifølge virksomhedens redegørelse tager man udgangspunkt i PSL₂(49), hvis kropsinvolution har centralisatoren PGL₂(7). Operationen frembringer den simple komponent PSL₂(7), som er udelukket fra familien, fordi 7 er et Mersenneprimtal. Axiom bemærker, at modeksemplerne ikke modbeviste selve UGT eller engang konklusionen i Walters Proposition II.5.9(ii).

Løsningen byggede på Solomons teori fra 1976 om maksimale 2-komponenter, som ifølge Axiom leverede de centrale idéer til et alternativt argument, som virksomhedens AxiomProver-system udarbejdede og formaliserede. Det afgørende trin, der i artiklen betegnes Theorem 2.3 (bevarelse af simple topgrupper), beskrives af Axiom som et nyt resultat i gruppeteori, bevist af AxiomProver. Sammen med Gilman og Solomons reduktioner samt Foote og Harris’ genkendelsessætninger giver det den UGT-form for simple grupper, der er nødvendig for klassifikationen. Efter formaliseringen fandt Axioms matematikere en kortere deduktion inden for førstegenerationsmetoderne, anført som Remark 9.5, der når frem til samme konklusion uden Theorem 2.3.

Artiklen The Unbalanced Group Theorem, indsendt af Colin Defant og Ken Ono, blev offentliggjort på Hexagons preprintserver som version 1 den 27. oktober 2026 under en CC BY 4.0-licens; projektsiden angiver, at den er på 35 sider. Axiom oplyser, at virksomheden samarbejder med gruppeteoretikere om at samle de rettelser, der er fundet i litteraturen, og vil offentliggøre dem på projektets rettelsesside. Lyons og Solomon, hvis arbejde danner grundlag for klassifikationen, blev konsulteret om rettelsen af UGT. Virksomheden siger, at den fortsat vil gennemgå og afhjælpe rettelserne sammen med et rådgivende udvalg, der omfatter dem, samt den eksterne rådgiver Dan Nakano. Axiom beskriver sit bidrag som at gøre beviset mekanisk efterprøveligt, dokumentere de hindringer, der blev mødt, og levere formaliserede argumenter, der løser dem, samtidig med at virksomheden understreger, at klassifikationen fortsat er en bedrift, der tilhører de matematikere, som opdagede grupperne og udviklede argumenterne.