In nur sieben Monaten hat die KI die Arbeitsleistung von über fünfzehn Mathematikern innerhalb von sechs Jahren vollbracht, Millionen von Codezeilen geschrieben und das Projekt zur Verifikation extrem umfangreicher mathematischer Beweise herausgefordert.

Klassifikation endlicher einfacher Gruppen (CFSG) zählt zu den umfangreichsten Beweisprojekten in der modernen Mathematik.

Dieser Beweis wurde von Hunderten von Mathematikern über Jahrzehnte hinweg in gemeinsamer Arbeit abgeschlossen, seine Ergebnisse verteilen sich auf Hunderte von Aufsätzen und Monographien, die Gesamtlänge beträgt fast zwanzigtausend Seiten, und sein Umfang übersteigt bei weitem die Grenzen, die eine einzelne Person oder sogar ein einzelnes Team vollständig nachprüfen kann.

Vor diesem Hintergrund wird die Einführung von KI-Unterstützung für groß angelegte formale Verifikation zu einem neuen Weg, der unbedingt ausprobiert werden muss.

Um die Entwicklung von AI for Math voranzutreiben, unter der Anregung von Herrn Shing-Tung Yau, haben Studierende des Spitzenprogramms der Qiuzhen-Akademie der Tsinghua-Universität sowie Forschungsteams des Shing-Tung Yau Center für Mathematische Wissenschaften, des Forschungsinstituts für Intelligente Industrie und der Universität Warwick FormaTheoria – ein KI-gestützter Arbeitsablauf für die mathematische Forschung vorgeschlagen: Die KI soll ausgehend von der ursprünglichen mathematischen Literatur Abhängigkeiten automatisch strukturieren, Wissenssysteme integrieren und formale Beweise konstruieren, die schließlich schrittweise vom Lean-Beweisassistenten überprüft werden.

Bis August 2026 hat FormaTheoria die Lean-Formalisierung von vier wichtigen Theoremen abgeschlossen und mehr als 994.000 Zeilen miteinander verbundenen kodierten mathematischen Theorien erzeugt. Obwohl noch ein langer Weg bis zur vollständigen Verifikation der Klassifikation endlicher einfacher Gruppen vor uns liegt, ist dieses Ergebnis bereits ein wichtiger Meilenstein auf dem Weg zu diesem endgültigen Ziel.

CFSG liefert ein zugrundeliegendes System für zahlreiche wichtige mathematische Ergebnisse

„Klassifikation endlicher einfacher Gruppen“ klingt sehr abstrakt. Im Volksmund gesagt, ist es wie eine „Grundteilliste“ für endliche Symmetrien: Jede komplexe endliche symmetrische Struktur kann schichtenweise zerlegt werden, bis man eine Reihe von unzerlegbaren Grundeinheiten erhält; und die Funktion von CFSG besteht darin, Mathematikern mitzuteilen, welche diese Grundeinheiten genau sind.

Normalerweise zerlegt die mathematische Forschung ein komplexes Problem zuerst in diese Grundeinheiten und bearbeitet sie dann gemäß der vollständigen Liste, die CFSG bereitstellt, kategorieweise. Daher wird CFSG zu einer Infrastruktur, die andere Beweise jederzeit aufrufen können. Wenn diese „Infrastruktur“ versteckte Lücken aufweist, können zahlreiche nachfolgende Ergebnisse, die auf ihren relevanten Schlussfolgerungen basieren, beeinträchtigt werden.

Einige professionelle Übersichten liefern quantitative Beweise für die Anwendung von CFSG. Die American Mathematical Society veröffentlichte 2018 speziell die Monographie „Applying the Classification of Finite Simple Groups: A User’s Guide“ von Stephen D. Smith. Das gesamte Werk umfasst 231 Seiten und 10 Kapitel, in denen die Anwendungsszenarien von CFSG strukturiert werden. Das öffentliche Verzeichnis der letzten zwei Kapitel des Buches listet 14 nummerierte Anwendungsthemen auf, darunter distanztransitive Graphen, die Frobenius-Vermutung, Permutationsgruppenalgorithmen, das Untergruppenwachstum endlich erzeugter Gruppen, Körpererweiterungen, Überlagerungen von Riemann-Flächen, das Waring-Problem in der Gruppentheorie, Expansionsgraphen und approximative Gruppen.

