Axiom formalisiert das gesamte Stacks Project in Lean – 16 Millionen Zeilen maschinengeprüfte Mathematik
The Stacks Project, Formalized in Lean
Axiom hat das Stacks Project – rund 7.500 Seiten Grundlagen der modernen algebraischen Geometrie – vollständig in Lean formalisiert. Die Bibliothek umfasst etwa 16 Millionen Zeilen Code und ist damit die größte integrierbare formale Mathematikbibliothek. Koordinierte KI-Agenten-Schwärme übersetzten und bewiesen Tausende Theoreme parallel. Dabei deckte das System Dutzende fehlerhafte oder unvollständige Aussagen im Original auf und lieferte Korrekturen samt Gegenbeispielen. Forscher und KI-Agenten können die Definitionen direkt importieren.
Anstatt fehlgeschlagene Beweisversuche als bloße Hindernisse zu betrachten, diagnostizierten unsere Agenten die zugrunde liegenden mathematischen Obstruktionen und konstruierten explizite Gegenbeispiele, um zu zeigen, wo die ursprünglichen Aussagen zusammenbrachen.