Dutzende Agenten haben innerhalb von 24 Tagen ein gigantisches Projekt der mathematischen Fachwelt in Angriff genommen und dabei eine vor 40 Jahren bestehende Lücke aufgedeckt.

Mehr als 100 Spitzenmathematiker haben Jahrzehnte damit verbracht, 15.000 Seiten an Beweisen zu verfassen.

Jetzt hat die KI nur 24 Tage gebraucht, um eines der größten Projekte in der Geschichte der menschlichen Mathematik in mehr als 43 Millionen Zeilen Code umzuwandeln, der schrittweise von Computern überprüft werden kann.

Noch erstaunlicher ist: Bei der Überprüfung der von diesen Mathematikern hinterlassenen Beweise hat die KI eine seit fast 40 Jahren bestehende Lücke in der Argumentation aufgedeckt.

Dies ist keine Mathematik-Olympiade-Aufgabe und keine mehrere Dutzend Seiten lange mathematische Arbeit, sondern der als „Enormous Theorem“ bekannte Satz zur Klassifikation endlicher einfacher Gruppen.

Ab Mitte des 20. Jahrhunderts haben Hunderte von Mathematikern an dieser Forschung teilgenommen. 1983 erklärte der Mathematiker Daniel Gorenstein, dass die Klassifizierungsarbeit abgeschlossen sei, doch danach stellte sich heraus, dass noch Teile fehlten. Erst 2004 füllten Mathematiker eine entscheidende Lücke mit einem 1221 Seiten langen Beweis.

Am 26. Oktober kündigte das KI-Mathematikunternehmen Axiom Math an, dass Dutzende von KI-Agenten, die von menschlichen Mathematikern und Ingenieuren organisiert wurden, die Lean-Formalisierung dieses riesigen Theorems innerhalb von 24 Tagen abgeschlossen haben, wobei etwa 43,1 Millionen Zeilen Code und 2,05 Millionen formale Aussagen erzeugt wurden – der erste rechnergeprüfte Beweis, der den gesamten Klassifikationssatz abdeckt.

Die mathematischen Schlussfolgerungen, die ursprünglich in mehr als 500 Arbeiten verteilt waren, sind nun in ein formalisiertes System organisiert, das schrittweise überprüft werden kann. Noch überraschender ist, dass die Agenten in diesem Prozess nicht nur Fehler in historischen Arbeiten fanden, sondern auch an der Konstruktion eines neuen Ergebnisses der Gruppentheorie mitgewirkt haben.

Das von Axiom veröffentlichte formalisierte Projekt zum Satz der Klassifikation endlicher einfacher Gruppen enthält etwa 43,1 Millionen Zeilen Lean-Code, 2,05 Millionen Aussagen, 100 Meilensteine und bezieht sich auf 715 Referenzliteraturquellen. Bildquelle: Offizielle Website von Axiom Math.

Wofür hat die Mathematikgemeinschaft jahrzehntelang Beweise erarbeitet?

Um die Schwierigkeit dieser Arbeit zu verstehen, muss man mit dem Begriff der „Symmetrie“ beginnen.

Ein quadratisches Blatt Papier deckt sich nach einer Drehung um 90 Grad vollständig mit seiner ursprünglichen Form; das Gleiche gilt für Drehungen um 180 und 270 Grad. Mathematiker bezeichnen die Struktur, die durch diese Drehoperationen und ihre Kombinationen gebildet wird, als „Gruppe“. Von geometrischen Figuren bis zur Teilchenphysik bietet die Gruppentheorie eine universelle Sprache zur Untersuchung von Symmetrien.

Komplexe endliche Gruppen können in gewissem Sinne in grundlegendere Teile zerlegt werden. Genau wie Ganzzahlen in Primfaktoren zerlegt werden können, werden diese nicht weiter zerlegbaren „Elementarteilchen“ als endliche einfache Gruppen bezeichnet.

Der Satz zur Klassifikation endlicher einfacher Gruppen beantwortet eine scheinbar einfache Frage: Welche all diese Elementarteilchen gibt es genau?

Die endgültige Liste umfasst zyklische Gruppen von Primzahlordnung, alternierende Gruppen, 16 unendliche Serien von einfachen Gruppen vom Lie-Typ sowie 26 spezielle „sporadische einfache Gruppen“. Die größte davon, die „Monster Group“, verfügt über etwa 8×10^53 Elemente. Allein der Beweis ihrer Existenz war einst eine große Errungenschaft der Mathematik.

Schematische Darstellung der Beziehungen zwischen einigen „sporadischen einfachen Gruppen“. Das M an der Spitze steht für die größte sporadische einfache Gruppe, die „Monster Group“, andere Knoten repräsentieren verschiedene sporadische einfache Gruppen.

Das Auffinden dieser Gruppen ist nur die Hälfte der Arbeit. Die eigentliche Schwierigkeit liegt im Beweis: Es kann keine 27. sporadische einfache Gruppe geben, und es existieren keine unentdeckten neuen Typen außer den in der Liste aufgeführten.

