Axiom Math brengt Lean-bewijs van 43,1 miljoen regels voor de classificatie van groepen uit

Axiom Math maakte op 27 oktober 2026 bekend dat het naar eigen zeggen het eerste volledige, door een computer gecontroleerde bewijs van de classificatie van de eindige enkelvoudige groepen uitbrengt. Ingenieurs en wiskundigen stuurden daarvoor gedurende 24 dagen zwermen van tientallen AI-agenten aan, die in de Lean-bewijsassistent ongeveer 43,1 miljoen regels code schreven.

‘Vandaag brengen we het eerste volledige, door een computer gecontroleerde bewijs van de classificatie van de eindige enkelvoudige groepen (CFSG) uit’, schreef het bedrijf in de aankondiging. De classificatie identificeert de elementaire bouwstenen van eindige groepen. Het oorspronkelijke bewijs beslaat ongeveer 15.000 pagina’s, verdeeld over meer dan 500 artikelen van zo’n 100 wiskundigen. Door die omvang kreeg het de bijnaam ‘de enorme stelling’.

Wat Axiom heeft uitgebracht

De CFSG stelt vast dat elke eindige enkelvoudige groep cyclisch van priemorde is, een alternerende groep op ten minste vijf letters, behoort tot een van de zestien oneindige families van groepen van Lie-type die over eindige lichamen zijn geconstrueerd, of een van precies 26 geïsoleerde sporadische groepen is. In de aankondiging staat dat sommige auteurs de Tits-groep als 27e groep meetellen. De grootste sporadische groep, de Monster-groep, werd in 1980 door Robert Griess geconstrueerd met behulp van een algebra van dimensie 196.884.

Het menselijke bewijsproject strekte zich uit over tientallen jaren. In 1963 bewezen Walter Feit en John Thompson dat elke niet-abelse eindige enkelvoudige groep een even orde heeft. Hun artikel van 255 pagina’s vulde een volledig nummer van het Pacific Journal of Mathematics. Daniel Gorenstein zette in 1972 een programma in zestien stappen op om de classificatie te voltooien en verklaarde die in 1983 afgerond. Het quasithin-geval berustte echter op een onvoltooid manuscript van Geoffrey Mason, totdat Michael Aschbacher en Stephen Smith in 2004 een behandeling van 1.221 pagina’s publiceerden. Daarmee werd het werk afgesloten dat bekend kwam te staan als het bewijs van de eerste generatie. Een systematischer bewijs van de tweede generatie, begonnen door Gorenstein en Richard Lyons en later voortgezet met Ronald Solomon en Inna Capdeboscq, is nog niet voltooid. Daarom formaliseerde Axiom het bewijs van de eerste generatie.

Op de projectpagina wordt de formalisering gepresenteerd als een uitwerking van het bewijs van de eerste generatie, waarbij elke logische stap door de kernel van Lean wordt gecontroleerd. De pagina vermeldt 43,1 miljoen regels Lean-code, 2,05 miljoen declaraties en 715 artikelen en boeken in het corpus. Axiom zegt dat de bewijskaart is gebaseerd op de delen van het bewijs van de tweede generatie en dat de formalisering ongeveer 1,2 miljoen regels code uit het eerdere Qiuzhen-CFSG-project bevat. Ook bouwt de formalisering voort op Mathlib, waaraan volgens Axiom honderden bijdragers hebben gewerkt. Het project noemt Dean Cureton, Vasily Ilin, Bhavik Mehta en Niels Voss als kernbijdragers, met Letong Hong als hoofdonderzoeker.

De openbare GitHub-repository omschrijft het resultaat als een Lean4-bewijs zonder ‘sorry’, vastgezet op versie 4.35.0-rc3, gebouwd op Mathlib en het TauCeti-project. Het gebruikt uitsluitend de standaardaxioma’s Classical.choice, propext en Quot.sound, en geen native_decide. De formele formulering van de classificatie, overgenomen uit TauCeti, luidt: ‘Elke eindige enkelvoudige groep is isomorf met een van de expliciet geconstrueerde groepen op de classificatielijst.’ Volgens de README controleert lake build de volledige ontwikkeling. Open wijzigingen aan de Lake-buildtool en optimalisaties die het team van plan is upstream bij te dragen, brachten de bouwtijd terug tot minder dan 24 uur. De code valt onder de Apache-2.0-licentie.

Een zwermproject van 24 dagen

Op 1 oktober 2026 opende Axiom een Slack-kanaal om het project te coördineren. Bestaand Lean-werk en een interne bewijskaart, samengesteld op basis van de gepubliceerde literatuur, verdeelden het werk in 108 mijlpalen en ongeveer 380 kleinere taken. De eerste zwerm ging op 2 oktober 2026 van start: agenten namen mijlpalen op zich via GitHub-issues en meldden afgerond werk in Slack. Hoofdagenten deelden moeilijke redeneringen op in onderdelen en controleerden beweringen, terwijl andere agenten naar bestaande resultaten zochten of Lean-bewijzen schreven. Een agent kon ontbrekende vereiste resultaten bovendien aan andere agenten delegeren; hun resultaten werden vervolgens opgenomen in een gedeelde repository.

