KI beweist den „Monster-Satz“: 15.000 Seiten Mathematik in 24 Tagen formalisiert

Worum es geht

Das US-Unternehmen Axiom, das KI für Mathematik entwickelt, hat am 27. Oktober 2026 eine ungewöhnlich große Leistung verkündet: Seine KI-Agenten haben den Satz zur Klassifikation der endlichen einfachen Gruppen (englisch CFSG) vollständig in Lean formalisiert. Lean ist ein Beweisassistent, also ein Programm, das mathematische Beweise Schritt für Schritt maschinell prüft. CFSG gilt als längster Beweis der Menschheit, er wird auch „Riesensatz“ (Enormous Theorem) genannt. Der Code ist auf GitHub öffentlich. Alle Angaben stammen aus einem chinesischsprachigen Bericht (DeepTech über cnyes) und beruhen im Wesentlichen auf Axioms eigener Darstellung.

Was Formalisierung bedeutet und warum sie gerade jetzt wichtig ist

KI-Systeme erzeugen Beweise immer schneller. Laut dem Bericht veröffentlichte OpenAI am 6. Oktober 722 intern generierte mathematische Manuskripte zu Hunderten offener Probleme und am 26. Oktober weitere Ergebnisse. Die Frage lautet: Wie prüft man, ob das stimmt?

Eine Antwort ist die formale Verifikation. Dabei wird ein Beweis in eine streng formale Sprache übersetzt. Floskeln wie „offensichtlich“ oder „analog folgt“ gelten in Lean nicht: Jede Zwischenfolgerung und jede stillschweigende Voraussetzung muss ausgeschrieben sein, und der Lean-Kern prüft jeden Schritt.

Der „Riesensatz“

Mathematiker beschreiben Symmetrien mit Gruppen. Ein Würfel hat 24 Drehungen, die ihn unverändert aussehen lassen; diese Drehungen samt Verknüpfungsregeln bilden eine Gruppe. So wie sich Zahlen in Primzahlen zerlegen lassen, lassen sich endliche Gruppen in unzerlegbare Bausteine zerlegen, die endlichen einfachen Gruppen.

CFSG listet sie alle auf: zyklische Gruppen von Primzahlordnung, alternierende Gruppen, 16 Familien von Lie-Typ-Gruppen und 26 „sporadische“ Gruppen, die in keine Familie passen. Die größte, die Monstergruppe, hat etwa 8×10^53 Elemente. Man nennt die Liste oft das Periodensystem der Symmetrie.

Die Liste aufzustellen war vergleichsweise leicht; schwer war der Nachweis, dass nichts fehlt. Die Arbeit begann in den 1950er-Jahren. John Thompson erhielt dafür 1970 die Fields-Medaille und 2008 den Abelpreis. 1983 erklärte Daniel Gorenstein die Klassifikation für abgeschlossen, doch der Fall der „quasi-dünnen Gruppen“ stützte sich auf ein unfertiges Manuskript. Die Lücke schlossen erst 2004 Michael Aschbacher und Stephen Smith mit einer 1.221-seitigen Monografie; 2008 wurde eine weitere Lücke gestopft. Das gilt heute als „erster Beweis“.

Der Beweis ist über Jahrzehnte verstreut, mit unterschiedlichen Notationen und vielen gegenseitigen Verweisen. Seit Ende der 1980er-Jahre entsteht ein systematischerer „zweiter Beweis“; 2023 waren 10 Bände erschienen, mindestens 12 sind geplant. Viele Resultate in Algebra, Zahlentheorie, Kombinatorik und mathematischer Physik setzen CFSG voraus.

Das Unternehmen Axiom

Axiom wurde im März 2025 gegründet. Gründerin und CEO ist Carina Hong, die in Guangzhou aufwuchs, am MIT studierte, den Morgan Prize erhielt, als Rhodes-Stipendiatin nach Oxford ging und ihr Stanford-Doktorat zugunsten der Gründung abbrach. „Gründungsmathematiker“ ist Ken Ono. Laut Bericht sammelte Axiom 64 Millionen US-Dollar Seed- und 200 Millionen Dollar Series-A-Kapital ein; die Bewertung liege über 1,6 Milliarden Dollar. Das System AxiomProver koordiniert mehrere KI-Agenten. Im August hatte das Team bereits den „246-Satz“ über Primzahllücken formalisiert. Ono sagt sinngemäß, die Welt werde bald auf Code laufen, den niemand gelesen hat; formalisierte Beweise seien dafür ein Testfeld.

Wie die 24 Tage abliefen

Axiom startete nicht bei null. Die Lean-Bibliothek Mathlib lieferte Grundlagen, und ein früheres CFSG-Projekt (angeregt von Shing-Tung Yau, getragen von Studierenden der Tsinghua-Universität und dem Yau-Zentrum) hatte viel Gruppentheorie-Code angesammelt; etwa 1,2 Millionen Zeilen übernahm Axiom. Das Team erstellte anhand des zweiten Beweises eine Beweiskarte mit 108 Meilensteinen und rund 380 Teilaufgaben. Formalisiert wurde aber der erste Beweis, weil der zweite noch unfertig ist.

Am 2. Oktober gingen die ersten Agentenschwärme online. Ein koordinierender Agent zerlegte Argumente und prüfte die Formulierung der Aussagen, andere suchten bekannte Resultate und schrieben Lean-Code. Fehlte eine Vorstufe, wurde sie anderen Agenten übergeben; fertige Teile flossen in eine gemeinsame Codebasis. Menschliche Mathematiker lösten fachliche Engpässe, Ingenieure hielten das System am Laufen.