1963 bewiesen Walter Feit und John Thompson in einer 255-seitigen Arbeit, dass alle nicht-kommutativen endlichen einfachen Gruppen eine gerade Ordnung haben, was den Durchbruch für die nachfolgende Klassifizierung eröffnete. 1972 stellte Gorenstein einen 16-stufigen Forschungsplan vor; 1983 erklärte er die Klassifizierung für abgeschlossen. Die verbliebene Lücke im Beweis für dünne Gruppen wurde erst 2004 von Michael Aschbacher und Stephen Smith geschlossen, 2008 folgten weitere Korrekturen.

Der riesige Beweis gleicht einem über Jahrzehnte gespannten Beziehungsnetz: Der Satz einer Arbeit zitiert den eines anderen Werks, das wiederum von früheren Lemmata abhängt. Viele Schritte lassen Bedingungen aus, die die Autoren für offensichtlich hielten. Selbst wenn jede Arbeit für sich betrachtet plausibel erscheint, ist es für eine einzelne Person fast unmöglich, jede Verbindung des gesamten Systems zu überprüfen.

Das Ziel von Axiom bei diesem Projekt ist es, all diese Verbindungen in computerüberprüfbare Beweise umzuwandeln.

24-tägiges Agent-Projekt, das fast von einem „korrekten Beweis“ zum Erliegen gebracht wurde

Dabei wird nicht ein großes Sprachmodell 15.000 Seiten lesen und dann auf einmal mehrere zehn Millionen Zeilen Code ausgeben.

Am 1. Oktober richtete Axiom einen speziellen Slack-Kanal ein und erstellte anhand der vorhandenen Lean-Bibliotheken und mathematischen Literatur einen Beweisplan mit 108 Meilensteinen und etwa 380 konkreten Aufgaben. Am 2. Oktober begannen die ersten Agenten, Aufgaben über GitHub Issues zu übernehmen.

Einige Agenten sind für die Zerlegung von Sätzen zuständig, andere suchen nach vorhandenen Ergebnissen, wieder andere generieren Lean-Beweise, und weitere prüfen Aussagen und integrieren Code. Wenn ein noch nicht abgeschlossener vorausgehender Satz ansteht, können die Agenten die Aufgabe an andere Agenten weitergeben. Menschliche Mathematiker lösen kritische Hindernisse, Ingenieure koordinieren die dauerhaft arbeitenden Systeme.

Diese Agenten werden von dem selbstentwickelten mathematischen Beweissystem AxiomProver von Axiom koordiniert. Das Projekt verwendet eine ständig angepasste Kombination mehrerer Modelle, die genaue Liste der zugrundeliegenden Modelle wird nicht veröffentlicht. Im Vergleich zur Durchführung der Schlussfolgerung durch ein einzelnes Modell legt dieses System mehr Wert auf Aufgabenzerlegung, Beweiserstellung und kollaborative Überprüfung zwischen verschiedenen Agenten.

Treemap des Formalisierungsprojekts zum Satz der Klassifikation endlicher einfacher Gruppen von Axiom, das den Umfang von Lean-Aussagen und Code in verschiedenen mathematischen Modulen darstellt. Bildquelle: Axiom Math.

Kurz nach Projektbeginn trat ein schwieriges Problem auf: Ein Agent kann zwar eine mathematische Aussage beweisen, aber nicht unbedingt genau die, die das Projekt wirklich benötigt.

Zum Beispiel sollte ursprünglich bewiesen werden, dass eine Brücke schwere Lastkraftwagen sicher passieren lassen kann. Der Agent fügte aber zunächst eine Bedingung hinzu: „Unter der Annahme, dass die Brückenpfeiler ausreichend stabil sind“. Mit dieser Voraussetzung bewies er problemlos, dass der LKW passieren kann, selbst Lean akzeptierte die gesamte Herleitung.

Aber das Problem ist: Ob die Pfeiler tatsächlich ausreichend stabil sind, wurde überhaupt nicht bewiesen.

Ähnliche Probleme traten in der frühen Projektphase wiederholt auf. Einige scheinbar abgeschlossene mathematische Aufgaben führten unbemerkt noch unbewiesene Voraussetzungen ein. Axiom musste Zehntausende von Codezeilen löschen, die auf diesen Annahmen beruhten, und die Arbeit neu organisieren.

Mit dem Wachstum der Codebasis konnte die Überprüfungsgeschwindigkeit von Lean die Produktivität der Agenten nicht mehr mithalten. Die Änderung eines grundlegenden Satzes kann dazu führen, dass aller davon abhängige Code neu überprüft werden muss. Die Ingenieure führten dafür gemeinsam genutzte Build-Caches und parallele Überprüfungsmechanismen ein, damit verschiedene Agenten bereits bestätigte Ergebnisse möglichst wiederverwenden können.

Am 10. Oktober gab es eine gute Nachricht im Slack-Kanal des Teams: „WE PROVED MONSTER IS SIMPLE.“ Die Agenten hatten die Formalisierung der Einfachheit der Monster-Gruppe abgeschlossen und auch ihre Existenz über die Griess-Algebra formalisiert.

Aber drei Tage später verlangsamte sich der Projektfortschritt plötzlich. Am 13. Oktober, obwohl Dutzende von Agenten ständig Code generierten, absolvierte das Team den ganzen Tag nur eine phasenweise Beweisaufgabe.

