Tech Teardown 042 | Stacks: 7.500 Seiten in 16 Mio. Zeilen Lean

Hintergrund und Phänomen: Eine „geschichtlich größte“ Ankündigung mit 94 Sternen

Am 4. November 2026 veröffentlichte Axiom (axiommath.ai) einen beigeschriebenen Blogpost, in dem es hieß, dass die gesamte Stacks-Project-Version in Lean-Formulierung abgeschlossen sei: etwa 16 Millionen Codezeilen (offizielle Angabe; das Repository ist zu groß, um eine separate Anzahl zu überprüfen). Es wurde behauptet, dass dies „die größte integrierte, wiederverwendbare formale Mathematikbibliothek aller Zeiten“ sei. Das Repository AxiomMath/Stacks unterliegt der Apache-2.0-Lizenz, und die Toolchain ist auf lean4 v4.34.0-rc2 gesetzt. Nach Daten vom 6. November 2026 hat das Repository 94 Sterne, HN-Einträge nur 66▲ und 17 Kommentare. Die angebliche Größe der Bibliothek und die damit verbundene Aufmerksamkeit bilden den ersten Beobachtungspunkt dieser Analyse. Warum lohnt sich die Veröffentlichung einer Mathematikbibliothek für eine technische Analyse? Weil sie möglicherweise das größte Projekt im Bereich „AI schreibt Code, Menschen legen Standards fest, Maschinen überprüfen“ ist.

Stacks Project ist an sich die Grundlage der algebraischen Geometrie: Es handelt sich um eine öffentliche Referenzbibliothek, die 2005 von dem Mathematiker Johan de Jong von der Columbia University ins Leben gerufen wurde und etwa 7500 Seiten umfasst. In den letzten zwanzig Jahren haben Hunderte von Mathematikern beigetragen. Das Editierprinzip besteht darin, jedem Satz eine Beweisführung zu geben, Annahmen explizit anzugeben und Abhängigkeiten auf vier Zeichen zurückzuverfolgen. De Jong bezeichnete sich selbst als jemanden, der „die mathematischen Grundlagen wie den Linux-Kernel pflegt“. Eine moderne Beweisführung in der algebraischen Geometrie könnte eine lange Kette von Theoremen aus Kommutative Algebra, Projektive Geometrie, Schichten, Homotopie und algebraischen Stacks umfassen. Lean fehlte bisher genau diese Infrastruktur. Axioms Motivation ist sehr direkt: Die Geschwindigkeit, mit der AI mathematische Beweisführungen generiert, übertrifft die menschliche Überprüfungskapazität bei weitem, weshalb formale Verifizierung zu einer Notwendigkeit geworden ist.

Architektur und technische Prinzipien: Tag-Mapping, zweistufige Überprüfung, mehrere Agenten zur Überprüfung

Das erste Mechanism ist die dauerhafte Vergleichbarkeit. Jede Lean-Ankündigung trägt das Attribut [@stacks TAG], das auf den vier Zeichen langen Tag in Stacks Project verweist. Ein Tag kann mehrere Ankündigungen entsprechen, und wenn ein Teil abgedeckt wird, wird dies durch die Attributnotizen angegeben. Tags, die bereits von Mathlib abgedeckt wurden, werden über add_to_stacks auf den Mathlib-Ankündigungen registriert. Die Ankündigungen sind zudem mit den entsprechenden Grothendieck-Einträgen aus EGA und SGA versehen (zum Beispiel @[ega] mit dem Eintrag IV 7.8.3). Die Attributnotizen unterscheiden zwischen „ganzen Sätzen, allgemeineren Fällen, Teilsätzen und besonderen Situationen“. Die dazugehörige Website stacks.axiommath.ai bietet eine parallele Ansicht der Originaltexte und des Lean-Codes sowie einen interaktiven Abhängigkeitsdiagramm an.

Das zweite Schritt ist ein zweistufiges Überprüfungssystem. Das Repository wird in zwei Ordner unterteilt: StacksCore und StacksFrontier. Core enthält Code, der menschlich überprüft wurde, auf den Originaltext zurückgeführt und die Naming-, Allgemeinheit- und Stilstandards von Mathlib erfüllt. Frontier enthält Code, der von AI-Agenten geschrieben wurde und am schnellsten wächst. Er muss vor dem Eintritt in Core überprüft werden. Der README erklärt klar: Der einzige Unterschied zwischen den beiden Schichten besteht darin, „wer den Code überprüft hat“. Beide sind ebenfalls von dem Lean-Kernel überprüft worden.