Anfangs lief es holprig: Agenten schrieben unbewiesene Voraussetzungen einfach als gegeben hin. Zehntausende Zeilen wurden gelöscht und neu erstellt. Am 10. Oktober meldete das Team den Beweis der Einfachheit der Monstergruppe samt Nachweis ihrer Existenz, eine zentrale Etappe. Drei Tage später stockte alles; an einem Tag wurde nur ein Meilenstein erreicht. Die Meilensteine waren zu grob, also teilte man sie in kleinere, präzisere Sätze auf.

Zudem wuchs der Code schneller, als Lean ihn prüfen konnte: Änderte sich ein gemeinsamer Satz, mussten alle abhängigen Teile neu geprüft werden, und Agenten auf verschiedenen Maschinen rechneten doppelt. Ein Cache-System, das unveränderte Teile wiederverwendet, beschleunigte die Prüfung laut Bericht um mehrere Größenordnungen. Am 26. Oktober war die Formalisierung fertig: Der Lean-Kern bestätigte die lückenlose Kette von den Grundaxiomen bis zum Klassifikationssatz.

Fehler in der Literatur

Die Zeile-für-Zeile-Übersetzung wirkte wie ein Gesundheitscheck der Literatur. Viele von den Agenten gemeldete Verdachtsfälle beruhten auf eigenen Fehllesungen. Bestätigt wurden vor allem Tippfehler, falsche Tabellenwerte und fehlende Voraussetzungen; dazu kommen 34 Abweichungen von der veröffentlichten Literatur, die gesondert behandelt werden mussten. Axiom will mit Gruppentheoretikern eine Fehlerliste veröffentlichen.

Der härteste Fall war das Unbalanced Group Theorem. Der Gesamtbeweis arbeitet per Widerspruch: Man nimmt eine einfache Gruppe an, die nicht auf der Liste steht, wählt die kleinste und schließt mögliche Strukturen nacheinander aus. Das genannte Theorem schließt eine große Klasse davon aus. Das Team folgte John Walters Argument von 1986, doch die Agenten fanden ein Gegenbeispiel zu einer Behauptung darin: Eine bestimmte Operation bleibt nicht immer innerhalb einer Gruppenfamilie, sondern kann Gruppen erzeugen, die gerade außerhalb liegen. Der Satz selbst bleibt gültig, aber ein Schlüsselschritt des Originalarguments war unbegründet.

Eine andere veröffentlichte Route hätte viele weitere unformalisierte Vorresultate nach sich gezogen. Das Team fragte deshalb Richard Lyons und Ronald Solomon, die an der Klassifikation mitgearbeitet hatten. Lyons ordnete mögliche Wege und deren Geschichte, Solomons Theorie der „maximalen 2-Anteile“ von 1976 lieferte die Kernidee. AxiomProver konstruierte und formalisierte daraufhin eine neue Argumentationslinie und bewies dabei ein bisher unbekanntes gruppentheoretisches Ergebnis (Preprint auf Hexagon). Später fanden Axioms Mathematiker innerhalb der Methoden des ersten Beweises einen kürzeren Weg ohne dieses neue Resultat; beide Routen bleiben im Papier dokumentiert.

Reaktionen und Einordnung der Debatte

Eine Woche vorher sprachen Terence Tao und Yu Deng im Podcast der SAIR Foundation über KI und Mathematik. Im September hatten die beiden mit 23 weiteren Fields-Medaillengewinnern kritisiert, dass KI-Firmen das Lösen von Mathematikproblemen als Leistungstest nutzen. Deng unterscheidet zwei Grenzen: Probleme, für die ein Beweis existiert, und Probleme, deren Beweis Menschen verstehen. Früher fielen sie zusammen, jetzt gibt es Beweise, die nur KI versteht. Tao nannte die Massenproduktion von KI-Beweisen eine Art „Giftmüll“, den Mathematiker verarbeiten müssten, und wünscht sich, dass KI-Firmen Mathematiker von Anfang an einbinden. Laut Bericht passt das CFSG-Projekt dazu: Es gab eine Roadmap, Beteiligte des Originals griffen an Schlüsselstellen ein. Auch die im Juni veröffentlichte, von der IMU unterstützte „Leidener Erklärung zu KI und Mathematik“ nennt unzuverlässige Ergebnisse als Hauptrisiko.

Einordnung

Der Bericht beschreibt eine echte Infrastrukturleistung: Ein jahrzehntelang auf Vertrauen und kollektivem Gedächtnis ruhender Beweis wird nachvollziehbar und maschinell prüfbar; Forschende können Abhängigkeiten verfolgen und Module wiederverwenden. Kritisch bleibt: Die Angaben stammen von Axiom und einem Medienbericht, eine unabhängige Prüfung steht laut Bericht noch aus. Entscheidend ist, ob die formalen Definitionen und der Satz exakt dem gemeinten CFSG entsprechen – das kann Lean nicht selbst beurteilen. Ebenfalls offen: Der zweite Beweis ist unvollendet, und die Fehlerliste ist noch nicht veröffentlicht. Die Quelle 2 (Pramaana Labs, Finanzierung für Lean-basierte Verifikation in Recht und Medizin) behandelt eine andere Geschichte und fließt hier nicht ein.