Axiom meldet sorry-freie Lean-Formalisierung der Klassifikation endlicher einfacher Gruppen

Axiom veröffentlicht sorry-freie Lean-Formalisierung der Gruppenklassifikation

Axiom Math hat laut eigener Ankündigung um den 26./27. Oktober 2026 eine vollständige Formalisierung der Klassifikation der endlichen einfachen Gruppen (CFSG) in Lean 4 veröffentlicht. Die Arbeit sei in 24 Tagen entstanden und umfasse rund 43,1 Millionen Zeilen Code. Welcher der beiden Termine stimmt, lässt sich dem Material nicht entnehmen. Eine Quelle nennt den 26., eine andere den 27. Oktober.

Das GitHub-Repository beschreibt den Beweis als sorry-frei. Er stützt sich nur auf die drei Standardaxiome Classical.choice, propext und Quot.sound; native_decide kommt nicht zum Einsatz. Grundlage sind Mathlib und das Projekt TauCeti, veröffentlicht unter Apache-2.0. Die zu beweisende Aussage übernimmt die CFSG-Formulierung aus TauCeti: Jede endliche einfache Gruppe ist isomorph zu einer Gruppe der expliziten Klassifikationsliste. Die Formalisierung folgt vor allem dem Beweis der ersten Generation.

108 Meilensteine, Agentenschwärme und menschliche Mathematiker für die schweren Fälle

Axiom zerlegte den Beweis nach eigenen Angaben in 108 Meilensteine und rund 380 kleinere Aufgaben. Leitagenten zerlegten Argumente und prüften Aussagen. Andere Agenten suchten vorhandene Resultate heraus oder schrieben Lean-Beweise. Für schwere mathematische Hindernisse sprangen menschliche Mathematiker ein; sie prüften außerdem die Endaussage. Die Gruppentheoretiker Richard Lyons und Ronald Solomon wurden zu den Argumenten konsultiert.

Das Team baute auf rund 1,2 Millionen Zeilen vorhandenen Gruppentheorie-Code auf. Welche Modelle die Agenten antrieben, nennt der Blogpost laut ai-tldr.dev nicht.

Gegenbeispiele zu einer Abschlussbehauptung im Unbalanced Group Theorem

Beim Formalisieren stieß Axiom eigener Darstellung nach auf Gegenbeispiele zu einer Abschlussbehauptung („closure assertion“). Sie steckt in einer veröffentlichten Beweisroute zum Unbalanced Group Theorem. Das zugehörige Paper (Hexagon 2610.00575, 35 Seiten) erläutert das Hindernis. Für den Fall einfacher Gruppen existiert eine alternative Argumentation auf Basis von Solomons Theorie maximaler 2-Komponenten aus dem Jahr 1976. Den Schlüsselschritt bildet Theorem 2.3.

Laut xenospectrum.com erschüttert der Fund die CFSG selbst nicht. Axiom arbeitet nach eigenen Angaben mit Gruppentheoretikern an einer Errata-Liste, die veröffentlicht werden soll. Den Befund stützt bislang allein Axiom.

„Erster vollständiger Beweis“ ist Herstellerangabe, unabhängige Prüfung fehlt

Axiom nennt das Ergebnis den „first complete computer-checked proof“ der CFSG. Das ist eine Herstellerangabe. Unabhängige Fachreaktionen oder eine externe Prüfung liegen im Material nicht vor. Zahlen und Anspruch stammen fast ausschließlich von Axiom.

Belegt sind Vorarbeiten, die ausdrücklich keine vollständige CFSG-Formalisierung darstellen. Dazu zählen das Feit-Thompson-Theorem in Coq (Gonthier et al., rund 170.000 Zeilen, laut lean-lang.org ohne Lean-Port), eine KI-gestützte Lean-Entwicklung im FormaTheoria-Paper bis zum Bender–Suzuki-Theorem sowie ein konstruktiver Lean-ATLAS einfacher Gruppen. Der Originalbeweis umfasst rund 15.000 Seiten, wie Axiom und Peter Cameron übereinstimmend angeben.

Offen bleibt, ob unabhängige Prüfer den Build nachvollziehen und die TauCeti-Aussage als korrekte Fassung der CFSG bestätigen.