Axiom Math: Komplett maschinengeprüfter Beweis der Klassifikation endlicher einfacher Gruppen

Worum es geht

Axiom Math hat am 27. Oktober 2026 nach eigener Darstellung den ersten vollständigen, von einem Computer geprüften Beweis der Klassifikation endlicher einfacher Gruppen (CFSG) veröffentlicht. Entstanden ist er in 24 Tagen: Ingenieure und Mathematiker steuerten Schwärme aus Dutzenden KI-Agenten, die etwa 43,1 Millionen Zeilen Code im Beweisassistenten Lean schrieben. Ein Beweisassistent ist ein Programm, das mathematische Beweise Schritt für Schritt auf logische Korrektheit prüft. Alle Angaben stammen von Axiom selbst.

Die Klassifikation beschreibt die Grundbausteine endlicher Gruppen. Der ursprüngliche menschliche Beweis erstreckt sich über rund 15.000 Seiten in mehr als 500 Artikeln von etwa 100 Mathematikern, weshalb er auch „der riesige Satz“ (enormous theorem) genannt wird.

Was die Klassifikation besagt

Jede endliche einfache Gruppe, also eine Gruppe ohne echte Zerlegung in kleinere Bausteine, ist laut CFSG eines von vier Dingen: zyklisch mit Primzahlordnung, alternierend auf mindestens fünf Symbolen, Mitglied einer von sechzehn unendlichen Familien vom Lie-Typ über endlichen Körpern oder eine von genau 26 sporadischen Gruppen. Manche Autoren zählen die Tits-Gruppe als 27. dazu. Die größte sporadische Gruppe, das „Monster“, konstruierte Robert Griess 1980 mithilfe einer Algebra der Dimension 196.884.

Die menschliche Beweisgeschichte zog sich über Jahrzehnte: 1963 bewiesen Walter Feit und John Thompson auf 255 Seiten, dass jede nichtabelsche endliche einfache Gruppe gerade Ordnung hat. Daniel Gorenstein formulierte 1972 ein 16-Schritte-Programm und erklärte die Klassifikation 1983 für abgeschlossen. Der „quasithin“-Fall stützte sich aber auf ein unfertiges Manuskript von Geoffrey Mason, bis Michael Aschbacher und Stephen Smith 2004 eine 1.221-seitige Behandlung veröffentlichten. Das ist der „Beweis der ersten Generation“. Ein systematischerer Beweis der zweiten Generation (Gorenstein, Lyons, Solomon, Capdeboscq) ist unvollständig; Axiom formalisierte deshalb die erste Generation.

Was veröffentlicht wurde

Laut Projektseite wird der Beweis der ersten Generation gefolgt, jeder logische Schritt vom Lean-Kernel geprüft. Die Zahlen: 43,1 Millionen Zeilen Lean, 2,05 Millionen Deklarationen, 715 Papers und Bücher im Korpus. Die Proof Map nutzte auch die Bände der zweiten Generation. Rund 1,2 Millionen Zeilen stammen aus dem früheren Projekt Qiuzhen-CFSG; zudem baut es auf Mathlib auf, der Mathematik-Bibliothek für Lean. Kernbeitragende sind Dean Cureton, Vasily Ilin, Bhavik Mehta und Niels Voss, Principal Investigator ist Letong Hong.

Das öffentliche GitHub-Repository beschreibt das Ergebnis als „sorry-freien“ Lean-4-Beweis (kein Platzhalter für ungeprüfte Teile), festgelegt auf Version 4.35.0-rc3, basierend auf Mathlib und dem TauCeti-Projekt. Es verwendet nur die Standardaxiome Classical.choice, propext und Quot.sound und kein native_decide. Der formale Satz lautet übersetzt:

Jede endliche einfache Gruppe ist isomorph zu einer der explizit konstruierten Gruppen auf der Klassifikationsliste.

lake build prüft die gesamte Entwicklung. Durch Änderungen am Build-Werkzeug Lake und geplante Optimierungen soll der Build unter 24 Stunden dauern. Lizenz: Apache-2.0.

Der Ablauf der 24 Tage

Am 1. Oktober 2026 richtete Axiom einen Slack-Kanal ein. Vorhandene Lean-Arbeit und eine interne Proof Map aus der Fachliteratur teilten das Vorhaben in 108 Meilensteine und rund 380 kleinere Aufgaben. Am 2. Oktober startete der erste Schwarm. Agenten beanspruchten Meilensteine über GitHub-Issues und meldeten Fortschritt in Slack. Leitagenten zerlegten schwierige Argumente und prüften Aussagen, andere suchten vorhandene Resultate oder schrieben Lean-Beweise; fehlende Vorarbeiten konnten an weitere Agenten delegiert werden, deren Ergebnisse in ein gemeinsames Repository flossen.