Der Anwendungswert von CFSG wurde auch auf höchster Ebene der internationalen mathematischen Gemeinschaft anerkannt. Der Internationale Mathematikerkongress 2014 lud Robert Guralnick, Preisträger des Cole-Preises für Algebra der American Mathematical Society von 2018, zu einem Themenvortrag mit dem Titel „Applications of the Classification of Finite Simple Groups“ ein.

Zu diesen Anwendungen gehören wichtige Ergebnisse mit großer akademischer Einflussnahme. CFSG ist ein zentrales Glied in der vollständigen Beweiskette des eingeschränkten Burnside-Problems, und Efim Zelmanov erhielt 1994 die Fields-Medaille für die Lösung dieses Problems. Smiths Monographie listet außerdem Richtungen wie das Waring-Problem über endliche einfache Gruppen und Expansionsgraphen als wichtige Anwendungsrichtungen von CFSG auf, und relevante repräsentative Arbeiten wurden in „Annals of Mathematics“ veröffentlicht (zum Waring-Problem; Durchmesser endlicher einfacher Gruppen und ihre Anwendungen). Diese Beispiele zeigen, dass CFSG bereits eine Reihe wichtiger Arbeiten unterstützt hat, die Top-Akademiepreise gewonnen und in den führenden mathematischen Zeitschriften erschienen sind.

In diesem Sinne ist CFSG zu einem wiederholt verwendeten zugrundeliegenden System geworden. Je mehr nachgelagerte Ergebnisse sich ansammeln, desto wichtiger wird die Verifikation seiner Korrektheit und Nachprüfbarkeit. Die verfolgbare und reproduzierbare maschinelle Überprüfung von CFSG gewinnt eine Bedeutung, die über die Gruppentheorie selbst hinausgeht.

Die Schwierigkeit besteht jedoch darin, dass die Beweise dieses zugrundeliegenden Systems aus verschiedenen Epochen, von verschiedenen Autoren und aus verschiedenen Dokumenten stammen, die verwendeten Symbole, Definitionen und Standardbedingungen oft nicht übereinstimmen, und ein Zitat sogar auf eine ganze andere Reihe von Dokumenten verweisen kann. In der Geschichte wurde eine wichtige Lücke im Klassifikationsbeweis erst mehr als zwanzig Jahre später durch eine zweibändige Monographie mit insgesamt 1220 Seiten geschlossen. FormaTheoria muss nicht nur schrittweise jede einzelne Schlussfolgerung überprüfen, sondern auch prüfen, ob Definitionen, Bedingungen und Zitate zwischen Hunderten von Dokumenten vollständig zusammenpassen, um schließlich eine bruchlose Beweiskette zu bilden.

Wie KI ein extrem groß angelegtes Beweisprojekt vorantreibt

Viele KI-Mathematiksysteme stehen vor einer bereits vorbereiteten Aufgabe, bei der Aufgabe, Definitionen und Werkzeuge vollständig bereitstehen, und die KI ist nur für die Suche nach dem Beweis verantwortlich. FormaTheoria ist anders: Es muss zuerst die mathematische Grundlage hinter der Aufgabe aus einer Menge verstreuter Dokumenten rekonstruieren und dann den Beweis abschließen. Diese Arbeit steht hauptsächlich vor vier Schwierigkeiten:

Erstens weiß das System im Voraus nicht, wie viele Materialien es einsehen muss.

Ein Zitat kann zu einem weiteren Aufsatz führen, und dieser Aufsatz wiederum kann weitere vorausgehende Arbeiten nach sich ziehen. Ursprünglich gab es im Projekt nur 3 Hauptquellen, während des Beweises wurden 12 weitere Quellen entdeckt; später ergänzte Materialien machen 65,6 % aller eingesehenen Seiten aus. Die Verarbeitungsmethode von FormaTheoria lautet: Sobald ein fehlendes vorausgehendes Theorem entdeckt wird, wird der aktuelle Beweis angehalten, diese Abhängigkeit wird gesucht und formalisiert, bevor zum ursprünglichen Aufgaben zurückgekehrt und weitergearbeitet wird. Die bereits überprüften Ergebnisse werden in einem einheitlichen Wissensspeicher gespeichert, sodass sie für nachfolgende Beweise wiederholt abgerufen werden können.

Zweitens lassen sich verschiedene Dokumente kaum direkt zusammenfügen.

