Axiom meldet Lean-Prüfung der Klassifikation der endlichen einfachen Gruppen, des längsten Beweises der Mathematik

Das Start-up Axiom gibt an, die Klassifikation der endlichen einfachen Gruppen (oft CFSG abgekürzt) per Computer überprüfbar gemacht zu haben. Der Satz trägt den Spitznamen „das enorme Theorem“: ein Beweis von rund 15.000 Seiten, verteilt auf mehr als 500 Artikel von etwa hundert Mathematikern über mehrere Jahrzehnte. Die Ankündigung erschien an diesem Dienstag, dem 27. Oktober, um 15:34 Uhr Pariser Zeit auf X, begleitet von einem ausführlichen, auf den Vortag datierten Blogbeitrag, einer interaktiven Beweiskarte und einem Code-Repository.

Worum es geht

Eine Gruppe beschreibt Symmetrien, etwa die 24 Drehungen, die einen Würfel unverändert lassen. Endliche Gruppen zerfallen in unteilbare „Bausteine“, die einfachen Gruppen, ähnlich wie ganze Zahlen in Primzahlen. Die Klassifikation besagt, dass die Liste dieser Bausteine vollständig ist: zyklische Gruppen von Primzahlordnung, alternierende Gruppen (auf mindestens fünf Elementen), sechzehn unendliche Familien von Gruppen „vom Lie-Typ“ und genau 26 sporadische Gruppen, darunter die größte, die Monstergruppe. Das Resultat wird in vielen Gebieten genutzt (Algebra, Zahlentheorie, Kombinatorik), doch nur sehr wenige Menschen können es als Ganzes nachprüfen.

Axiom hat diesen Beweis in Lean neu geschrieben, einem Beweisassistenten: einer Sprache, in der jede Definition und jeder logische Schritt so präzise formuliert wird, dass ein Programm ihn kontrollieren kann. Die Projektseite nennt 43,1 Millionen Zeilen Lean und 2,05 Millionen Deklarationen.

Wie KI-Agenten eingesetzt wurden

Axioms Bericht ist vor allem einer über Organisation. Das Projekt startete am 1. Oktober 2026 mit einer Beweiskarte aus der Literatur und bereits vorhandenem Lean-Code, aufgeteilt in 108 Meilensteine und etwa 380 Aufgaben. Ab dem 2. Oktober übernahmen Schwärme von mehreren Dutzend AxiomProver-Agenten mit einer wechselnden Mischung von Modellen Aufgaben über GitHub-Tickets und meldeten Ergebnisse in Slack. „Leitende“ Agenten zerlegten schwierige Argumente und prüften Aussagen; andere suchten nach vorhandenen Resultaten oder schrieben Beweise.

Axiom verschweigt die Rückschläge nicht. Scheinbar einfache Meilensteine verbargen enorme Voraussetzungen, die die Agenten angenommen statt bewiesen hatten: Zehntausende Zeilen wurden gelöscht. Auch die Neukompilierung wurde zum Engpass, gelöst durch einen zwischen Rechnern geteilten Cache. Menschen blieben zentral: Mathematiker für inhaltliche Hürden, Ingenieure für den Betrieb des Systems.

Was die Maschine gefunden hat

Formalisieren zwingt dazu, explizit zu machen, was ein menschlicher Leser selbst ergänzt. Laut Axiom waren die meisten gefundenen Probleme geringfügig (Tippfehler, fehlerhafte Tabellen, vergessene Voraussetzungen), doch 34 nennenswerte Abweichungen von der Literatur mussten gelöst werden. Die gravierendste betrifft das Unbalanced Group Theorem in der Fassung von John Walter aus dem Jahr 1986: Die Agenten fanden Gegenbeispiele zu einem Schritt der Argumentation, ohne den Satz selbst zu widerlegen. Mit Hilfe von Richard Lyons und Ronald Solomon, zwei langjährigen Experten der Klassifikation, wurde ein anderer Weg auf Grundlage von Solomons Arbeiten von 1976 gebaut. Axiom stellt dies als neues gruppentheoretisches Resultat vor, beschrieben in einem begleitenden Paper.

Axiom verspricht, die vollständige Errata-Liste gemeinsam mit einem Gremium von Fachleuten zu veröffentlichen. Solange sie nicht online ist, bleibt die Gesamtzahl der gefundenen Fehler nicht überprüfbar.

Grenzen, die man kennen sollte

Lean prüft die Schlussfolgerungen, nicht die Bedeutung der Aussage: Menschen müssen noch kontrollieren, dass der finale Satz und seine Definitionen genau das sagen, was die Klassifikation besagt. Axiom räumt das in seinem Text ein. Zum Zeitpunkt dieses Artikels ist keine vollständige unabhängige Prüfung veröffentlicht, und wir haben das Repository nicht selbst kompiliert. Die Formalisierung beginnt auch nicht bei null: Sie übernimmt rund 1,2 Millionen Zeilen aus dem Projekt Qiuzhen-CFSG und baut auf der Bibliothek Mathlib auf.

Die Ankündigung kommt einen Tag nach den von OpenAI beanspruchten mathematischen Resultaten, über die wir hier berichtet haben. Der Ansatz ist ein anderer: OpenAI sagt, neue Resultate gefunden zu haben, Axiom sagt, ein bekanntes Resultat mechanisch geprüft und Teile davon korrigiert zu haben.