Axioms KI-Agenten formalisieren die Klassifikation endlicher einfacher Gruppen in Lean

Axiom Math gab am 26. Oktober 2026 bekannt, dass es den ersten vollständigen computergeprüften Beweis der Klassifikation endlicher einfacher Gruppen veröffentlicht hat, geschrieben im Lean-Beweisassistenten [1]. Über 24 Tage hinweg leiteten seine Ingenieure und Mathematiker Schwärme von Dutzenden KI-Agenten, die etwa 43,1 Millionen Zeilen Lean-Code produzierten [1][2].

Was hat Axiom formalisiert?

Die Klassifikation, oft als enormer Satz bezeichnet, listet die Bausteine aller endlichen Gruppen auf, der Mathematik der Symmetrie [1]. Sie besagt, dass jede endliche einfache Gruppe zyklisch von Primzahlordnung, alternierend, vom Lie-Typ oder eine von 26 sporadischen Gruppen ist [2].

Axiom sagt, der ursprüngliche Beweis umfasst etwa 15.000 Seiten in mehr als 500 Artikeln von etwa 100 Mathematikern [1]. Seine Lean-Version folgt dem Beweis der ersten Generation und ist laut der GitHub-Seite des Projekts sorry-frei, was bedeutet, dass kein Schritt unbeweisen bleibt [3].

Axiom sagt, seine KI-Agenten haben etwa 43,1 Millionen Zeilen Lean in 24 Tagen produziert, um die Klassifikation zu formalisieren. Die Projektseite listet 2,05 Millionen Deklarationen und 715 Papers und Bücher im Korpus auf [2]. Axiom sagt, die Formalisierung enthält etwa 1,2 Millionen Zeilen aus einem früheren Projekt, Qiuzhen-CFSG, und baut auf der Mathlib-Bibliothek auf [1].

Wie hat der Agentenschwarm funktioniert?

Axiom eröffnete am 1. Oktober 2026 einen Slack-Kanal für das Projekt, und der erste Schwarm ging am 2. Oktober live [1]. Eine aus der Literatur abgeleitete Beweiskarte teilte die Arbeit in 108 Meilensteine und etwa 380 kleinere Aufgaben, die Agenten über GitHub-Issues übernahmen [1].

Leitende Agenten zerlegten schwierige Argumente und prüften Aussagen, während andere nach bestehenden Ergebnissen suchten oder Lean-Beweise schrieben [1]. Menschliche Mathematiker kümmerten sich um mathematische Hindernisse und Ingenieure hielten das System am Laufen [1]. Axiom sagt, es habe Zehntausende Zeilen gelöscht, die auf unbeweisenen Annahmen basierten, und Teile der Arbeit neu gestartet [1].

Am 10. Oktober verkündete laut Axiom eine Nachricht im Kanal, dass die Agenten bewiesen hatten, dass die Monstergruppe einfach ist [1]. Lean prüft die Deduktionen, während Menschen die finale Aussage und Definitionen prüfen, um zu bestätigen, dass sie das beabsichtigte Theorem ausdrücken [1].

Welche Fehler haben die KI-Agenten gefunden?

Axiom sagt, die meisten gefundenen Probleme seien geringfügig gewesen, wie Tippfehler, Fehler in Tabellen oder fehlende Hypothesen [1]. Axiom fand 34 bemerkenswerte Abweichungen vom veröffentlichten Bericht, die gelöst werden mussten. Der wesentlichste Fall betraf das Unbalanced Group Theorem [1][2].

Dort fanden die Agenten Gegenbeispiele zu einer Abschlussbehauptung in John Walters Argument von 1986, was einen wichtigen Schritt ungerechtfertigt ließ, ohne das Theorem selbst zu widerlegen [1]. Ein alternatives Argument, das auf Ronald Solomons Theorie maximaler 2-Komponenten von 1976 aufbaute, wurde zu einem neuen Ergebnis, das in einem 35-seitigen Paper verfasst wurde [1][2]. Solomon und Richard Lyons, die am ursprünglichen Beweis mitgearbeitet hatten, wurden konsultiert [1].

Hat jemand außerhalb von Axiom den Beweis geprüft?

Noch nicht, laut RuntimeWire [4]. Carina Hong, Axioms CEO, sagte gegenüber RuntimeWire, dass bisher keine externe Gruppe den Beweis neu aufgebaut und überprüft hat. Axiom veröffentlicht die Build-Artefakte, damit andere ihn reproduzieren können [4].

Die GitHub-Seite sagt, ein einzelner Build-Befehl prüft das gesamte Projekt, und dass Axiom ausstehende Änderungen an Lake, Leans Build-Tool, nutzte, um die Build-Zeit unter 24 Stunden zu halten [3]. The AI Pin berichtete über OpenAIs separate Behauptungen neuer mathematischer Entdeckungen am 27. Oktober.

Unsere Einschätzung

Meinung: Die Prüfung eines Beweises, den kein einzelner Mensch je vollständig gelesen hat, ist eine überzeugendere Nutzung von KI in der Mathematik als die Jagd nach neuen Schlagzeilen, und das Finden von 34 realen Abweichungen zeigt, dass die Prüfung Substanz hatte. Das Ergebnis ist jedoch nur so stark wie seine externen Checks, daher sind ein unabhängiger Neuaufbau und eine gruppentheoretische Errata-Prüfung wichtiger als die Zeilenzahl.

Was wir nicht verifizieren konnten

• Ob der 43,1-Millionen-Zeilen-Beweis außerhalb von Axiom baut und prüft; laut RuntimeWire hatte bis zum 27. Oktober 2026 keine externe Gruppe einen Neuaufbau abgeschlossen.
• Welche KI-Modelle die Agenten antrieben; Axiom sagt nur, sie hätten einen wechselnden Mix von Modellen verwendet.
• Wie unabhängige Gruppentheoretiker das Ergebnis bewerten; wir fanden keine veröffentlichte Reaktion eines Gruppentheoretikers außerhalb von Axioms Beraterkreis zum Zeitpunkt der Veröffentlichung.
• Die vollständige Liste der 34 bemerkenswerten Abweichungen; Axiom sagt, es werde die Errata-Liste nach Konsultation mit Gruppentheoretikern veröffentlichen.
• Ob das neue Paper zum Unbalanced Group Theorem einer Peer-Review standhält; es ist auf Hexagon veröffentlicht, und wir konnten keine Peer-Review in einer Zeitschrift bestätigen.