Verschiedene Autoren verwenden unterschiedliche Definitionen, Symbole und Standardbedingungen. Zwei Definitionen können mathematisch völlig äquivalent sein, aber sobald sie in Lean-Code geschrieben werden, können sie inkompatibel zueinander sein. FormaTheoria vergleicht wiederholt das Originaldokument und den vorhandenen Code, um die erforderlichen Umwandlungsbeziehungen aufzubauen. Gleichzeitig schützt das System bereits überprüfte mathematische Aussagen und prüft, ob jede Korrektur nachfolgende Beweise beeinträchtigt. Auf diese Weise können mehrere unabhängige Werke und Aufsätze schrittweise in denselben theoretischen Rahmen integriert werden.

Drittens kann der Code, der die Prüfung besteht, das Originaldokument dennoch falsch verstehen.

Lean prüft nur, ob die Beweislogik konsistent ist und die Schlussfolgerung aus den Voraussetzungen folgt, kann aber nicht beurteilen, ob diese Schlussfolgerung dem Originaldokument treu bleibt. Die KI kann leicht eine Bedingung übersehen, „alle“ und „es existiert“ verwechseln oder sogar die Schlussfolgerung falsch verändern. Dafür hat FormaTheoria eine unabhängige Prüfstufe eingerichtet: Die Übersetzungskomponente erstellt zuerst die Lean-Aussage, dann prüft die Prüfkomponente Punkt für Punkt anhand des Originaldokuments. In 14 Dokumentenabschnitten der Aufsatzanalyse wurden die Erstantworten der Übersetzung in 11 Abschnitten zur Überarbeitung zurückgeschickt. Dieser unabhängige Prüfmechanismus wird damit zu einer zweiten „Sicherung“ neben der maschinellen Überprüfung.

Viertens können die Originaldokumente selbst Probleme aufweisen.

In alten Dokumenten können Druckfehler, fehlende Bedingungen oder unklare Formulierungen auftreten. FormaTheoria behält die ursprünglichen Seiten bei, um später bei Widersprüchen im Beweis zurückzuverfolgen und nachzuforschen. Wenn das Dokument eine Korrektur unterstützt, ergänzt das System Bedingungen oder baut Kompatibilitätsbeziehungen auf; wenn die Beweise unzureichend sind, zeichnet das System das Problem auf und übergibt es an Mathematiker zur Beurteilung.

Darüber hinaus erfordert dieses Projekt, dass die KI über einen langen Zeitraum hinweg den Rhythmus beibehält. Ein einziger Dialog kann die vollständige Aufgabe nicht aufnehmen. Dazu verwendet FormaTheoria ein ständig aktualisiertes „Beweiskarte“ zur Verwaltung des Fortschritts: Schwere Ziele werden in kleinere Hilfssätze zerlegt, erfolgreiche Ergebnisse werden schichtenweise zum Haupttheorem zurückgeführt, und fehlgeschlagene Wege werden ebenfalls aufgezeichnet, um zu vermeiden, dass das System wiederholt in dieselbe Sackgasse gerät.

Bei der Parallelstrategie gibt es spezielle Entwürfe im Projekt. Unabhängige Aufgaben können gleichzeitig vorangetrieben werden; wenn mehrere Aufgaben auf dasselbe vorausgehende Ergebnis treffen, erledigt das System es nur einmal und erlaubt anderen Aufgaben, es wiederzuverwenden. Und die gemeinsamen mathematischen Inhalte, die bei einer Änderung weitreichende Auswirkungen haben können, werden nacheinander einzeln modifiziert, um Konflikte zu vermeiden. Kontrollierte Experimente im Aufsatz zeigen, dass diese abhängigkeitsbewusste Parallelität bei den getesteten Aufgaben eine 4,2-fache Beschleunigung erreicht hat.

Daraus bildet FormaTheoria eine vollständige Arbeitskette: Dokumente suchen, Abhängigkeiten ergänzen, Originaltexte übersetzen, Beweise konstruieren, maschinell prüfen, unabhängig überprüfen, Konflikte koordinieren und unklare Probleme an Mathematiker übergeben. Jeder Schritt ist verantwortungsbewusst und nachvollziehbar. Genau dies ist eine Konstruktion, die auf die tatsächlichen Schwierigkeiten reagiert, die in extrem groß angelegten Beweisprojekten auftreten, und die KI befähigt, verstreute mathematische Dokumente schrittweise zu einem prüfbaren, verfolgbaren und erweiterbaren Theoriegebäude zu verbinden.

