Axiom Math veröffentlicht einen Lean-Beweis der Gruppenklassifikation mit 43,1 Millionen Zeilen

Axiom Math teilte am 27. Oktober 2026 mit, dass das Unternehmen nach eigenen Angaben den ersten vollständigen, computergestützt geprüften Beweis der Klassifikation der endlichen einfachen Gruppen veröffentlicht. Ingenieure und Mathematiker erarbeiteten ihn innerhalb von 24 Tagen, indem sie Schwärme aus Dutzenden KI-Agenten koordinierten, die im Lean-Beweisassistenten rund 43,1 Millionen Codezeilen schrieben.

„Heute veröffentlichen wir den ersten vollständigen, computergestützt geprüften Beweis der Klassifikation der endlichen einfachen Gruppen (CFSG)“, schrieb das Unternehmen in seiner Ankündigung. Die Klassifikation bestimmt die grundlegenden Bausteine endlicher Gruppen. Ihr ursprünglicher Beweis umfasst rund 15.000 Seiten in mehr als 500 Artikeln von etwa 100 Mathematikern – ein Umfang, der ihm den Spitznamen „Satzungeheuer“ einbrachte.

Was Axiom veröffentlicht hat

Die CFSG besagt, dass jede endliche einfache Gruppe entweder zyklisch von Primzahlordnung, eine alternierende Gruppe auf mindestens fünf Symbolen, eine von sechzehn unendlichen Familien von Gruppen vom Lie-Typ über endlichen Körpern oder eine von genau 26 isolierten sporadischen Gruppen ist. In der Ankündigung wird darauf hingewiesen, dass manche Autoren die Tits-Gruppe als 27. Gruppe mitzählen. Die größte sporadische Gruppe, die Monstergruppe, wurde 1980 von Robert Griess mithilfe einer Algebra der Dimension 196.884 konstruiert.

Die Arbeit am Beweis durch Menschen erstreckte sich über Jahrzehnte. 1963 bewiesen Walter Feit und John Thompson in einem 255-seitigen Aufsatz, der eine ganze Ausgabe des Pacific Journal of Mathematics füllte, dass jede nichtabelsche endliche einfache Gruppe eine gerade Ordnung hat. Daniel Gorenstein legte 1972 ein Programm mit sechzehn Schritten zur Vervollständigung der Klassifikation vor und erklärte sie 1983 für abgeschlossen. Der Quasithin-Fall beruhte jedoch auf einem unvollendeten Manuskript von Geoffrey Mason, bis Michael Aschbacher und Stephen Smith 2004 eine 1.221-seitige Behandlung veröffentlichten und damit den als Beweis der ersten Generation bekannt gewordenen Beweis abschlossen. Ein systematischerer Beweis der zweiten Generation, den Gorenstein und Richard Lyons begonnen hatten und dem sich später Ronald Solomon und Inna Capdeboscq anschlossen, ist weiterhin unvollständig. Daher formalisierte Axiom den Beweis der ersten Generation.

Die Projektseite stellt die Formalisierung als Umsetzung des Beweises der ersten Generation dar, bei der jeder logische Schritt vom Lean-Kernel überprüft wird. Sie führt 43,1 Millionen Lean-Zeilen, 2,05 Millionen Deklarationen sowie 715 Artikel und Bücher im Korpus auf. Axiom zufolge stützte sich die Beweiskarte auf die Bände des Beweises der zweiten Generation. Außerdem enthält die Formalisierung rund 1,2 Millionen Codezeilen aus dem früheren Projekt Qiuzhen-CFSG und baut auf Mathlib auf, zu dessen Entwicklung laut Axiom Hunderte von Mitwirkenden beigetragen haben. Als zentrale Mitwirkende des Projekts werden Dean Cureton, Vasily Ilin, Bhavik Mehta und Niels Voss genannt; die wissenschaftliche Leitung hat Letong Hong.

