AI-Startup verifiziert längsten Beweis: 43 Mio. Codezeilen
Das US-amerikanische KI-Mathematikunternehmen Axiom hat den vollständigen formalen Beweis des Klassifikationssatzes der endlichen einfachen Gruppen in der Theorembeweiser-Sprache Lean abgeschlossen. Der am 27. Oktober veröffentlichte und auf GitHub unter dem Namen AxiomMath/CFSG veröffentlichte Code umfasst rund 43,1 Millionen Zeilen und wurde von autonomen KI-Agenten innerhalb von 24 Tagen erstellt. Die formale Überprüfung durch den Lean-Kernel bestätigt, dass alle logischen Schritte von den Axiomen bis zum Abschluss des über 15.000 Seiten langen Beweiswerks ohne Lücken verifiziert sind. Die Klassifikation endlicher einfacher Gruppen gilt als längster Beweis der Mathematikgeschichte. Sie verbindet mehr als 500 Aufsätze von etwa 100 Mathematikern und listet alle einfachen endlichen Gruppen auf: die alternierenden Gruppen, 16 Familien von Lie-Typen und die 26 sporadischen Gruppen. Der ursprüngliche Beweis war so verzweigt, dass nur noch wenige Eingeweihte ihn vollständig überblickten. Das Projekt zeigt, wie formale Verifikation KI-generierte oder historisch gewachsene Beweise wieder überprüfbar machen kann. Unter der Leitung von Gründerin Carina Hong und Founding Mathematician Ken Ono stellte Axiom im Oktober die vollständige Lean-Formalisierung für den ersten Beweis der Klassifikation her. Die Agenten von AxiomProver zerlegten das Werk in 108 Meilensteine mit etwa 380 Teilaufgaben und nutzten vorhandene Strukturen aus dem Mathlib-Universum sowie mehr als eine Million Zeilen aus einem von Yau Shing-Tung initiierten Projekt der Tsinghua-Universität. Der Start verlief holprig: Unbelegte Prämissen führten zum Löschen zehntausender Zeilen. Nach einer Neuordnung der Meilensteine und einer verbesserten Caching-Infrastruktur beschleunigte die Überprüfung. Am 10. Oktober meldeten die Agenten den ersten Erfolg beim Nachweis, dass die Monstergruppe einfach ist. Am 26. Oktober meldete das System die formale Vollständigkeit. Der Prozess deckte auch Schwächen auf. 34 Abweichungen von der publizierten Literatur und mehrere Fehler in früheren Veröffentlichungen konnten bestätigt werden. Kritisch wurde es beim Theorem der unbalancierten Gruppen, das einen Teilfall ausschließt. Das Team dokumentierte dort eine falsche Behauptung von John Walter aus dem Jahr 1986, die zwar den Satz selbst nicht widerlegte, aber seine Beweiskette unterbrach. Axiom beriet sich mit Richard Lyons und Ronald Solomon. Die Lösung bestand in einer alternativen Route, die einen bisher fehlenden gruppen theoretischen Hilfssatz erforderte und auf der Plattform Hexagon dokumentiert ist. Diese neue Route führt zu einer kürzeren Schlussfolgerung innerhalb des ursprünglichen Rahmens. Inhaltlich liefert die Arbeit mehr als einen maschinellen Beweis. Der Lean-Code macht die gesamte Gliederung in Abhängigkeiten sichtbar und kann als Grundlage für weitere algebraische Verifikation dienen. Das Timing fällt in eine Phase, in der mathematische KI-Entwickler von Größen wie Terence Tao und Hongjie Deng in Diskussionen auf die Kluft zwischen maschinell erzeugten Beweisen und menschlichem Verständnis hinweisen. Axiom adressiert dieses Problem, indem der Beweis nicht nur ausgeführt, sondern auch durch die Community überprüft und korrigiert wird. Die Zukunft der Mathematik könnte damit auf formale Infrastruktur verlagert werden, während neue KI-Agenten die Beweise für die wachsende Zahl von Problemen produzieren, die Menschen zu lesen nicht mehr schaffen.
