Axiom Math släpper Lean-bevis med 43,1 miljoner rader för klassificeringen av grupper

Axiom Math meddelade den 27 oktober 2026 att företaget släpper vad det beskriver som det första fullständiga datorverifierade beviset för klassificeringen av ändliga enkla grupper. Beviset togs fram på 24 dagar av ingenjörer och matematiker som ledde svärmar av dussintals AI-agenter, vilka skrev omkring 43,1 miljoner rader kod i bevisassistenten Lean.

”I dag släpper vi det första fullständiga datorverifierade beviset för klassificeringen av ändliga enkla grupper (CFSG)”, skrev företaget i sitt tillkännagivande. Klassificeringen identifierar ändliga gruppers grundläggande byggstenar. Det ursprungliga beviset omfattar omkring 15 000 sidor i mer än 500 artiklar av cirka 100 matematiker – en omfattning som har gett det smeknamnet den enorma satsen.

Vad Axiom har släppt

CFSG visar att varje ändlig enkel grupp är cyklisk av primtalsordning, alternerande på minst fem symboler, tillhör en av sexton oändliga familjer av grupper av Lie-typ konstruerade över ändliga kroppar eller är en av exakt 26 isolerade sporadiska grupper. I tillkännagivandet påpekas att vissa författare räknar Titsgruppen som en 27:e grupp. Den största sporadiska gruppen, monstret, konstruerades av Robert Griess 1980 med hjälp av en algebra av dimensionen 196 884.

Det mänskliga arbetet med beviset sträckte sig över flera årtionden. År 1963 bevisade Walter Feit och John Thompson att varje icke-abelsk ändlig enkel grupp har jämn ordning. Beviset publicerades i en artikel på 255 sidor som fyllde ett helt nummer av Pacific Journal of Mathematics. Daniel Gorenstein lade 1972 fram ett program med sexton steg för att slutföra klassificeringen och förklarade den fullständig 1983, men det kvasitunna fallet vilade på ett ofullbordat manuskript av Geoffrey Mason tills Michael Aschbacher och Stephen Smith publicerade en behandling på 1 221 sidor 2004. Därmed avslutades det som kom att kallas den första generationens bevis. Ett mer systematiskt bevis av den andra generationen, som inleddes av Gorenstein och Richard Lyons och senare även omfattade Ronald Solomon och Inna Capdeboscq, är fortfarande ofullständigt. Därför formaliserade Axiom beviset av den första generationen.

Projektsidan beskriver formaliseringen som en uppföljning av beviset av den första generationen, där varje logiskt steg kontrolleras av Leans kärna. Där anges också att kodbasen omfattar 43,1 miljoner rader Lean-kod, 2,05 miljoner deklarationer och 715 artiklar och böcker. Axiom uppger att företagets beviskarta bygger på volymerna från den andra generationen och att formaliseringen innehåller omkring 1,2 miljoner kodrader från det tidigare projektet Qiuzhen-CFSG. Den bygger också på Mathlib, som enligt Axiom är ett verk av hundratals bidragsgivare. Projektet anger Dean Cureton, Vasily Ilin, Bhavik Mehta och Niels Voss som kärnbidragsgivare, med Letong Hong som huvudansvarig forskare.

Det offentliga GitHub-arkivet beskriver resultatet som ett Lean4-bevis utan `sorry`, låst till version 4.35.0-rc3, byggt på Mathlib och TauCeti-projektet och med endast standardaxiomen Classical.choice, propext och Quot.sound; native_decide används inte. Den formella utsagan om klassificeringen, hämtad från TauCeti, lyder: ”Varje ändlig enkel grupp är isomorf med en av de uttryckligen konstruerade grupperna på klassificeringslistan.” I README-filen står det att lake build kontrollerar hela utvecklingsarbetet och att öppna ändringar i byggverktyget Lake, tillsammans med optimeringar som teamet planerar att bidra med uppströms, har pressat byggtiden till under 24 timmar. Koden har licensen Apache-2.0.

En svärm arbetade i 24 dagar

Den 1 oktober 2026 öppnade Axiom en Slack-kanal för att samordna projektet. Befintligt Lean-arbete och en intern beviskarta som sammanställts utifrån den publicerade litteraturen delade upp arbetet i 108 milstolpar och omkring 380 mindre uppgifter. Den första agentgruppen sattes i arbete den 2 oktober 2026. Agenterna tog på sig milstolpar via GitHub-ärenden och rapporterade slutfört arbete i Slack. Ledande agenter bröt ned svåra resonemang och granskade utsagor, medan andra agenter sökte efter befintliga resultat eller skrev Lean-bevis. En agent kunde också delegera saknade förutsättningar till andra agenter, vars resultat fördes in i ett gemensamt arkiv.

