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.
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.