Die dritte Schicht ist das Agent-Engineering. Axiom hat eine „Koordinierte AI-Agent-Kluster“ implementiert, die parallele Übersetzung von Aussagen, die Suche nach bestehenden Abstraktionen in Mathlib, die Konstruktion von Beweisen sowie die Lösung vorheriger Abhängigkeiten durchführt. Dabei wird ein hierarchisches Agent-System und ein streng koordinierter Protokoll verwendet (Details des Protokolls werden im Blog nicht angegeben). Die Glaubwürdigkeit der Aussagen wird durch drei Mechanismen gesichert: Mehr-Agent-Audits, eine semantische Überprüfung der Originaltext sowie die harte Einschränkung, dass „jeder Definitionstheorem erfolgreich mit dem nachfolgenden Theorem verbunden sein muss“.

Die vierte Schicht ist ein korrigierender Kreislauf, der von Gegenbeispielen angetrieben wird. Im formalen Prozess wurden Dutzende Aussagen in den Originaltexten von Stacks gefunden, die lokale Korrektur benötigen: fehlende Annahmen, Randfälle im richtigen Merkmalfeld, zu breite Aussagen, die nicht gültig sind. Die Agenten sind dafür verantwortlich, mathematische Hindernisse zu diagnostizieren und explizite Gegenbeispiele zu konstruieren; wenn ein falsches Theorem einen Beweislücke im tieferen Theorem verursacht, werden alternative Wege aus den Literaturquellen gesucht, um das Haupttheorem unter den ursprünglichen Annahmen neu aufzubauen.

Schlüsseldaten: 63.000 Module, kein sorry, drei Axiome

Die folgenden Zahlen stammen von offiziellen Angaben oder aus der Dokumentation des Repos; keine Dritte Überprüfung vorhanden.

Die offizielle Größe beträgt etwa 16 Millionen Zeilen; die README-Dokumentation gibt an, dass es etwa 63.000 Module gibt und dass „jeder Tag mit formulierbaren Inhalten im Stacks-Projekt formalisiert wurde“ (offizielle Angabe der README-Dokumentation). Unformierte Beispiele, Übungen und Anmerkungen werden der Community als Aufgabe überlassen.

Es gibt drei strenge Qualitätskriterien: Der Lean-Kernel überprüft jeden Beweis; im gesamten Repo gibt es kein sorry und keine native_decide; nur die drei Standardaxiome propext, Classical.choice und Quot.sound werden verwendet. Jeder kann mit dem Befehl #print axioms diese Axiome überprüfen.

Der Baukostenansatz ist ein realer Hürde: Die offizielle Anweisung lautet lake exe cache get && lake build. Die vollständige Konstruktion ist zeitaufwendig und verbraucht viel Speicher; die offizielle Pläne gehen in Richtung eines Kompilations-Caching-Dienstes, der bisher noch nicht verfügbar ist. Das bedeutet, dass diese Bibliothek mit 63.000 Modulen für gewöhnliche Personalcomputer momentan nicht besonders geeignet ist.

Community-Daten: Eingegrenzt am 6. November, der Repos hat eine Bewertung von 94★; HN-Einträge (Story 50380979, veröffentlicht am 5.11.2026) haben eine Bewertung von 66▲ und 17 Kommentare. Die Anzahl der Kommentare ist nicht groß, aber die Qualität ist hoch: Es gibt sowohl positive Beurteilungen bezüglich des formalen Ansatzes als auch direkte Fragen zur Verifizierungsphilosophie. Als Vergleich: Derselbe Verein veröffentlichte am 27.10.2026 eine Formalisierung der begrenzten Singularity-Klassifikation (CFSG); Axiom hat die beiden unterschieden: CFSG dreht sich um einzelne Landmark-Theoreme und ist weniger organisatorisch; Stacks ist eine Grundbibliothek, deren Wert in den tausenden wiederholt genutzten Definitionen, Konstruktionen und Theoremen liegt, was die wesentlichen Herausforderungen des Engineering unterscheidet.

Einfluss und Bedeutung: Die „Glaubwürdigkeit der Aussagen“ zu einer überprüfbaren Eigenschaft machen

Erstens ist es die Verwendbarkeit. Dies ist kein Denkmal, sondern eine Grundlage: Mathematiker und AI-Agenten können Stacks importieren und direkt auf die Grundlagen der algebraischen Geometrie zugreifen. Mit den Befehlen #stacks_tags und #stacks_tags! werden alle mit Tag-Anweisungen versehenen Elemente aufgelistet. Was ergänzt wird, ist die Lücke in der modernen algebraischen Geometrie innerhalb des Lean-Ökosystems – die Formalisierung dieses Bereichs kann direkt darauf aufbauen, ohne dass alles von vorne übersetzt werden muss. Dies gilt besonders für Agenten: Die Taskboards teilen „welche Beispiele noch nicht formalisiert wurden“ in bearbeitbare Aufgaben auf, und die README-Datei begrüßt die Community-Redaktion, damit Code aus Frontier in Core übernommen werden kann. Dies schafft eine vorteilhafte Basis für die mathematische Unterstützung durch AI.

