Das auf Mathematik spezialisierte KI-Unternehmen Axiom gibt an, sein Agentenschwarm AxiomProver habe die Klassifikation der endlichen einfachen Gruppen (CFSG) in 24 Tagen in Lean formalisiert, und bezeichnet das als den ersten vollständig computergeprüften Beweis dieses Satzes. Der Code ist auf GitHub unter der Apache-2.0-Lizenz veröffentlicht. Laut Repository enthält die finale Version keine sorry-Platzhalter, verwendet kein native_decide und stützt sich nur auf drei Standardaxiome: Propositionale Extensionalität, das klassische Auswahlaxiom und die Korrektheit von Quotienten.
Die Klassifikation der endlichen einfachen Gruppen wird oft als „Periodensystem der Symmetrie“ bezeichnet. Sie besagt, dass jede endliche einfache Gruppe entweder zu einer von 18 unendlichen Familien gehört oder eine der 26 sporadischen Gruppen ist. Der Originalbeweis verteilt sich auf mehr als 500 Aufsätze mit etwa 15.000 Seiten, geschrieben von rund 100 Mathematikern zwischen etwa 1955 und 2004. Das letzte Stück, der Quasithin-Teil von Aschbacher und Smith, umfasst allein 1221 Seiten.
Was in den 24 Tagen geschah
Nach Axioms Darstellung wurde die Slack-Gruppe für die Zusammenarbeit am 1. Oktober eingerichtet, die ersten Agenten gingen am 2. Oktober online. Der gesamte Beweis wurde in 108 Meilensteine und etwa 380 kleine Aufgaben zerlegt; die Agenten übernahmen Aufgaben über GitHub-Issues und meldeten ihren Fortschritt in Slack. Ein führender Agent zerlegte die Probleme und prüfte die Aussagen, die übrigen suchten vorhandene Ergebnisse oder schrieben Lean-Beweise und verteilten bei fehlenden Voraussetzungen weitere Arbeit nach unten.
Reibungslos lief das nicht. Eine frühe Tranche Code wurde wegen eines Fehlers durch versteckte Annahmen komplett gelöscht, das Team plante neu. Später wurde die Build-Geschwindigkeit zum Engpass: Die Ingenieure setzten auf Caching und parallele Prüfung und lagerten endliche Berechnungen als überprüfbare Zertifikate aus, wodurch der vollständige Build auf unter 24 Stunden sank. Am 10. Oktober verkündete das Projekt vorab gesondert den Beweis, dass die Monstergruppe einfach ist.
Beim Korpus gibt Axiom an, insgesamt 715 Aufsätze und Bücher eingelesen zu haben. Wiederverwendet wurden zudem rund 1,2 Millionen Zeilen Code aus dem früheren Projekt Qiuzhen-CFSG sowie bestehende Formalisierungsbibliotheken wie Mathlib und Tau Ceti.
Nebenbei entdeckte Fehler
Bei der Formalisierung hielt das Team 34 deutlichere mathematische Abweichungen fest. Die meistbeachtete liegt auf dem Beweisweg über den „Unbalanced Group Theorem“ (UGT): Eine Abschlussbehauptung in Walters Memoiren von 1986 hat ein Gegenbeispiel, denn ausgehend von PSL₂(49) gelangt man zu PSL₂(7), das von dieser Familie gerade ausgeschlossen wird. Auch zu einem Lemma von Aschbacher und Smith fand sich ein Gegenbeispiel, SL₂(5); wenn die Gleichung zu einer Ungleichung wird, muss die nachfolgende Argumentation entsprechend erweitert werden.
Axiom veröffentlichte dazu eigens eine 35-seitige Arbeit, die ein alternatives Argument vorschlägt, und besserte diesen Beweisweg unter Mitwirkung von Beratern wie Lyons und Solomon aus. Das Unternehmen betont wiederholt, diese Gegenbeispiele widerlegten das UGT nicht, geschweige denn erschütterten sie die Klassifikation.
„the classification remains the achievement of the mathematicians who discovered the groups“
(Die Klassifikation bleibt die Leistung der Mathematiker, die die Gruppen entdeckt haben.)
Im Vergleich zu früheren maschinellen Verifikationen
Am häufigsten wird die Verifikation des Satzes von Feit-Thompson (Satz über ungerade Ordnung) herangezogen, die Gonthiers Team 2012 in Coq abschloss. Der Satz geht auf die 255-seitige Arbeit von Feit und Thompson aus dem Jahr 1963 zurück; das Projekt dauerte etwa sechs Jahre und war ein Grundpfeiler des Klassifikationsbeweises. Axiom deckt nun das ganze Gebäude ab, und die Zeit wird in Tagen gemessen.
Direkt vergleichen lässt sich die Geschwindigkeit nicht. Das Projekt zum Satz über ungerade Ordnung baute die Bibliothek damals nahezu bei null auf, während Axiom auf Mathlib und dem früheren 1,2-Millionen-Zeilen-CFSG-Code aufsetzt. Die Zahl der Agenten wird nur mit „Dutzenden“ angegeben; Rechenleistung, Hardware und Gesamtkosten dahinter sind nicht offengelegt, ebenso wenig der Personalaufwand. Die 24 Tage sind die Laufzeit des Formalisierungsprojekts selbst und schließen die Jahrzehnte menschlicher Arbeit, auf denen es beruht, nicht ein.
Einige Vorbehalte nennt das Projekt offen. Die Metadaten kennzeichnen die Prüfung als „Selbstbewertung“; bislang hat kein Dritter den vollständigen Build in einer sauberen Umgebung reproduziert. Die maschinelle Prüfung garantiert nur, dass die Herleitung aus den niedergeschriebenen Annahmen korrekt ist; ob die Definitionen der Klassifikationsaussage dem ursprünglichen Satz treu sind, müssen Gruppentheoretiker weiterhin Punkt für Punkt abgleichen. Die UGT-Arbeit erschien auf einer Preprint-Plattform ohne Peer-Review, und die Errata-Liste will Axiom auf der Projektseite veröffentlichen.
Für alle, die sich mit Formalisierung beschäftigen, sind als Nächstes zwei Dinge entscheidend: ob die Community die 43,1 Millionen Zeilen unabhängig durchlaufen lassen kann und wie viele der 34 Abweichungen von den ursprünglichen Autoren bestätigt werden.
Quellen: Projektankündigung und GitHub-Repository von Axiom, Unite.AI, CocoLoop, Kingy AI; Zeilenzahl des Lean-Codes, Zahl der Deklarationen, Meilensteine und Abweichungen nach den von Axiom veröffentlichten Angaben, Dauer der Verifikation des Satzes über ungerade Ordnung nach Unterlagen von Microsoft Research.