Das Wichtigste in Kürze
- Axiom hat mit dem KI-Beweiser-Cluster AxiomProver die Klassifikation der endlichen einfachen Gruppen vollständig in Lean nachgebaut.
- Angegeben sind rund 50 Millionen Zeilen Code und eine Laufzeit von 24 Tagen; Axiom nennt das den größten computergeprüften Mathematikbeweis.
- Einen öffentlichen Build, einen Download oder eine nutzbare Projektseite gibt es bisher nicht.
Kurzüberblick
| System | AxiomProver-Cluster, Formalisierung in Lean |
|---|---|
| Umfang | rund 50 Millionen Zeilen |
| Laufzeit | 24 Tage |
| Bekanntgabe | 27. Oktober 2026 |
| Kategorie | KI & Modelle |
| Urheber | Axiom |
| Trend-Index | 🔥 3,6 Mio. Trend-Index |
| Veröffentlicht | |
| Zuletzt aktualisiert |
Der Satz, den Axiom in Lean gelegt hat
Der größte mathematische Beweis der Menschheitsgeschichte ist jetzt computergeprüft.
Axiom hat am 27. Oktober 2026 eine vollständige Auto-Formalisierung der Klassifikation der endlichen einfachen Gruppen angekündigt, auf Englisch Classification of Finite Simple Groups. In der Mitteilung heißt der Satz das Periodensystem der Symmetrie: ein Beweis von etwa 15.000 Seiten, an dem über 100 Mathematiker über mehrere Generationen gearbeitet haben.
Geleistet hat das der KI-Beweiser-Cluster AxiomProver. Die Formalisierung liegt in Lean und umfasst nach Angaben des Teams rund 50 Millionen Zeilen. Entstanden ist sie in 24 Tagen. Axiom bezeichnet das Ergebnis als den größten computergeprüften Mathematikbeweis. Gezeigt wurde das bisher in einer kurzen Vorschau zur Ankündigung.
Was an Technik und Größe feststeht
Bekannt ist die grobe Bauart: ein Cluster von KI-Beweisern, das den bestehenden Satz in Lean nachformuliert und maschinell prüft. Weiteres zur Architektur, zu Modellgewichten, zu einer API oder zu Preisen und Kontingenten nennt die Ankündigung nicht.
Der Vergleich, den Axiom selbst aufmacht, liegt zwischen dem klassischen Text und der neuen Lean-Fassung. Der menschliche Beweis ist ein Generationenwerk auf Papier; die Formalisierung ist ein sehr großes, in knapp dreiehalb Wochen erzeugtes Codekorpus.
| Fassung | Bekannte Eckdaten |
|---|---|
| Klassischer Beweis | etwa 15.000 Seiten, über 100 Mathematiker, mehrere Generationen |
| Lean-Formalisierung | AxiomProver, rund 50 Millionen Zeilen, 24 Tage |
Wofür das taugt und was offen bleibt
Sobald eine prüfbare Fassung vorliegt, wäre der natürliche Nutzen ein maschinengeprüfter Bezugstext für die Klassifikation selbst: Forschungsgruppen könnten einzelne Kapitel in Lean nachlesen, statt sich nur auf die gedruckte Überlieferung zu stützen. Dieselbe Pipeline ist außerdem ein Belastungsprobe dafür, ob ein Beweiser-Cluster einen Beweis dieser Größe überhaupt geschlossen formalisieren kann.
Du kannst AxiomProver derzeit weder laden noch über eine API ansteuern. Einen öffentlichen Build, einen Download und eine offizielle Seite hat Axiom noch nicht veröffentlicht; in den Angaben zum Projekt fällt lediglich die Adresse cfsg.axiommath.ai. Offen bleibt damit, wer die 50 Millionen Zeilen unabhängig nachprüft, welche Teile der menschlichen Vorlage wie übersetzt wurden und ob Gewichte oder Werkzeuge später offen oder nur intern bleiben.
- Prüfung des Klassikers
Eine vollständige Lean-Fassung würde den Satz Zeile für Zeile maschinell nachvollziehbar machen.
- Maßstab für große Formalisierungen
24 Tage und rund 50 Millionen Zeilen sind die konkreten Größen, an denen sich spätere Läufe messen lassen.
- Kein Zugang für Außenstehende
Ohne Build, Download oder nutzbare Seite bleibt die Formalisierung vorerst eine Ankündigung mit Vorschau.
Häufige Fragen
Kann ich AxiomProver schon selbst ausprobieren?
Nein. Veröffentlicht sind bisher weder ein Build noch ein Download noch eine nutzbare Seite. Die Formalisierung wurde nur in einer kurzen Vorschau zur Ankündigung vom 27. Oktober 2026 gezeigt.
Was genau ist die Klassifikation der endlichen einfachen Gruppen?
Axiom beschreibt sie als Periodensystem der Symmetrie: ein Beweis von etwa 15.000 Seiten, erarbeitet von über 100 Mathematikern über mehrere Generationen. AxiomProver hat genau diesen Satz in Lean formalisiert.
