Es galt als das unübersichtlichste Monument der modernen Wissenschaft: die Klassifikation der endlichen einfachen Gruppen, in der Fachwelt ehrfürchtig als „Enormous Theorem“ bezeichnet. Rund 15.000 Seiten mathematischer Beweistext, verteilt auf mehr als 500 Fachaufsätze von rund 100 Mathematikern über ein halbes Jahrhundert hinweg. Kein einzelner Mensch auf der Welt hat jemals alle Zeilen dieses gigantischen Gemeinschaftswerks lückenlos gelesen, verstanden und auf Fehler abgeklopft. Bis jetzt.
Das auf formale Mathematik spezialisierte KI-Startup Axiom Math hat den gesamten Beweis der ersten Generation vollständig in der formalen Programmiersprache Lean 4 rekonstruiert und von einem Software-Kernel verifizieren lassen. Das Ergebnis übertrifft bisherige Dimensionen der Computer-Mathematik bei weitem: Rund 43,1 Millionen Zeilen maschinell geprüfter Lean-Code, erzeugt in nur 24 Tagen von koordinierten KI-Agentenschwärmen. Bei der Übertragung deckte das System 34 teils gravierende Fehler in der publizierten Fachliteratur auf - und bewies kurzerhand ein eigenständiges neues mathematisches Theorem, um einen blockierten Beweispfad der menschlichen Autoren zu reparieren.
Die Atome der Symmetrie und eine 15.000-Seiten-Kathedrale
Um die Tragweite des Vorhabens zu verstehen, lohnt ein Blick auf die mathematische Bedeutung: Gruppen beschreiben in der Mathematik Symmetrien - etwa die Drehungen eines Würfels oder die Permutationen von Teilchenzuständen in der Quantenphysik. Nach dem klassischen Jordan-Hölder-Satz lässt sich jede endliche Gruppe in elementare, nicht weiter zerlegbare Bausteine zerlegen. Diese einfachen Gruppen sind gewissermaßen die chemischen Atome oder Primzahlen der Symmetrielehre.
Die Klassifikation (Classification of Finite Simple Groups, kurz CFSG) liefert ein lückenloses Periodensystem dieser Symmetrie-Atome. Sie beweist, dass jede endliche einfache Gruppe entweder zu einer von drei unendlichen Familien gehört (zyklische Gruppen mit Primzahlordnung, alternierende Permutationsgruppen sowie 16 Lie-Typ-Familien über endlichen Körpern) oder eine von exakt 26 isolierten Ausnahmen darstellt, den sogenannten sporadischen Gruppen. Die größte von ihnen, die sogenannte Monstergruppe, umfasst unvorstellbare rund 8 × 1053 Elemente.
Doch während die Entdeckung der Gruppen schrittweise voranschritt, erwies sich der Nachweis, dass es darüber hinaus wirklich keine weiteren Ausnahmen geben kann, als beispiellose Mammutaufgabe. Was in den 1960er-Jahren mit dem 255 Seiten langen Feit-Thompson-Theorem begann und 1983 von Daniel Gorenstein voreilig als vollendet ausgerufen wurde, benötigte bis ins Jahr 2004, als Michael Aschbacher und Stephen Smith in einer 1.221-seitigen Abhandlung die letzte offene Lücke der sogenannten Quasithin-Gruppen schlossen. Die resultierende Literatur war derart verstreut und von wechselnden Notationen geprägt, dass Spitzenforscher seit Jahrzehnten an einer zweiten, vereinfachten Beweisgeneration arbeiten, die bis heute unvollendet ist. Während OpenAIs jüngste Wissenschaftsoffensive vor allem neue Beweise für einzelne offene Vermutungen lieferte, ging Axiom das gesamte historische Fundament an.
24 Tage, dutzende Agenten und 43 Millionen Zeilen Code
Für die maschinelle Formalisierung wählte das Team um Gründerin Carina (Letong) Hong, Zahlentheoretiker Ken Ono, Colin Defant, Bhavik Mehta und Niels Voss bewusst die historische Erstgeneration des Beweises, da diese die einzige vollständig publizierte Route darstellt. In einem ausführlichen Forschungsbericht schildert das Team den Ablauf: Am 1. Oktober 2026 richtete das Startup einen Slack-Kanal zur Koordination ein, am 2. Oktober ging der erste Schwarm von KI-Agenten („AxiomProver“) live.
Die Architekten unterteilten das 15.000-Seiten-Monster in einen strukturierten Bauplan aus 108 Meilensteinen und rund 380 Teilaufgaben. Spezialisierte Führungs-Agenten zerlegten komplexe mathematische Lemmata in überprüfbare Unterbeweise, während andere Agenten im Hintergrund bestehende Resultate suchten oder Zeile für Zeile formalen Lean-Code schrieben. Als externe Fachberater holte Axiom namhafte Koryphäen an Bord, darunter Richard Lyons und Ronald Solomon - zwei jener Pioniere, die den ursprünglichen Beweis über Jahrzehnte hinweg selbst mitgeprägt hatten.
Die Dimensionen des nun im interaktiven Beweis-Explorer und auf GitHub freigegebenen Repositoriums stellen alles in den Schatten, was bisher in formalen Beweissystemen realisiert wurde: Das Projekt umfasst über 2,05 Millionen Deklarationen und 43,1 Millionen Zeilen Lean-Code - ein Vielfaches der gesamten globalen Standardbibliothek Mathlib. Um die Code-Masse überhaupt kompilieren zu können, mussten die Ingenieure verteilte Cache-Systeme und Compiler-Optimierungen entwickeln; der vollständige Prüflauf via Lake dauert auf Server-Hardware knapp unter 24 Stunden.
| Dimension | Menschlicher Originalbeweis (1955 bis 2004) | Axiom Lean-4-Formalisierung (2026) |
|---|---|---|
| Umfang | Ca. 15.000 Seiten in über 500 Fachaufsätzen | 43,1 Millionen Zeilen Lean-Code (2,05 Mio. Deklarationen) |
| Projektdauer | Rund 50 Jahre über mehrere Forscher-Generationen | 24 Tage via koordinierter Agentenschwarm |
| Prüfmechanismus | Dezentrale Peer-Reviews, kein Mensch las alles lückenlos | 100 % deterministisch durch Lean-Kernel verifiziert (sorry-frei) |
| Fehlerkontrolle | Zahlreiche nachträgliche Lücken (z. B. Quasithin-Fall) | 34 Literatur-Abweichungen identifiziert, 1 neues Theorem bewiesen |
Wie die KI einen publizierten Beweis kippte und ein neues Theorem erfand
Der eigentliche Erkenntnisgewinn liegt jedoch nicht im bloßen Abtippen historischer Texte, sondern in der unbarmherzigen Strenge des Lean-Compilers. Ein formaler Beweisassistent verzeiht keine unpräzisen Übergänge, keine stillschweigend vorausgesetzten Annahmen und kein mathematisches Handwaving. Das System stoppte überall dort, wo die publizierte Originalliteratur Lücken aufwies.
Insgesamt registrierte Axioms System 34 nennenswerte Abweichungen von der Fachliteratur. Viele betrafen typografische Versehen oder fehlerhafte Tabellenwerte. In Michael Aschbachers und Stephen Smiths Werk zu den Quasithin-Gruppen entdeckte die KI ein Gegenbeispiel für ein Lemma, das fälschlicherweise die Gleichheit zweier numerischer Größen behauptete: Für die Gruppe SL₂(5) betrug der Wert 1 statt der geforderten 2, was eine Anpassung der nachfolgenden Fallunterscheidung nötig machte.
Weit dramatischer verlief die Prüfung des Unbalanced Group Theorem (UGT), eines zentralen Brückenpfeilers, der von John Walter 1986 bewiesen worden war. Bei dem Versuch, Walters Argumente formal abzusichern, stießen die Agenten auf ein handfestes Gegenbeispiel zu einer grundlegenden Abgeschlossenheitsannahme: Für die projektive lineare Gruppe PSL₂(49) führt die zentrale Symmetrie zu einer Untergruppe mit der einfachen Komponente PSL₂(7), die jedoch aus der betrachteten Familie explizit ausgeschlossen war. Walters Beweisroute war an dieser Stelle schlichtweg fehlerhaft.
Das Unbalanced Group Theorem im Detail
Die mathematische Rolle: Das Theorem identifiziert eine einfache Gesamtgruppe anhand der ungeraden Ordnungsstrukturen in den Symmetrien ihrer Untergruppen.
Die historische Schwachstelle: John Walters Beweis von 1986 stützte sich auf eine Abgeschlossenheitsannahme, die bei Gegenbeispielen wie PSL₂(49) rechnerisch kollabierte.
Die Reparatur durch KI: AxiomProver überbrückte die Lücke mit Ronald Solomons Theorie maximaler 2-Komponenten und bewies Theorem 2.3 („Preservation of simple tops“).
Da ein Wechsel auf unvollendete moderne Alternativbeweise das Projekt um Jahre zurückgeworfen hätte, schlugen die Agenten in Absprache mit den Altmeistern Lyons und Solomon einen eigenständigen Ausweg ein: Basierend auf Solomons Theorie maximaler 2-Komponenten aus dem Jahr 1976 konstruierte AxiomProver eine alternative Beweisführung für den einfachen Fall. Dabei bewies die KI ein neues gruppentheoretisches Resultat, das als Theorem 2.3 („Preservation of simple tops“) formuliert und von Colin Defant und Ken Ono in einem 35-seitigen Preprint auf dem Preprint-Server Hexagon veröffentlicht wurde. Die KI half somit nicht nur beim Nachvollziehen, sondern reparierte eigenständig die historische Beweiskette.
Zwischen Faszination und der Frage nach der Spezifikation
In der internationalen Mathematik-Gemeinde sorgt der Vorstoß für enormes Aufsehen, befeuert aber auch die Debatte um die Verlässlichkeit rein maschineller Forschung, wie sie bereits nach den Resolutionen führender Fields-Medaillenträger und den Diskussionen über akademische Anerkennung bei KI-Ergebnissen entbrannt war.
Auf der Habenseite steht eine fundamentale Gewissheit: Der Lean-Kernel arbeitet deterministisch nach strengen logischen Kernaxiomen (Classical.choice, propext, Quot.sound). Im gesamten Code existiert kein einziger Platzhalter (`sorry`) und kein Ausweichen auf ungeprüfte native Rechenoperationen (`native_decide`). Ist der Kernel einmal fehlerfrei durchgelaufen, steht logisch fest, dass die Schlussfolgerungen formal korrekt aus den Prämissen folgen.
Die verbleibende Skepsis in Fachforen richtet sich daher nicht gegen die Logikprüfung, sondern gegen die Spezifikation: Ein formaler Beweis ist nur so viel wert wie die formale Definition der ursprünglichen Behauptung. Wenn die oberste Aussage unbemerkt eine Lücke enthält oder Ausnahmen anders definiert als die klassische Fachliteratur, beweist der Computer zwar eine wahre Aussage, aber womöglich nicht exakt das beabsichtigte Theorem. Axiom betont zwar, dass man die Formulierung aus dem externen Gemeinschaftsprojekt TauCeti übernommen und von Spitzenforschern habe abnehmen lassen, doch die globale Überprüfung von 43,1 Millionen Codezeilen wird die Fachwelt noch monatelang beschäftigen.
Unabhängig davon markiert das Projekt eine historische Wegmarke: Wie sich das Forschungstempo durch koordinierte Agentensysteme vervielfacht, zeigt sich nirgendwo deutlicher als an einem mathematischen Mammutwerk, an dem drei Generationen brillanter Menschen ein halbes Jahrhundert lang gearbeitet haben - und das eine Schwarm-KI in kaum mehr als drei Wochen absichert und korrigiert.
🎯 Was das für die Praxis bedeutet
1. Formale Verifikation schlägt Chatbot-Plausibilität: Reine Sprachmodelle neigen zu überzeugend klingenden Halluzinationen. Die Kopplung generativer Agenten an formale Compiler (wie Lean) beweist, wie KI-Systeme zu 100 Prozent verlässlichen, mathematisch wasserdichten Ergebnissen geführt werden können.
2. Agentenschwärme als automatische Auditoren: Was für 15.000 Seiten mathematische Fachliteratur funktioniert, revolutioniert die Qualitätskontrolle komplexer Systeme: Schwärme finden versteckte Zirkelschlüsse und Randfallfehler, die menschlichen Prüfern über Jahrzehnte entgangen sind.
3. Neuer Standard für sicherheitskritische Software: Die Fähigkeit, 43 Millionen Zeilen formalen Code koordiniert zu generieren und zu verifizieren, ebnet den Weg für die lückenlose Zertifizierung von Kryptografie, Chip-Designs und sicherheitskritischer Steuerungssoftware.