Zweitens sind es die Signale der Formalisierung, die die Mathematik weiterentwickeln. Dutzende von Originalaussagen wurden als erforderlich für Korrektur identifiziert, und Agenten haben explizite Gegenbeispiele entwickelt, was zeigt, dass die großangelegte Formalisierung nicht nur eine Übersetzung ist, sondern auch eine automatische Überprüfung des Originaltextes. HN hat darauf hingewiesen, dass das Stacks Project selbst fast wie „Lean in natürlicher Sprache“ ist: Jedes Theorem wird mit einer Beweisführung versehen, Annahmen sind explizit dargestellt und Abhängigkeiten können rückverfolgt werden. Daher ist eine hochwertige Formalisierung nicht überraschend. Ein anderer Kommentator sagte, dass nach der Veröffentlichung von CFSG erwartet wurde, dass jemand Stacks bearbeiten würde.

Drittens sind es die methodologischen Erkenntnisse für AI-Engineering außerhalb der Mathematik (das ist meine Einschätzung). Wenn AI Code massenhaft generiert, ist der schwächste Punkt oft nicht, ob die Beweisführung gültig ist, sondern ob die Aussagen dem ursprünglichen Sinn treu sind: Kernel-Überprüfungen können das Erstere kontrollieren, aber nicht, ob „das Theorem korrekt übersetzt wurde“. Das dreifache Set, das Axiom bietet – mehr-Agenten-Audits, semantische Kollationen und harte Einschränkungen für die Nachverarbeitung – ist im Grunde eine Engineering-Axiom, die „die Treue der Aussagen gegenüber der Richtigkeit der Beweisführung“ priorisiert. Diese Denkweise kann direkt auf jede Situation übertragen werden, in der AI-Übersetzungen als Code für eine großangelegte Auditierung verwendet werden.

Kontroversen und Risiken: Ablehnung von oben nach unten, kritische Kommentare und der Unterschied beim kalten Start

Die spannendsten Grenzen liegen bei der Haltung von oben nach unten. Am 21. Oktober 2026 bat de Jong in einer Ankündigung von oben nach unten, nicht direkt in das Stacks Project-Repository AI-generierte Kommentare und PRs einzureichen (Übermittlung durch Axiom-Blog). Axiom zeigte Respekt vor dieser Grenze: Formalisierung, Gegenbeispiele und Korrekturen blieben alle in seinem Repository, während die Verwaltung von oben nach unten weiterhin von de Jong und der Community erfolgte, damit Mathematiker sie in ihrem eigenen Tempo überprüfen und nutzen konnten. HN hat auf die spannenden Punkte hingewiesen: Der neueste Beitrag auf dem ursprünglichen Stacks Project-Blog vom 21.10 hatte den Titel „No AI for now“. Der Kommentator hatte enttäuscht über die Fortschritte in der AI-Mathematik. Mit anderen Worten, diese 16 Millionen Zeilen Code haben derzeit nur die Identität eines unabhängigen Projekts und haben noch keine Unterstützung von oben nach unten erhalten.

Der zweite Streitpunkt betrifft die Texte. Viele HN-Kommentatoren kritisieren die Veröffentlichung des Blogs als typisches AI-Slop: Metaphern wie „Dieser Meilenstein beginnt mit“ vermitteln ein unklares Gefühl bezüglich der Qualität des Ergebnisses. Die Gegenargumente sind ebenso direkt: Einige Nutzer wiesen darauf hin, dass Axiom eine hohe Finanzierung erhalten hat (der Kommentator behauptete dies ohne unabhängige Überprüfung), und es handelt sich um ein von AI erstelltes großes Lean-Beweisdokument, bei dem die AI-Eigenschaften im Domainnamen selbst enthalten sind. Warum sollte man sich dann über die AI-Stilistik in den Texten ärgern? Meine Meinung: Die Kritik an den Texten berührt nicht das technische Wesentliche, aber sie betrifft ein wirkliches Problem: Der Blog enthält keine offenen Dokumentationen bezüglich des Koordinierungsprotokolls für „Agent-Cluster“. Je weniger transparen das Engineering-Blitzschloss ist, desto leichter wird der Stil der Texte kritisiert werden (das ist meine Einschätzung).

