Das Wichtigste in Kürze
- Axiom kündigt 16 Millionen Zeilen Lean zum gesamten Stacks Project an, einem offenen Nachschlagewerk der algebraischen Geometrie mit über 7500 Seiten.
- Codequalität und die starke Vernetzung des Werks sollen erhalten bleiben; erzeugt haben das KI-Agenten.
- Eine öffentliche Seite, ein Download oder ein nutzbarer Build ist bislang nicht erschienen.
Kurzüberblick
| Umfang | 16 Millionen Zeilen Lean |
|---|---|
| Vorlage | Gesamtes Stacks Project, 7500+ Seiten |
| Angekündigt | 4. November 2026 |
| Zugang | Noch keine öffentliche Seite oder Download |
| Kategorie | KI & Modelle |
| Urheber | Axiom |
| Trend-Index | 🔥 4,6 Mio. Trend-Index |
| Veröffentlicht | |
| Zuletzt aktualisiert |
Eine mathematische Stadt aus Lean
Die meisten halten Vibecoding im großen Maßstab für Slop. Hier ist ein Gegenbeispiel.
Axiom stellt die Arbeit als Gegenbeispiel zu der Annahme vor, großflächiges KI-Programmieren liefere nur unbrauchbaren Code. Veröffentlicht werden soll eine Formalisierung des gesamten Stacks Project: kritischer Unterbau der modernen Mathematik, den Axiom als mathematische Stadt beschreibt.
Die Vorlage ist die offene Enzyklopädie der algebraischen Geometrie mit mehr als 7500 Seiten. Daraus sind laut Ankündigung 16 Millionen Zeilen Lean geworden. Lean ist die Sprache, in der Beweise maschinenprüfbar festgehalten werden; konkrete Beweisziele, Dateistruktur und Prüfzeiten nennt die Ankündigung nicht.
Was an der Struktur hängen bleibt
Axiom betont optimierte Codequalität und den Erhalt der stark vernetzten Struktur des Stacks Project. Gemeint ist nicht eine lose Sammlung einzelner Dateien, sondern ein Geflecht, in dem Definitionen, Lemmas und Verweise aufeinander aufbauen. Genau diese Verknüpfung macht das Werk als Infrastruktur brauchbar.
- Gesamtes Werk
Formalisiert werden soll das komplette Stacks Project, nicht ein einzelnes Kapitel.
- Agenten
Erzeugt haben den Lean-Code KI-Agenten von Axiom; Modellname, Laufzeit und Prüfpipeline sind nicht genannt.
- Open Source
Die Ankündigung spricht von einer Veröffentlichung inklusive Open Source, ohne Repository-Adresse.
Zugang und offene Punkte
Bisher gibt es keinen öffentlichen Build, keinen Download und keine offizielle Projektseite. Sichtbar ist die Ankündigung nur in einem kurzen Vorschauvideo. Du kannst den Code deshalb noch nicht selbst laden, prüfen oder in ein Lean-Projekt einbinden.
Preise, API, App und Nutzungsgrenzen sind nicht genannt, weil es sich nicht um einen Chatbot mit Tarif, sondern um eine angekündigte Codebasis handelt. Ungeklärt bleibt, wie vollständig die 16 Millionen Zeilen geprüft sind, welche Lean-Version gilt und wann das Repository wirklich erreichbar ist. Ein Vergleich mit anderen Beweisassistenten oder Formalisierungen lässt sich aus den vorliegenden Angaben nicht mit Zahlen führen.
| Punkt | Stand laut Ankündigung |
|---|---|
| Vorlage | Gesamtes Stacks Project, über 7500 Seiten |
| Ergebnis | 16 Millionen Zeilen Lean, Struktur erhalten |
| Herstellung | KI-Agenten, optimierte Codequalität |
| Öffentlicher Zugriff | Noch keine Seite und kein Download |
Häufige Fragen
Kann ich die Formalisierung schon herunterladen?
Nein. Eine öffentliche Seite, ein Download oder ein nutzbarer Build ist noch nicht erschienen. Bisher liegt nur die Ankündigung mit kurzem Vorschauvideo vor.
Ist das ein neues Sprachmodell zum Chatten?
Nein. Axiom beschreibt eine Lean-Formalisierung des Stacks Project, erzeugt von KI-Agenten. Ein Modellname, eine App oder eine API wird nicht genannt.