Anfangs zeigten sich Schwachstellen: Manche scheinbar machbaren Meilensteine verbargen riesige Voraussetzungen, die Agenten nur angenommen statt bewiesen hatten. Das Team löschte zehntausende Zeilen und startete mit besserem Plan neu. Auch die Build-Zeit wurde zum Engpass, weil Agenten schneller Beweise lieferten, als Lean sie neu prüfen konnte. Axiom verteilte Build-Caches auf Worker, führte Prüfungen parallel aus und lagerte aufwendige endliche Rechnungen in separat prüfbare Zertifikate aus – nach Firmenangabe beschleunigte das die Verifikation um Größenordnungen.

Am 10. Oktober meldete ein Kanalbeitrag, die Agenten hätten bewiesen, dass das Monster einfach ist; auch seine Existenz über die Griess-Algebra und ein Identifikationssatz wurden formalisiert. Am 13. Oktober schloss sich nur ein Meilenstein, woraufhin man offene Meilensteine in kleinere, präzise Theoreme zerlegte, jeweils mit kurzem Lean-Beweis, wie sie den Meilenstein ergeben.

Lücken im veröffentlichten Beweis

Bei der Übersetzung nach Lean traten Probleme im Originalbeweis zutage. Die meisten waren klein (Tippfehler, Tabellenfehler, fallengelassene Voraussetzungen), doch Axiom zählt 34 nennenswerte Abweichungen, die gewichtigsten zum Unbalanced Group Theorem (UGT).

Ein Beispiel aus den Quasithin-Bänden von Aschbacher und Smith: Ein Lemma behauptete die Gleichheit zweier Größen. Die Agenten fanden ein Gegenbeispiel mit der Gruppe SL₂(5), bei dem eine Größe 1 war, wo 2 nötig gewesen wäre. Eine Ungleichung korrigierte das Lemma, doch spätere Argumente hatten die Gleichheit genutzt, um Fälle auszuschließen; das Team erweiterte ein früheres Argument entsprechend.

Das UGT hilft, eine ganze Gruppe aus Informationen über Untergruppen zu bestimmen. Laut Abstract des Begleitpapiers folgt unter den induktiven Annahmen der Klassifikation aus einer nichttrivialen Untergruppe ungerader Ordnung, die im Zentralisator einer Involution normal ist, dass die einfache Gruppe vom Lie-Typ in ungerader Charakteristik oder alternierend gewisser Grade ist. Axiom ging über John Walters Memoir von 1986 vor und fand explizite Gegenbeispiele zu einer dort genutzten Abschlussbehauptung: Eine Operation, die einfache Gruppen in einer bestimmten Familie halten sollte, konnte eine ausdrücklich ausgeschlossene Gruppe erzeugen. Ausgehend von PSL₂(49), dessen Körperinvolution den Zentralisator PGL₂(7) hat, entsteht die Komponente PSL₂(7), die wegen der Mersenne-Primzahl 7 ausgeschlossen ist. Diese Gegenbeispiele widerlegen laut Axiom weder das UGT noch Walters Proposition II.5.9(ii).

Die Reparatur nutzte Solomons Theorie der maximalen 2-Komponenten von 1976. Daraus erzeugte und formalisierte das System AxiomProver ein alternatives Argument. Der Schlüsselschritt, Theorem 2.3 („Erhalt einfacher Tops“), gilt laut Axiom als neues Resultat der Gruppentheorie. Zusammen mit Reduktionen von Gilman und Solomon sowie Erkennungssätzen von Foote und Harris liefert er die für die Klassifikation nötige UGT-Form. Nach der Formalisierung fanden Axiom-Mathematiker eine kürzere Herleitung (Remark 9.5), die ohne Theorem 2.3 auskommt.

Das Paper „The Unbalanced Group Theorem“ von Colin Defant und Ken Ono erschien am 27. Oktober 2026 als Version 1 auf dem Hexagon-Preprint-Server (CC BY 4.0, 35 Seiten). Axiom will mit Gruppentheoretikern die Errata sammeln und auf einer Errata-Seite veröffentlichen. Lyons und Solomon wurden zur UGT-Reparatur konsultiert und gehören zusammen mit Dan Nakano zu einem Beirat. Axiom betont, die Klassifikation bleibe die Leistung der Mathematiker, die die Gruppen entdeckten und die Argumente entwickelten.

Einordnung

Der Fall zeigt, dass KI-Agenten in großem Maßstab formale Mathematik erzeugen können, und er macht einen berühmten, schwer überprüfbaren Beweis mechanisch kontrollierbar. Dass dabei Fehler im Literaturbeweis auftauchten, aber reparierbar waren, stützt den Wert der Formalisierung. Kritisch bleibt: Die Angaben stammen vom Unternehmen selbst, eine unabhängige Prüfung der Aussage und der Errata steht noch aus. Dass der Lean-Kernel den Beweis akzeptiert, hängt zudem davon ab, dass die formale Aussage das Gemeinte korrekt abbildet. Auch ist offen, wie viel von der Leistung auf menschliche Planung und frühere Projekte wie Qiuzhen-CFSG und Mathlib entfällt. Der Beweis der zweiten Generation bleibt unvollständig.