KI-Agenten prüfen riesige Mathe-Bibliothek: Axiom verifiziert das Stacks Project

Worum es geht

Das US-Start-up Axiom Math hat am Mittwoch bekanntgegeben, das sogenannte Stacks Project formal verifiziert zu haben – also jeden Satz und jede Definition einer der umfangreichsten Mathematik-Sammlungen, die Menschen je geschrieben haben, von einem Computer auf logische Korrektheit prüfen zu lassen. Die Arbeit erledigte eine Flotte von KI-Agenten, also KI-Programmen, die selbstständig Teilaufgaben übernehmen und abarbeiten. Sie übersetzten rund 7.654 Seiten in etwa 16 Millionen Zeilen Code.

Axiom, laut TechCrunch mit rund 1,6 Milliarden Dollar bewertet, verkauft das Projekt als Gegenmittel gegen „AI Slop“ – so nennt man minderwertige, massenhaft produzierte KI-Inhalte. Hintergrund: KI-Systeme liefern inzwischen fast wöchentlich angebliche Lösungen mathematischer Probleme. TechCrunch erwähnt, dass OpenAI im vergangenen Monat 719 Manuskripte mit behaupteten Lösungen zu einigen der schwierigsten Probleme des Fachs veröffentlicht habe. Wer soll das alles prüfen?

Was das Stacks Project ist

Das Stacks Project wurde 2005 vom Mathematiker Johan de Jong an der Columbia University als frei zugängliches Nachschlagewerk gestartet. Seitdem haben viele Mathematiker beigetragen: von Algebra auf Studienanfänger-Niveau bis zu den fortgeschrittensten Ideen in Algebra, Geometrie und Zahlentheorie. Der Columbia-Mathematiker Peter Woit sagte laut TechCrunch, es gebe „nichts wirklich Vergleichbares“, und verglich es mit den berühmten Bourbaki-Büchern – einer Reihe, mit der eine Gruppe französischer Mathematiker im 20. Jahrhundert die Mathematik von Grund auf neu aufgebaut hat.

Die besondere Schwierigkeit: Die Inhalte sind eng verflochten. Wie in einem Stammbaum baut fast jedes Ergebnis auf früheren Definitionen und Sätzen auf. Bei der Übersetzung musste jede dieser Verbindungen über 16 Millionen Codezeilen hinweg erhalten bleiben.

„Dinge, die groß sind, und Dinge, die empfindlich sind, passen im Leben einfach nicht zusammen“, sagte Axiom-Chefin Carina Hong zu TechCrunch. „Man will, dass die Sätze konsistent und nicht paradox sind. Man will, dass die Definitionen sich nicht gegenseitig bekämpfen.“

Wie formale Verifikation funktioniert

Beim Formalisieren wird ein mathematischer Beweis in die Programmiersprache Lean übersetzt. Ein Beweisassistent – ein Programm, das wie ein extrem pedantischer Korrektor jeden logischen Schritt nachrechnet – prüft dann Zeile für Zeile. Besteht der Code die Prüfung, können Mathematiker sicher sein, dass der Beweis logisch stimmt. Dasselbe Prinzip, formale Verifikation genannt, nutzen Ingenieure, um Chipdesigns abzusichern; in Frankreich hat man damit laut TechCrunch sogar Fehler in Software zur Berechnung von Familienleistungen gefunden.

Axiom war selbst unsicher, ob das klappt. „Wir wussten nicht, ob Vibe Coding die Schönheit von Stacks bewahren kann“, so Hong – Vibe Coding meint Programmieren, bei dem man eine KI weitgehend selbstständig Code schreiben lässt.

Agenten-Schwarm mit lockerer Hierarchie

Das Team gab den Agenten nur eine grobe Struktur vor und ließ sie parallel arbeiten. „Wir haben eine Hierarchie vorgegeben, aber keine vollständige, die jedem einzelnen Agenten diktiert hätte, was er tun soll“, erklärt Ashvin Swaminathan aus dem technischen Team. „Die Agenten haben sich selbst Aufgaben gesucht und erkannt, woran sie parallel arbeiten können.“

Außerdem trainierte Axiom eigene, auf Mathematik spezialisierte Modelle – laut Hong ein Schritt, den die meisten anderen Verifikations-Start-ups nicht gegangen seien. Anfangs habe ein hauseigener Lean-Experte den Agenten ein menschliches Gespür für guten Stil vermittelt; inzwischen hätten die Agenten dieses Gespür selbst entwickelt (Herstellerangabe).

