Chinas KI-Startup überführt Stacks in verifizierbaren Code

Das 2025 gegründete KI-Mathematikunternehmen Axiom Math hat das seit 2005 von Johan de Jong an der Columbia University aufgebaute Referenzwerk Stacks Project in maschinell prüfbaren Lean-Code überführt. Das Projekt dokumentiert mit über 650 Mitwirkenden mehr als 20.000 Definitionen, Lemmas und Theoreme der algebraischen Geometrie auf 116 Kapiteln und mehr als 7.600 Seiten. Am 4. November veröffentlichte Axiom eine Codebasis mit rund 15,75 Millionen Zeilen, die alle formalisierbaren Einträge abdeckt und an das von der Lean Community gepflegte Mathlib anknüpft. Axiom nutzt einen zweistufigen Aufbau: Der Kern mit geprüften, Mathlib-konformen Beweisen und eine Frontier-Ebene mit KI-generierten, noch nicht vollständig begutachteten Teilen. Jede Behauptung wird vom Lean-Kernel überprüft. Das Team setzt KI-Agenten für Architektur, Definitionen und Beweise ein, während vier Mathematikerinnen und Mathematiker die Einpflegung von Beiträgen prüfen. Dabei entdeckten die Agenten demnach Dutzende lokale Probleme im Originaltext und lieferten Gegenbeispiele. Bereits in Mathlib enthaltene oder für Lean ungeeignete Einträge sind markiert; Beispiele, Übungen und Kommentare bleiben offene Beiträge. Die Arbeit folgt früheren Axiom-Projekten zur Formalisierung des Primabstand-Theorems über die Lücke 246 und der Klassifikation endlicher einfacher Gruppen. Im Gegensatz zu diesen einmaligen Meilensteinen zielt das Stacks-Projekt auf eine dauerhafte, erweiterbare Wissensbasis. Der Schritt zeigt, dass KI-gestützte Formalisierung von isolierten Großbeweisen zu fortlaufender, kollaborativ nutzbarer Infrastruktur wechselt. Zugleich bleibt die menschliche Prüfung das Nadelöhr. Die Lean-Community fordert klare Designregeln, öffentliche Reviews, Vermeidung von Duplikaten und nachvollziehbare Bezüge zu Originalquellen. Für die Forschung könnte eine verifizierte Mathematikdatenbank doppelten Nutzen haben: Mathematikerinnen und Mathematiker können Beweise beim Entstehen prüfen, während KI-Agenten auf geprüfte Aussagen zurückgreifen, statt Beweise von Grund auf neu zu erzeugen. Axiom plant, die formalisierten Teile in Mathlib einzubringen, und sieht in verifizierter Mathematik einen Schlüssel für Code, Kryptografie und quantitative Finanzanalyse. Kurzfristig wird eine vollständige Übernahme in Mathlib jedoch als unwahrscheinlich angesehen, weil nicht nur formale Korrektheit, sondern auch die Treue zur intendierten mathematischen Bedeutung menschlicher Kontrolle bedarf.