Axiom Math teilte am 26. Oktober mit, dass das Unternehmen nach eigener Darstellung den ersten vollständigen computergestützten Beweis der Klassifikation endlicher einfacher Gruppen in Lean abgeschlossen hat.
In der Ankündigung von Axiom Math erklärt das Unternehmen, das Projekt habe den CFSG-Beweis der ersten Generation formalisiert und in Schritte zerlegt, die Lean maschinell prüfen kann. Axiom gibt außerdem an, dass der Aufwand 24 Tage dauerte, Dutzende KI-Agenten einsetzte und rund 43,1 Millionen Zeilen Lean-Code erzeugte.
Die Formalisierung reproduzierte nicht nur die Fachliteratur. Axiom zufolge deckte sie 34 bemerkenswerte Abweichungen von veröffentlichten Argumentationen auf und markierte ein Problem in einem veröffentlichten Beweisweg zum Unbalanced Group Theorem. Das Unternehmen plant nach eigenen Angaben, eine ausführlichere Errata-Liste für Mathematiker zu veröffentlichen.
Für Builder ist weniger der zentrale Satz als das Betriebsmodell interessant: Ein Problem mit vielen Abhängigkeiten wird in nachverfolgbare Teilprobleme zerlegt, während eine Prüfinstanz eingebunden bleibt, damit plausibel wirkende Ergebnisse nicht mit einem abgeschlossenen Resultat verwechselt werden. Dieses Muster ist überall relevant, wo Agenten Abdeckung und Korrektheit nachweisen müssen, statt nur vollständig wirkenden Text zu erzeugen.