Axiom Math verhindert KI-Müll in der Mathematik

Das Unternehmen Axiom Math hat die vollständige maschinelle Überprüfung eines der größten Werke der modernen Mathematik abgeschlossen. Wie Axiom am Mittwoch mitteilte, wurde das Stacks Project in die formale Beweissprache Lean überführt. Die Umsetzung umfasst nach Angaben des Unternehmens rund 7.654 Seiten und etwa 16 Millionen Zeilen maschinell geprüften Codes. Das 2005 vom Mathematiker Johan de Jong initiierte Stacks Project ist eine offene Referenzsammlung für Algebra, Geometrie und Zahlentheorie und wird seit Jahren von einem großen Kreis von Fachleuten fortgeschrieben. Axiom nutzt für dieses Vorhaben eigene KI-Agenten, die anfangs von Mathematikexperten angeleitet und später in Teilen eigenständig weitertrainiert wurden. Die 25-jährige Gründerin und Geschäftsführerin Carina Hong hatte im März 2025 ein Doktorandenprogramm für Mathematik an der Stanford University verlassen, um das Unternehmen zu gründen. Im selben Monat schloss Axiom eine von Menlo Ventures geführte Finanzierungsrunde der Kategorie A über 200 Millionen US-Dollar ab; die Bewertung liegt den Angaben zufolge bei 1,6 Milliarden US-Dollar. Im Kern steht die formale Verifikation: Mathematische Beweise werden so in Code überführt, dass ein Beweisassistent sie Zeile für Zeile auf logische Konsistenz prüfen kann. Bei einem eng vernetzten Werk wie dem Stacks Project reicht die isolierte Prüfung einzelner Sätze nicht aus. Jede Definition und jeder Lehrsatz muss in das bestehende Gefüge passen, damit keine Widersprüche entstehen. Genau darin lag die größte technische Schwierigkeit. Die KI-Agenten arbeiteten weitgehend parallel, wählten Teilaufgaben selbst und bekamen nur eine lockere Hierarchie vorgegeben. Für die mathematische Forschung schafft die vollständige Formalisierung eine neue Grundlage, insbesondere im Bereich der algebraischen Geometrie, der in Lean bislang stark unterrepräsentiert war. Forscher können künftig auf bereits geprüfte Ergebnisse aufbauen, statt Beweise jedes Mal vollständig neu zu strukturieren. Der Träger der Fields-Medaille, Terence Tao, bringt diesen Ansatz auf den Punkt: Aus formalisierten Beweisen erwachsen weitere formalisierte Beweise. Axiom sieht die Bedeutung jedoch über die reine Mathematik hinaus. Wenn KI-Systeme künftig zunehmend Software erzeugen, steigen auch die Anforderungen an Sicherheit, Verlässlichkeit und Struktur. Die formalisierte Mathematikbibliothek soll als vertrauenswürdiger Unterbau dienen, auf dem KI-Agenten neue Infrastruktur, Werkzeuge und Anwendungen entwickeln können. Hong argumentiert, dass ein schnelles Wachstum ohne solide, wiederverwendbare Grundlagen leicht zu fehlerhaften und schwer korrigierbaren Systemen führt. Damit positioniert sich Axiom als Anbieter formaler Infrastruktur für die nächste Generation autonomer KI.