Das öffentliche GitHub-Repository beschreibt das Ergebnis als sorry-freien Lean4-Beweis, der auf Version 4.35.0-rc3 festgelegt ist, auf Mathlib und dem Projekt TauCeti aufbaut und ausschließlich die Standardaxiome Classical.choice, propext und Quot.sound verwendet – native_decide kommt nicht zum Einsatz. Die aus TauCeti übernommene formale Aussage der Klassifikation lautet: „Jede endliche einfache Gruppe ist zu einer der explizit konstruierten Gruppen auf der Klassifikationsliste isomorph.“ Laut README prüft lake build die gesamte Entwicklung. Offene Änderungen am Lake-Build-Tool und Optimierungen, die das Team upstream einzubringen plant, senkten die Build-Zeit auf weniger als 24 Stunden. Der Code steht unter der Apache-2.0-Lizenz.

Ein 24-tägiger Einsatz eines Agentenschwarms

Am 1. Oktober 2026 richtete Axiom einen Slack-Kanal ein, um das Projekt zu koordinieren. Bereits vorhandene Lean-Arbeiten und eine interne, anhand der veröffentlichten Fachliteratur erstellte Beweiskarte teilten die Arbeit in 108 Meilensteine und rund 380 kleinere Aufgaben auf. Der erste Agentenschwarm ging am 2. Oktober 2026 an den Start. Die Agenten beanspruchten Meilensteine über GitHub-Issues und meldeten abgeschlossene Arbeiten in Slack. Führende Agenten zerlegten schwierige Argumentationen und überprüften Aussagen, während andere Agenten nach vorhandenen Ergebnissen suchten oder Lean-Beweise schrieben. Fehlende Voraussetzungen konnte ein Agent an andere Agenten delegieren; deren Ergebnisse flossen in ein gemeinsames Repository ein.

Schon die ersten Fortschritte legten Schwachstellen offen. Hinter einigen zunächst überschaubar wirkenden Meilensteinen verbargen sich umfangreiche Voraussetzungen, die die Agenten voraussetzten, statt sie zu beweisen. Das Team löschte Zehntausende auf diesen Annahmen beruhende Zeilen und begann mit einem tragfähigeren Plan von vorn. Bei einem frühen Meilenstein ging es um den Signalizer-Funktor-Satz; der vorgeschlagene Beweis beruhte auf strukturellen Annahmen, die noch begründet werden mussten. Auch die Build-Zeiten wurden zum Engpass, als die Agenten schneller Beweise erstellten, als Lean sie erneut überprüfen konnte. Axiom zufolge verteilten die Ingenieure des Unternehmens zwischengespeicherte Build-Ergebnisse auf mehrere Rechner, führten unabhängige Prüfungen parallel aus und lagerten aufwendige endliche Berechnungen in separat überprüfbare Zertifikate aus. Diese Änderungen hätten die Überprüfung nach Angaben des Unternehmens um Größenordnungen beschleunigt.

Am 10. Oktober 2026 verkündete eine Nachricht im Kanal, dass die Agenten bewiesen hätten, dass die Monstergruppe einfach ist, berichtet das Unternehmen. Die Agenten formalisierten außerdem die Existenz der Monstergruppe mithilfe der Griess-Algebra sowie einen Satz, der Gruppen vom Monstertyp mit der Monstergruppe identifiziert. Am 13. Oktober 2026 wurde nur ein Meilenstein abgeschlossen. Daraufhin organisierten die Ingenieure eine Neuplanung und teilten die noch offenen Meilensteine in kleinere, präzise formulierte Sätze auf. Für jede solche Zerlegung musste anhand eines kurzen Lean-Beweises gezeigt werden, wie sich aus den einzelnen Teilen der ursprüngliche Meilenstein ableiten ließ.

Lücken im veröffentlichten Beweis entdeckt

Die Übertragung des Beweises nach Lean legte Probleme in den veröffentlichten Argumentationen offen, berichtet Axiom. Die meisten waren geringfügig – Druckfehler, Fehler in Tabellen oder ausgelassene Voraussetzungen –, doch das Unternehmen zählt 34 nennenswerte Abweichungen von der veröffentlichten Fassung. Die schwerwiegendste betrifft den Unbalanced Group Theorem (UGT).