Das Problem lag in der Aufgabenzerlegung. Die verbleibenden mathematischen Probleme waren zu komplex, hinter einer großen Aufgabe verbargen sich noch viele ungelöste Kleinprobleme. Obwohl die Agenten ständig neue Beweise schreiben konnten, fällt es ihnen schwer zu beurteilen, wie viele kritische Schritte sie bereits gelöst haben und wie weit sie vom endgültigen Ziel entfernt sind.

Axiom musste die Strategie neu anpassen, komplexe Beweise in kleinere, klarere Aufgaben zerlegen und die Agenten auffordern zu erläutern, wie diese kleinen Beweise schrittweise kombiniert werden, um schließlich die ursprünglich benötigte Schlussfolgerung zu erhalten.

Die KI deckt einen 40 Jahre alten Fehler auf und ergänzt einen neuen Beweis

Als die Beweiserstellung in die Tiefen der historischen Literatur vordrang, stellten die Agenten etwas fest, das problematischer war als die Aufgabenplanung: Auch die ursprünglichen mathematischen Arbeiten können Fehler enthalten.

Menschliche Mathematiker lassen oft vertraute Schlussfolgerungen aus, aber Lean verlangt die explizite Angabe jeder Voraussetzung. Nach Statistiken von Axiom gab es im Formalisierungsprozess 34 bemerkenswerte Abweichungen in der Literatur, die bearbeitet werden mussten – darunter Schreibfehler, fehlende Bedingungen und wesentliche Probleme, die neu hergeleitet werden mussten.

Ein Beispiel findet sich in dem Werk von Aschbacher und Smith über „quasidünne Gruppen“. Ein Lemma im Originaltext behauptet, dass zwei Größen gleich sind, aber der Agent fand mit der Gruppe SL₂(5) ein Gegenbeispiel: Eine Größe ist 1, während die Gleichung verlangt, dass sie 2 ist. Wenn man die Gleichung in eine Ungleichung ändert, kann das Lemma korrigiert werden, aber die nachfolgende Schlussfolgerung stützte sich auf das Gleichheitszeichen. Das Team musste den Geltungsbereich einer vorhergehenden Argumentation erweitern und die betroffenen Fälle neu bearbeiten.

Ein größeres Hindernis stammt aus der Forschung von John Walter aus dem Jahr 1986 zum „Unbalanced Group Theorem (UGT)“.

Das UGT ist ein wichtiges Werkzeug für die Klassifikation endlicher einfacher Gruppen. Es hilft Mathematikern, anhand einer bestimmten lokalen Struktur innerhalb einer Gruppe zu schließen, zu welchem Typ die gesamte Gruppe gehören kann. Eine zentrale Schlussfolgerung von Walter ging implizit davon aus, dass bei einer bestimmten Operation an einer bestimmten Gruppenfamilie die zugehörige einfache Gruppe immer noch zur ursprünglichen Gruppenfamilie gehört.

Die Agenten fanden ein Gegenbeispiel: Ausgehend von PSL₂(49) betrachtet man die durch seine Automorphismen über endliche Körper induzierte Involution, die einfache Gruppenkomponente des zugehörigen Zentralisators ergibt PSL₂(7). Aber diese gehört genau nicht zu der von Walter festgelegten Gruppenfamilie, die ursprüngliche Aussage über die Abgeschlossenheit kann nicht aufrechterhalten werden.

Dadurch wird die Schlussfolgerung des UGT nicht widerlegt, aber es bedeutet, dass bei der Fortführung dieser Beweisroute ein Schritt auf eine andere Grundlage gestellt werden muss.

Axiom konsultierte dazu die Gruppentheorie-Experten Richard Lyons und Ronald Solomon. Die von Solomon 1976 vorgeschlagene Theorie maximaler 2-Komponenten lieferte den entscheidenden Ansatz für die neue Route.

Anschließend konstruierten und formalisierten die Agenten ein neues Ergebnis der Gruppentheorie mit dem Namen „Preservation of simple tops“, das beweist, dass unter den benötigten Bedingungen die zugehörige einfache Gruppenstruktur bei dem Vergleich bestimmter Untergruppen erhalten bleibt. Dieses Ergebnis wurde in die 35-seitige Arbeit „The Unbalanced Group Theorem“ als Satz 2.3 aufgenommen und mit anderen vorhandenen Ergebnissen kombiniert, um den für die Klassifikation benötigten Beweis des UGT abzuschließen.

Interessanterweise fanden die Mathematiker von Axiom nach Abschluss der Formalisierung einen kürzeren Pfad in der ursprünglichen Beweismethode, mit dem die Zielschlussfolgerung auch ohne Verwendung dieses neuen Satzes erzielt werden kann. Trotzdem wurden der neue Satz und sein vollständiger Beweis beibehalten und stellen ein zusätzliches mathematisches Ergebnis dieses Projekts dar.

Die vom Axiom-Team abgeschlossene Forschung zum Unbalanced Group Theorem, bei der Satz 2.3 „Preservation of simple tops“ das neue mathemat