△

Sieben Monate, vier wichtige Theoreme, fast eine Million Zeilen überprüfbarer Code

Am 22. Januar 2026 reichte FormaTheoria erstmals Code ein. Bis zum 2. August 2026 hat das Projekt eine wichtige theoretische Kette bis zum Bender–Suzuki-Theorem durchlaufen und nacheinander die Beweise für das Feit–Thompson-Theorem ungerader Ordnung, das Glauberman-Z*-Theorem und das Brauer–Suzuki-Theorem abgeschlossen.

Diese vier Theoreme sind nicht voneinander isoliert, sie bilden eine wichtige zusammenhängende Linie in der Klassifikation endlicher einfacher Gruppen, wobei der Beweis des letzten Theorems oft auf dem riesigen mathematischen Fundament aufbaut, das von dem vorherigen gelegt wurde.

Der Projekt-Schnappschuss zum Zeitpunkt des Abschlusses der oben genannten Beweise umfasst:

• Mehr als 994.000 Zeilen Lean-Code;
• Mehr als 850 Code-Dateien;
• Das System hat insgesamt 15 Bücher und Aufsätze mit insgesamt 1037 Seiten eingesehen, von denen etwa zwei Drittel schrittweise im Laufe des Beweises entdeckt wurden.

Natürlich kann die Anzahl der Codezeilen nur eine Seite des Projektumfangs zeigen. Wenn man vom Bender–Suzuki-Theorem als Endpunkt rückwärts verfolgt, hat das Projekt bereits ein Beweisnetz mit 30.298 mathematischen Aussagen und 186.187 Abhängigkeitsbeziehungen gebildet, wobei die längste Abhängigkeitskette 458 Ebenen erreicht. Wenn die relevanten Inhalte in der Lean-Bibliothek mitgezählt werden, erweitert sich dieses Netz auf 74.922 Aussagen und mehr als 1,44 Millionen Abhängigkeitsbeziehungen. Man kann sagen, dass hinter fast einer Million Zeilen Code ein verzweigtes, eng vernetztes Beweisnetz steht. Diese Forschung zeigt, dass KI-Agenten unter der gemeinsamen Wirkung von maschineller Überprüfung und schichtenweiser Prüfung große, extrem lang andauernde mathematische Projekte kontinuierlich vorantreiben können.

Der tatsächliche Betriebsprozess des Projekts weist ebenfalls Merkmale extrem langer Laufzeiten auf. Die längste im Aufsatz aufgezeichnete Ausführung eines Agenten dauerte 9,17 Tage, währenddessen das System die gesammelten Informationen 606 Mal komprimierte und strukturierte und gleichzeitig stets das aktuelle Beweisziel, die bereits abgeschlossenen Ergebnisse und die noch zu lösenden Probleme beibehielt. Diese Daten zeigen, dass das Projekt ein sich ständig weiterentwickelndes extrem lang andauerndes Beweisnetz verwaltet, das durch eine einzelne Generierung oder einen einzigen Dialog nicht so komplexen Prozess abdecken kann.

Bisher war die groß angelegte mathematische Formalisierung stark auf menschlichen Einsatz angewiesen, der normalerweise mehrere Jahre lang fortwährende Zusammenarbeit von mehreren Forschern erfordert. Ein vergleichbarer historischer Bezug: Die vorherige Rocq-Formalisierungsversion des Feit–Thompson-Theorems wurde von etwa 15 Personen in sechs Jahren abgeschlossen. FormaTheoria hat jedoch in sieben Monaten den gesamten Inhalt dieses menschlichen Projekts abgeschlossen und darüber hinaus die Formalisierung anderer wichtiger Theoreme vorangetrieben. Sieben Monate sind für eine KI-Agentenaufgabe immer noch eine extrem lange Laufzeit, aber im Vergleich zur traditionellen manuellen Formalisierung verkürzt die Beteiligung der KI die Zeitdauer des Projekts erheblich.

△

Formalisierung lässt versteckte Probleme in Dokumenten nach und nach ans Licht kommen

Mathematische Dokumente richten sich normalerweise an Forscher, die mit diesem Gebiet vertraut sind. Daher lassen Autoren oft Bedingungen aus, die bereits im vorherigen Text erschienen sind, oder gehen davon aus, dass die Leser die Äqu