Ein Beispiel fand sich in Aschbacher und Smiths Bänden zu quasidünnen Gruppen: Dort behauptete ein Lemma, zwei numerische Größen seien gleich. Die Agenten fanden ein Gegenbeispiel mit der Gruppe SL₂(5), bei der eine Größe 1 statt der von der behaupteten Gleichheit geforderten 2 betrug. Die Ersetzung der Gleichheit durch eine Ungleichung korrigierte das Lemma. Spätere Argumentationen hatten jedoch die Gleichheit verwendet, um Fälle auszuschließen. Daher erweiterte das Team eine frühere Argumentation, um diese Konfigurationen abzudecken.

Der UGT hilft dabei, aus Informationen über die Untergruppen auf eine ganze Gruppe zu schließen: Laut der Zusammenfassung von dem zugehörigen Artikel muss unter den induktiven Hypothesen der Klassifikation eine nichttriviale Untergruppe ungerader Ordnung, die im Zentralisator einer Involution normal ist, dazu führen, dass die umgebende einfache Gruppe vom Lie-Typ in ungerader Charakteristik oder eine alternierende Gruppe von bestimmtem Grad ist. Axiom ging den UGT anhand von John Walters Monografie aus dem Jahr 1986 an. Bei der Formalisierung dieser Argumentation fanden die Agenten explizite Gegenbeispiele zu einer darin verwendeten Abschlusseigenschaft: Eine Operation, von der angenommen wurde, dass sie die zugehörigen einfachen Gruppen innerhalb einer bestimmten Familie hält, konnte eine Gruppe hervorbringen, die ausdrücklich aus dieser Familie ausgeschlossen war.

Laut der Darstellung des Unternehmens geht die Operation von PSL₂(49) aus, dessen Körperinvolution den Zentralisator PGL₂(7) hat, und ergibt die einfache Komponente PSL₂(7). Diese ist aus der Familie ausgeschlossen, da 7 eine Mersenne-Primzahl ist. Axiom weist darauf hin, dass die Gegenbeispiele weder den UGT selbst noch auch nur die Schlussfolgerung von Walters Proposition II.5.9(ii) widerlegten.

Die Korrektur stützte sich auf Solomons Theorie der maximalen 2-Komponenten aus dem Jahr 1976. Wie Axiom erklärt, lieferte sie die zentralen Ideen für eine alternative Argumentation, die das System AxiomProver entwickelte und formalisierte. Der entscheidende Schritt, im Artikel als Theorem 2.3 (Erhaltung einfacher Tops) formuliert, wird von Axiom als ein neues, mit AxiomProver bewiesenes Ergebnis der Gruppentheorie beschrieben. Zusammen mit den Reduktionen von Gilman und Solomon sowie den Erkennungssätzen von Foote und Harris liefert dieser Schritt die für die Klassifikation benötigte Form des UGT für einfache Gruppen. Nach der Formalisierung fanden Mathematiker von Axiom eine kürzere Herleitung mit Methoden der ersten Generation, die als Bemerkung 9.5 festgehalten ist und ohne Theorem 2.3 zum selben Schluss gelangt.

Der von Colin Defant und Ken Ono beigesteuerte Artikel The Unbalanced Group Theorem erschien am 27. Oktober 2026 als Version 1 auf dem Preprint-Server Hexagon unter einer CC-BY-4.0-Lizenz; auf der Projektseite wird er mit einem Umfang von 35 Seiten aufgeführt. Axiom erklärt, mit Gruppentheoretikern zusammenzuarbeiten, um die in der Literatur gefundenen Errata zusammenzustellen und sie auf der Errata-Seite des Projekts zu veröffentlichen. Lyons und Solomon, auf deren Arbeit die Klassifikation beruht, wurden zur Korrektur des UGT konsultiert. Das Unternehmen erklärt, die Errata auch künftig gemeinsam mit einem Beirat zu kuratieren und zu beheben, dem die beiden angehören, ebenso wie der externe Berater Dan Nakano. Axiom beschreibt seinen Beitrag als die mechanische Überprüfbarkeit des Beweises, die Dokumentation der dabei aufgetretenen Hindernisse und die Bereitstellung formalisierter Argumentationen, die diese ausräumen. Zugleich betont das Unternehmen, dass die Klassifikation das Verdienst der Mathematiker bleibt, die die Gruppen entdeckt und die Argumentationen entwickelt haben.