Axiom zufolge haben KI-Agenten die Klassifikation der endlichen einfachen Gruppen in Lean formalisiert

Axiom, ein KI-Mathematikunternehmen, gab auf X eine vollständige automatische Formalisierung der Klassifikation der endlichen einfachen Gruppen in Lean bekannt – ein Ergebnis, das es als „periodisches System der Symmetrie“ bezeichnet. Den ursprünglichen Beweis beschreibt das Unternehmen als rund 15.000 Seiten lang und von über 100 Mathematikerinnen und Mathematikern über mehrere Generationen hinweg verfasst. Es bezeichnet ihn als den größten mathematischen Beweis der Geschichte, der per Computer verifiziert wurde.

Laut Axioms Open-Source-Repository erzeugten Schwärme von KI-Agenten innerhalb von 24 Tagen rund 43,1 Millionen Zeilen Lean-Code. Dabei deckten sie 715 Fachartikel und Bücher ab und markierten 34 Abweichungen von der veröffentlichten Darstellung. Ein Beitrag des KI-Nachrichtenkontos TestingCatalog ergänzt, dass die Agenten die Arbeit wie Softwareteams aufteilten und schneller Code schrieben, als Lean ihn überprüfen konnte.

Diese Zahlen stammen von Axiom selbst; eine unabhängige Prüfung der Formalisierung gehört nicht zur Ankündigung. Bis zum 28. Oktober hatte der Beitrag auf X rund 6.200 Likes erhalten.