Das Ergebnis schließt laut Swaminathan eine große Lücke: „Wenn man sich ansieht, was in der Mathematik formalisiert wurde, gibt es dieses riesige schwarze Loch. Und das betrifft die algebraische Geometrie.“ Wer neue Arbeiten in diesem Gebiet mit Lean prüfen wollte, hatte bisher kaum eine Grundlage. „Jetzt schon.“

Vorgeschichte: das „enorme Theorem“ in 24 Tagen

Die Stacks-Meldung folgt nur wenige Tage auf ein noch spektakuläreres Projekt. Am 27. Oktober veröffentlichte Axiom laut Unite.AI den nach eigenen Angaben ersten vollständig computergeprüften Beweis der Klassifikation der endlichen einfachen Gruppen. Diese beschreibt die Grundbausteine aller endlichen Gruppen; der Originalbeweis verteilt sich auf rund 15.000 Seiten in über 500 Artikeln von etwa 100 Mathematikern und trägt den Spitznamen „das enorme Theorem“.

Die Arbeit dauerte laut Axiom 24 Tage: Ab dem 2. Oktober arbeiteten Schwärme aus Dutzenden Agenten 108 Meilensteine und rund 380 kleinere Aufgaben ab, koordiniert über GitHub-Issues und Slack. Es lief nicht reibungslos: Agenten hatten Voraussetzungen einfach angenommen statt bewiesen, das Team löschte zehntausende Zeilen und plante neu. Auch das Nachprüfen durch Lean wurde zum Engpass, weil die Agenten schneller Beweise produzierten, als Lean sie checken konnte.

Besonders interessant: Beim Übersetzen stießen die Agenten auf 34 nennenswerte Abweichungen in der veröffentlichten Literatur – meist Tippfehler, falsche Tabellen oder vergessene Voraussetzungen. In einem Lemma von Aschbacher und Smith fanden sie ein Gegenbeispiel mit der Gruppe SL₂(5). Beim „Unbalanced Group Theorem“ entdeckten sie Gegenbeispiele zu einer Behauptung in John Walters Arbeit von 1986; die Lücke wurde mit einem nach Axiom-Angaben neuen, von ihrem System AxiomProver bewiesenen Satz geschlossen. Das Theorem selbst wurde dadurch nicht widerlegt. Der Code steht unter Apache-2.0-Lizenz auf GitHub; die Fehlerliste will Axiom mit Gruppentheoretikern wie Richard Lyons und Ronald Solomon aufarbeiten.

Das Unternehmen und seine Wette

Carina Hong, 25, brach ein Mathe-Promotionsstudium in Stanford ab und gründete Axiom im März 2025. Im März dieses Jahres sammelte die Firma 200 Millionen Dollar in einer Series A unter Führung von Menlo Ventures ein. Die eigentliche Zielgruppe sind nicht nur Mathematiker: Axiom setzt darauf, dass Software, die zunehmend von KI-Agenten geschrieben wird, künftig auf geprüften Grundlagen stehen muss, um Fehler und Sicherheitslücken auszuschließen.

„Mathematik ist das Gebiet, in dem man anfängt, solche Dinge zu bauen, und das ist eine übertragbare Fähigkeit“, sagt Swaminathan. „Unsere Lean-Formalisierung ist jetzt das Substrat, auf dem Agenten aufbauen können.“ Fields-Medaillen-Träger Terence Tao hat das Prinzip so zusammengefasst: „Je mehr formalisierte Beweise man hat, desto mehr formalisierte Beweise kann man erstellen.“ Hong gibt sich selbstbewusst: „Ich fordere alle Coding-Firmen offen heraus, an Formalisierung in diesem Maßstab zu arbeiten.“

Einordnung

Formale Verifikation ist eine der wenigen Methoden, mit denen sich KI-Ergebnisse wirklich zuverlässig prüfen lassen – nicht durch Vertrauen, sondern durch mechanisches Nachrechnen. Dass Agenten in Wochen Projekte stemmen, für die menschliche Teams Jahre bräuchten, ist ein deutlicher Fortschritt; Mathematiker in der algebraischen Geometrie bekommen ein nutzbares Fundament.

Einschränkungen bleiben: Die Angaben stammen bislang vom Unternehmen selbst, eine unabhängige Begutachtung der 16 Millionen Zeilen durch die Fachgemeinschaft steht aus. Ob der Stacks-Code wie der Gruppen-Beweis offen verfügbar ist, geht aus den Quellen nicht hervor. Formale Verifikation garantiert außerdem nur, dass die Beweise zu den formalisierten Aussagen passen – ob diese Aussagen genau das treffen, was die Originalautoren meinten, ist eine eigene Frage. Und ob der Ansatz sich, wie Axiom hofft, auf allgemeine Softwareentwicklung übertragen lässt, ist bislang eine Wette, kein Beleg.