Der dritte Punkt betrifft den Unterschied beim Cold Start. Die Aussage von „die größte formalisierte Mathematikbibliothek aller Zeiten“ passt nicht zu den 94★-Bewertungen und den 17 HN-Kommentaren. Es gibt objektive Gründe dafür: Der Aufbau der gesamten Bibliothek ist schwierig, die Caching-Dienstleistung ist noch nicht verfügbar, und das Publikum für algebraische Geometrie ist bereits begrenzt. Das Thema hat sich sogar über die Grenzen der Algebra-Geometrie hinausgehoben: Ein Kommentator korrigierte speziell eine abwegige Diskussion, was zeigt, dass diese Stack in der Algebra-Geometrie als „Stack“ funktioniert, nicht als technologische Stack. Diese Fehlinterpretation bestätigt, dass die Aufmerksamkeit, die durch die Veröffentlichung erregt wurde, die Fachgrenzen überschritten hat. Aber HN hat auch Fragen bezüglich der Prüfung der Konformität der Annahmen aufgegeben: Wie kann man die Konformität der Annahmen überprüfen? Die multi-agentenbasierte Prüfung im Blog ist die Antwort, nur der fragende Kommentator hat sie nicht gelesen. Ein anderer Kommentar ist noch fundamentaler: Selbst wenn die Beweise vollständig korrekt wären, bleibt das Problem der Mathematik in der AI-Ära die menschliche Verständlichkeit. Menschen, die keine Aufgaben lösen oder Beweise lesen, werden nicht durch die Größe der Bibliothek verstanden.

Schlussfolgerung und Perspektiven: Nur Bibliotheken, die importiert werden können, sind echte Denkmäler

Das Kernwort lautet: Axiom hat das 7500-seitige Werk über algebraische Geometrie in etwa 16 Millionen Lean-Codezeilen übersetzt (offizielle Angabe). Drei Standardaxiome, kein Sorry, vollständige Überprüfung des Kerns und ein doppeltes Bewertungssystem für Core/Frontier sorgen für die Richtigkeit. Doch die Identitätsgrenze „AI-Daten ablehnen“ bleibt ungelöst.

Der Eingang zur Teilnahme ist vorhanden: Importiere Stack-Produkte sofort, suche nach #stacksTags mit der entsprechenden Tagung; erhalte Aufgaben auf der Taskliste auf stacks.axiommath.ai/contributing und verwende die Claim-Tagung in GitHub, um Störungen zu vermeiden. Die Überprüfung des Frontier-Codecs und seine Einführung in Core ist die wichtigste Art der Beiträge im Moment. Drei Dinge sind interessant für normale Entwickler: Ob die Caching-Dienstleistung online geht (entscheidet darüber, ob 63k Module von gewöhnlichen Entwicklern genutzt werden können), ob Axiom die Details des Agent-Koordinierungsprotokolls öffentlich macht (entscheidet darüber, ob multi-agentenbasierte Prüfungen wiederholt werden können) und ob de Jongs Politik verändert wird (entscheidet darüber, ob diese Bibliothek als eigenständiges Projekt in den lebendigen Text integriert werden kann).

Für normale Entwickler bietet diese Bibliothek auch ein Referenzmodell: Wie man eine Bewertung für große Codebibliotheken generiert, die von AI erstellt wurden, und wie man „Konformität mit den ursprünglichen Anforderungen“ in überprüfbare Einschränkungen umwandelt. Meine Schlussfolgerung: Das Interessanteste an Stack-Produkten ist nicht die Zahl der 16 Millionen Zeilen, sondern dass sie die Frage „Ist die Mathematik, die von AI geschrieben wurde, glaubwürdig?“ in zwei getrennte, überprüfbare Fragen aufteilt: Die Richtigkeit wird dem Kern übergeben, die Konformität der Überprüfung. Das Erste bietet eine feste Garantie, das Letzte bietet ein Engineering-Plan, aber keine öffentliche Veröffentlichung auf Protocol-Level – das ist der größte Ungewissheitsfaktor derzeit.

Referenzquellen

• Axiom offizielle Blogseite (axiommath.ai, veröffentlicht am 04.11.2026, unterzeichnet von Axiom; 16 Millionen Zeilen, Agent-Kluster, Gegenbeispiele wurden alle nach offiziellen Angaben genannt; Volltext gespeichert in der lokale Datei stacks.txt)
• Repository: github.com/AxiomMath/Stacks (94★ / Apache-2.0 / lean4 v4.34.0-rc2 / main Branch, Snapshot vom 06.11.2026; README mit 59 gelesenen Zeilen; Das Repository ist zu groß um es zu klonen, die Anzahl der Zeilen wurde nicht gemessen)
• HN-Eintrag: story 50380979 (66▲ / 17 Kommentare, veröffentlicht am 05.11.2026, Snapshot vom 06.11.2026; Die Kommentardatei hn-stacks-full.json enthält 11 Belege, der gesamte Text wurde wiedergegeben, ohne direkte Zitate)
• Hintergrund des Stacks Project und die Ankündigung von de Jong vom 21.10.2026: Beide sind offizielle Darstellungen aus dem Axiom Blog

Unterzeichner: Yongliang