Axiom Math verifiziert das Stacks Project gegen KI-Schrott

So funktioniert die Verifikation

Mathematiker schreiben einen Beweis als Code in der Programmiersprache Lean um, und ein Beweisassistent prüft ihn Zeile für Zeile. Ingenieure nutzen dasselbe Prinzip, die formale Verifikation, um Chipdesigns zu bestätigen. Forscher in Frankreich fanden damit Fehler in einer Software zur Berechnung von Familienleistungen.

Stacks war eine harte Probe, weil Sätze und Definitionen aufeinander aufbauen, ähnlich wie in einem Stammbaum. Der Columbia-Mathematiker Johan de Jong startete das Open-Source-Projekt 2005. Es reicht von Algebra auf Universitätsniveau bis zu algebraischer Geometrie und Zahlentheorie. „Große und zugleich empfindliche Dinge passen im Leben nicht zusammen“, sagte CEO Carina Hong.

Axiom gab seinen Agenten eine lose Hierarchie und ließ sie parallel arbeiten, wobei sie sich Aufgaben selbst suchten. Zudem trainierte das Unternehmen eigene Mathematikmodelle. Laut Ashvin Swaminathan klaffte in der formalisierten Mathematik ein „riesiges schwarzes Loch“ bei der algebraischen Geometrie, auf dem Forscher mit Lean nun aufbauen können.

Mehr als Mathematik

Axiom sieht jedes verifizierte Ergebnis als Baustein. Terence Tao formulierte es so: „Je mehr formalisierte Beweise man hat, desto mehr kann man erstellen.“ Zur Zielgruppe zählen auch Entwickler, die kaum garantieren können, dass Code frei von Fehlern und Sicherheitslücken ist, ein Problem, das mit KI-generiertem Code wächst.

Hong, 25, brach ein Mathematik-Promotionsprogramm in Stanford ab und gründete Axiom im März 2025. Im März sammelte die Firma 200 Millionen Dollar in einer von Menlo Ventures geführten Series A ein. Sie fordert alle Coding-Unternehmen offen heraus, Formalisierung in diesem Maßstab anzugehen.