De första framstegen blottlade svaga punkter. Vissa milstolpar som verkade hanterbara dolde enorma förutsättningar som agenterna hade antagit i stället för att bevisa. Teamet raderade tiotusentals kodrader som byggde på dessa antaganden och började om med en mer hållbar plan. En tidig milstolpe gällde satsen om signaliseringsfunktorer, där ett preliminärt bevis byggde på strukturella antaganden som fortfarande behövde motiveras. Byggtiderna blev också en flaskhals när agenterna producerade bevis snabbare än Lean kunde kontrollera dem på nytt. Axiom uppger att företagets ingenjörer distribuerade cachade byggresultat mellan arbetsnoder, körde oberoende kontroller parallellt och lät dyra ändliga beräkningar utföras separat med certifikat som kunde kontrolleras var för sig. Enligt företaget gjorde dessa förändringar verifieringen många gånger snabbare.

Den 10 oktober 2026 meddelade ett meddelande i kanalen att agenterna hade bevisat att monstret är enkelt, berättar företaget. Agenterna formaliserade också monstrets existens med hjälp av Griessalgebran samt en sats som identifierar grupper av monstertyp med monstret. Den 13 oktober 2026 avslutades bara en milstolpe. Ingenjörerna organiserade då ett omplaneringsarbete där ofärdiga milstolpar delades upp i mindre, exakt formulerade satser. För varje sådan uppdelning krävdes ett kort Lean-bevis som visade hur delarna tillsammans kunde uppfylla den ursprungliga milstolpen.

Luckor upptäckta i det publicerade beviset

Översättningen av beviset till Lean blottlade problem i de publicerade argumenten, rapporterar Axiom. De flesta var mindre — tryckfel, fel i tabeller eller utelämnade hypoteser — men företaget räknar 34 anmärkningsvärda avvikelser från den publicerade framställningen. Den mest betydande gäller Unbalanced Group Theorem, eller UGT.

Ett exempel återfanns i Aschbacher och Smiths volymer om kvasi-tunna grupper, där ett lemma hävdade att två numeriska storheter var lika. Agenterna fann ett motexempel som involverade gruppen SL₂(5), där den ena storheten var 1 medan den hävdade likheten krävde 2. Att ersätta likheten med en olikhet rättade till lemmat, men senare argument hade använt likheten för att utesluta fall, så teamet utvidgade ett tidigare argument så att det även omfattade dessa konfigurationer.

UGT gör det möjligt att identifiera en hel grupp utifrån information om dess delgrupper: enligt sammanfattningen till den tillhörande artikeln innebär klassifikationens induktiva hypoteser att en icke-trivial delgrupp av udda ordning, som är normal i centralisatorn till en involution, tvingar den omgivande enkla gruppen att vara av Lie-typ i udda karakteristik eller alternerande av vissa grader. Axiom tog sig an UGT med utgångspunkt i John Walters monografi från 1986, och medan agenterna formaliserade det argumentet fann de explicita motexempel till ett slutningspåstående som det använde: en operation som antogs hålla de tillhörande enkla grupperna inom en viss familj kunde ge upphov till en grupp som uttryckligen var utesluten ur den.

Enligt företagets redogörelse utgår man från PSL₂(49), vars fältinvolution har centralisatorn PGL₂(7), och operationen ger då den enkla komponenten PSL₂(7), som är utesluten ur familjen eftersom 7 är ett Mersenneprimtal. Axiom påpekar att motexemplen inte kullkastade UGT i sig, eller ens slutsatsen i Walter sats II.5.9(ii).

Reparationen byggde på Solomons teori från 1976 om maximala 2-komponenter, som enligt Axiom tillhandahöll huvudidéerna till ett alternativt argument som företagets system AxiomProver tog fram och formaliserade. Det centrala steget, som i artikeln anges som sats 2.3 (bevarande av enkla toppar), beskrivs av Axiom som ett nytt resultat inom gruppteorin, bevisat av AxiomProver. Tillsammans med reduktionerna av Gilman och Solomon och igenkänningssatserna av Foote och Harris ger det den form av UGT för enkla grupper som klassifikationen kräver. Efter formaliseringen fann Axioms matematiker en kortare härledning med första generationens metoder, dokumenterad som anmärkning 9.5, som når samma slutsats utan sats 2.3.

Artikeln, The Unbalanced Group Theorem, som Colin Defant och Ken Ono har bidragit till, publicerades på Hexagons preprintserver som version 1 den 27 oktober 2026 under licensen CC BY 4.0. På projektsidan anges att den omfattar 35 sidor. Axiom uppger att företaget samarbetar med gruppteoretiker för att sammanställa de rättelser som påträffats i litteraturen och publicera dem på projektets rättelsesida. Lyons och Solomon, vars arbete ligger till grund för klassifikationen, rådfrågades om reparationen av UGT. Företaget säger att det kommer att fortsätta sammanställa och åtgärda rättelserna tillsammans med en rådgivande nämnd där de ingår, liksom den externa rådgivaren Dan Nakano. Axiom beskriver sitt bidrag som att göra beviset mekaniskt kontrollerbart, dokumentera de hinder som påträffats och tillhandahålla formaliserade argument som löser dem, samtidigt som företaget framhåller att klassifikationen är en bedrift av de matematiker som upptäckte grupperna och utvecklade argumenten.