Axiom veröffentlicht eine Lean-Formalisierung des gesamten Stacks Project, rund 16 Millionen Zeilen aus KI-Agentenschwärmen
Das rund 7.500 Seiten starke Referenzwerk der algebraischen Geometrie ist nun eine maschinell geprüfte Bibliothek; externe Mathematiker haben die Treue der Aussagen noch nicht geprüft.
Warum es wichtig ist
Die moderne algebraische Geometrie hatte kaum Lean-Infrastruktur, weil ein einzelner Beweis von langen Ketten von Resultaten aus kommutativer Algebra, Schemata, Garben und Kohomologie abhängen kann. Laut Axiom behält die Bibliothek die dauerhaften Tags des Stacks Project bei, sodass Menschen und KI-Agenten Definitionen und Sätze direkt in neue Beweise importieren können. Sie folgt auf Axioms Lean-Formalisierung der Klassifikation der endlichen einfachen Gruppen vom 27. Oktober 2026. Entscheidend ist, ob Mathematiker, die die Aussagen mit dem Originaltext abgleichen, sie für treu halten und ob die Bibliothek neben Mathlib genutzt wird.
Die wichtigsten Fakten
- Stacks Project: rund 7.500 Seiten
- Etwa 16 Millionen Zeilen Lean-Code
- Erstellt mit koordinierten KI-Agentenschwärmen
- 2005 von Johan de Jong (Columbia University) begonnen
- Einsehbar unter stacks.axiommath.ai
- Folgt Axioms CFSG-Formalisierung vom 27. Oktober 2026