15.000 Seiten Mathematik in 24 Tagen: KI-Agenten prüfen den „enormen Satz“ per Computer
Das Start-up Axiom hat nach eigenen Angaben den Beweis der Klassifikation endlicher einfacher Gruppen mit Schwärmen von KI-Agenten komplett in Lean formalisiert. Unabhängig nachgebaut ist das noch nicht.
Grafik: TERRA WORLD NEWS (eigene Darstellung nach den genannten Quellen)
Die Klassifikation der endlichen einfachen Gruppen gilt als längster Beweis der Mathematik: rund 15.000 Seiten in mehr als 500 Fachartikeln von etwa 100 Mathematikern über Jahrzehnte. Das Start-up Axiom Math meldet nun, den gesamten Beweis in die Sprache des Beweisprüfers Lean übertragen zu haben, in dem der Computer jeden logischen Schritt kontrolliert. Dutzende KI-Agenten arbeiteten dafür in Schwärmen 24 Tage lang; heraus kamen rund 43,1 Millionen Zeilen Lean-Code.
Dabei stießen die Agenten laut Axiom auf 34 nennenswerte Abweichungen von der veröffentlichten Literatur; die wichtigen davon untersuchten menschliche Mathematiker. Beraten ließ sich Axiom von den Gruppentheoretikern Richard Lyons und Ronald Solomon. Menschen prüften zudem, ob die formalen Aussagen tatsächlich den gemeinten Satz ausdrücken. Den Begriff „enormer Satz“ prägte einst der Mathematiker Daniel Gorenstein.
Dass es sich um den ersten vollständig computergeprüften Beweis handelt, ist bislang eine Angabe von Axiom selbst. Auf die Frage, ob jemand außerhalb der Firma den Beweis schon nachgebaut und geprüft habe, antwortete Firmenchefin Carina Hong laut RuntimeWire: „Noch nicht.“ Axiom veröffentliche die Build-Dateien, um externe Gruppen dazu zu ermutigen.