In een vroeg stadium kwamen zwakke plekken aan het licht. Achter sommige mijlpalen die haalbaar leken, gingen enorme vereiste tussenresultaten schuil die agenten hadden aangenomen in plaats van bewezen. Het team verwijderde tienduizenden regels code die op die aannames waren gebaseerd en begon opnieuw met een degelijker plan. Een vroege mijlpaal betrof de stelling over de signalizer-functor. Het kandidaatbewijs daarvoor steunde op structurele aannames die nog onderbouwd moesten worden. Ook de bouwtijd werd een knelpunt: agenten produceerden bewijzen sneller dan Lean ze opnieuw kon controleren. Axiom zegt dat de ingenieurs gecachete bouwresultaten over meerdere werkers verdeelden, onafhankelijke controles parallel uitvoerden en tijdrovende eindige berekeningen onderbrachten in certificaten die afzonderlijk konden worden gecontroleerd. Volgens het bedrijf versnelden die aanpassingen de verificatie met meerdere ordes van grootte.

Op 10 oktober 2026 kondigde een bericht in het kanaal aan dat de agenten hadden bewezen dat de Monster-groep enkelvoudig is, vertelt het bedrijf. De agenten formaliseerden ook het bestaan van de Monster-groep via de Griess-algebra en een stelling die groepen van het Monster-type identificeert met de Monster-groep. Op 13 oktober 2026 werd slechts één mijlpaal afgerond. De ingenieurs zetten daarop een nieuwe planningsronde op, waarbij onvoltooide mijlpalen werden opgesplitst in kleinere, nauwkeurig geformuleerde stellingen. Bij elke opsplitsing moest met een kort Lean-bewijs worden aangetoond hoe de onderdelen samen de oorspronkelijke mijlpaal zouden bewijzen.

Hiaten gevonden in het gepubliceerde bewijs

Axiom meldt dat het vertalen van het bewijs naar Lean problemen in de gepubliceerde argumentatie aan het licht bracht. De meeste waren klein — typfouten, fouten in tabellen of weggelaten hypothesen — maar het bedrijf telt 34 noemenswaardige afwijkingen van de gepubliceerde versie. De belangrijkste heeft betrekking op de Unbalanced Group Theorem, of UGT.

Een voorbeeld kwam uit de quasidunne delen van Aschbacher en Smith, waarin een lemma stelde dat twee numerieke grootheden gelijk waren. De agents vonden een tegenvoorbeeld met de groep SL₂(5), waarin de ene grootheid 1 was, terwijl de gestelde gelijkheid 2 vereiste. Door de gelijkheid te vervangen door een ongelijkheid werd het lemma gecorrigeerd, maar latere argumenten gebruikten de gelijkheid om gevallen uit te sluiten. Daarom breidde het team een eerder argument uit, zodat het ook die configuraties omvatte.

De UGT helpt een volledige groep te identificeren aan de hand van informatie over haar deelgroepen: volgens het abstract van het begeleidende artikel dwingt onder de inductieve hypothesen van de classificatie een niet-triviale deelgroep van oneven orde die normaal is in de centralisator van een involutie, de omgevende enkelvoudige groep tot een groep van Lie-type in oneven karakteristiek of tot een alternerende groep van bepaalde graden. Axiom benaderde de UGT via de memoire van John Walter uit 1986. Tijdens de formalisering van dat argument vonden de agents expliciete tegenvoorbeelden voor een afsluitingseigenschap waarop het berustte: een bewerking die de bijbehorende enkelvoudige groepen binnen een bepaalde familie zou moeten houden, kon een groep opleveren die uitdrukkelijk van die familie was uitgesloten.

Volgens de beschrijving van het bedrijf vertrekt de bewerking van PSL₂(49), waarvan de veldinvolutie de centralisator PGL₂(7) heeft, en levert zij de enkelvoudige component PSL₂(7) op. Die is uitgesloten van de familie omdat 7 een Mersennepriemgetal is. Axiom merkt op dat de tegenvoorbeelden de UGT zelf niet weerlegden, en evenmin de conclusie van stelling II.5.9(ii) van Walter.

De correctie bouwde voort op Solomons theorie uit 1976 over maximale 2-componenten, die volgens Axiom de centrale ideeën leverde voor een alternatieve redenering die het AxiomProver-systeem voortbracht en formaliseerde. De belangrijkste stap, in het artikel geformuleerd als stelling 2.3 (behoud van eenvoudige toppen), wordt door Axiom beschreven als een nieuw resultaat in de groepentheorie, bewezen door AxiomProver. Samen met de reducties van Gilman en Solomon en de herkenningsstellingen van Foote en Harris levert deze stap de vorm van de UGT voor enkelvoudige groepen die nodig is voor de classificatie. Na de formalisering vonden de wiskundigen van Axiom een kortere afleiding met methoden van de eerste generatie. Deze is vastgelegd als opmerking 9.5 en bereikt dezelfde conclusie zonder stelling 2.3.

Dat artikel, The Unbalanced Group Theorem, waaraan Colin Defant en Ken Ono bijdroegen, verscheen op 27 oktober 2026 als versie 1 op de Hexagon-preprintserver onder een CC BY 4.0-licentie. Volgens de projectpagina telt het 35 pagina’s. Axiom zegt samen te werken met groepentheoretici om de errata uit de literatuur te verzamelen en die te publiceren op de erratapagina van het project. Lyons en Solomon, wier werk aan de basis ligt van de classificatie, werden geraadpleegd over de correctie van de UGT. Het bedrijf zegt de errata te blijven beheren en oplossen met een adviesraad waarin ook zij zitting hebben, naast extern adviseur Dan Nakano. Axiom omschrijft zijn bijdrage als het mechanisch controleerbaar maken van het bewijs, het documenteren van de aangetroffen obstakels en het aanleveren van geformaliseerde argumenten om die op te lossen. Daarbij stelt het bedrijf dat de classificatie de verdienste blijft van de wiskundigen die de groepen ontdekten en de argumenten ontwikkelden.