# Axiom überführt das Stacks Project in maschinengeprüften Lean-Code

> Die 16 Millionen Zeilen umfassende Formalisierung macht eine wichtige Referenz zur algebraischen Geometrie laut Axiom für Beweise nutzbar, die Lean überprüft.

Oossa · 2026-11-05 · https://oossa.com/de/axiom-turns-the-stacks-project-into-machine-checked-lean-code

Axiom Math hat eine maschinengeprüfte Version des Stacks Project veröffentlicht, einer wichtigen Open-Source-Referenz zur algebraischen Geometrie. Bei der Formalisierung wurde die Mathematik des Projekts in rund 16 Millionen Zeilen Lean-Code übertragen, die ein Beweisprüfungsprogramm Schritt für Schritt überprüft. Laut Axiom können Forschende und KI-Agenten die Ergebnisse als zusammenhängende Bibliothek nutzen, um neue formale Beweise zu entwickeln.

Die Quellen nennen leicht unterschiedliche Seitenzahlen: TechCrunch spricht von rund 7.654 Seiten, Axiom von ungefähr 7.500. Der Aufbau des ursprünglichen Nachschlagewerks begann 2005 mit dem Mathematiker Johan de Jong von der Columbia University; über zwei Jahrzehnte hinweg trugen weitere Mathematiker dazu bei. Axiom formalisiert diese bereits vorhandene wissenschaftliche Arbeit – das bedeutet nicht, dass die KI-Agenten die zugrunde liegende Mathematik eigenständig entdeckt hätten.

## Warum ist eine zusammenhängende Bibliothek wichtig?

Eine Beweisbibliothek ist nicht nur deshalb nützlich, weil ihre einzelnen Sätze geprüft wurden, sondern auch, weil spätere Beweise sie samt ihren Abhängigkeiten wiederverwenden können. Axiom zufolge wurden die dauerhaften Tags des Stacks Project beibehalten, sodass sich Lean-Deklarationen den entsprechenden Stellen im Originaltext zuordnen lassen. Auf der Website des Unternehmens können Leserinnen und Leser außerdem Text und Code nebeneinander anzeigen und nachvollziehen, wie die Ergebnisse voneinander abhängen.

Das ist besonders in der algebraischen Geometrie wichtig, wo ein Beweis auf einer langen Kette von Ideen aus Bereichen wie kommutativer Algebra, Schemata, Garben und Kohomologie aufbauen kann. Vor dieser Veröffentlichung hätten Forschende deutlich weniger Lean-Infrastruktur zur Formalisierung moderner algebraischer Geometrie zur Verfügung gehabt, so Axiom. Die Bibliothek bietet ihnen einen Ausgangspunkt, statt dass sie diese Grundlagen für jedes Projekt erneut formalisieren müssen.

## Grundlage für künftige Beweise – und Software

Laut Axiom arbeiteten die Agenten parallel daran, Tausende von Sätzen zu übertragen, zu beweisen und zu integrieren. TechCrunch berichtet, das Unternehmen habe den Agenten einen groben Rahmen vorgegeben, damit sie selbst Aufgaben finden konnten. Außerdem habe Axiom eigene, auf Mathematik spezialisierte Modelle trainiert. Die fertige Bibliothek sei die größte integrierte, wiederverwendbare Sammlung formalisierter Mathematik – so beschreibt Axiom die eigene Veröffentlichung.

Dieselbe Art der Prüfung kommt unter anderem beim Chipdesign und bei der Softwareverifikation zum Einsatz. Axiom zufolge könnten wiederverwendbare, geprüfte Grundlagen KI-Agenten dabei helfen, verlässlichere Systeme zu entwickeln, wenn sie immer mehr Code schreiben. Die Veröffentlichung überprüft jedoch die Formalisierung des Stacks Project – nicht jede neue mathematische Behauptung und nicht jede Software, die ein KI-System möglicherweise erzeugt.

## Die Fakten

- Axiom datierte die Veröffentlichung auf den 4. November 2026.
- Die Lean-Formalisierung umfasst rund 16 Millionen Codezeilen.
- Johan de Jong begann 2005 mit dem Stacks Project; seitdem ist es durch Beiträge von Mathematikern gewachsen.
- Laut TechCrunch nahm Axiom im März 2026 in einer von Menlo Ventures angeführten Series A 200 Millionen Dollar auf.

## Warum es wichtig ist

Für Mathematikerinnen und Mathematiker, die in der algebraischen Geometrie arbeiten, bietet die Bibliothek geprüfte Ergebnisse, die sie wiederverwenden können, statt dieselben Grundlagen in Lean neu aufzubauen. Sie bestätigt die Formalisierung dieser Referenz, belegt aber nicht, dass künftige KI-generierte Beweise oder Software ohne Prüfung verlässlich sein werden.

## Quellen und Referenzen

1. [Axiom Math wants to keep AI slop out of mathematics](https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/) – TechCrunch, 2026-11-05
2. [Axiom](https://axiommath.ai/research/the-stacks-project-formalized/?utm_source=openai) – Axiom

Zuletzt aktualisiert: 2026-11-05