Wie passen die Teile eines Beweises zusammen, der über Hunderte Veröffentlichungen verteilt ist? Axiom Math beschreibt dazu am 26. Oktober eine Lean-Formalisierung der Klassifikation endlicher einfacher Gruppen. Von Forschern angeleitete KI-Agenten übertrugen die mathematischen Argumente in eine computerprüfbare Struktur.
Grundbausteine endlicher Symmetrien
Gruppen beschreiben, wie Transformationen zusammenwirken. Die Drehungen, nach denen ein Würfel gleich aussieht, geben ein anschauliches Beispiel. Die Klassifikation benennt die Grundbausteine endlicher Gruppen. Der menschliche Beweis umfasst ungefähr 15.000 Seiten in mehr als 500 Artikeln von etwa 100 Mathematikern.
Warum die Formalisierung eine eigene Aufgabe ist
In Lean müssen Definitionen, Voraussetzungen und Schlussfolgerungen präzise zusammenpassen. Ein bekanntes Ergebnis kann nicht einfach verwendet werden, wenn seine Annahmen an der benötigten Stelle fehlen. Literatur aus mehreren Jahrzehnten in einer gemeinsamen Struktur zu verbinden ist deshalb mehr als eine Übersetzung von Text in Code.
Axiom teilte das Vorhaben in 108 Meilensteine und etwa 380 kleinere Aufgaben. Agenten bearbeiteten Voraussetzungen und Beweise in einem gemeinsamen Repository. Mathematiker untersuchten Hindernisse; Ingenieure organisierten die wachsende Prüflast. Nach Angaben des Unternehmens entstanden in 24 Tagen etwa 43,1 Millionen Zeilen Lean.
Die Verbindungen müssen ebenfalls stimmen
Axiom nennt 34 bedeutsame Abweichungen von der veröffentlichten Literatur, die geklärt werden mussten. Fehlende Annahmen oder unpassende Abhängigkeiten können verhindern, dass ein Teilergebnis den Gesamtbeweis trägt. Die 24 Tage beziehen sich auf diese Formalisierung, nicht auf die jahrzehntelange mathematische Entstehung des Theorems.
Ivys Einordnung
Was sagt uns dieses Ergebnis? Ein funktionierender Baustein hilft nur dann, wenn er genau die Aussage liefert, die an dieser Stelle gebraucht wird. Nachvollziehbare Abhängigkeiten sind deshalb ebenso interessant wie die Codemenge. Formalisierung kann sichtbar machen, wie mathematisches Wissen im Detail zusammenhängt.
