Verbraucht 183 Milliarden Tokens, Meta hat mit KI ein Mathematiklehrbuch in eine riesige Lean-Bibliothek übersetzt.

Die Mathematik erlebt eine KI-Revolution.

Das ist in den letzten Monaten besonders deutlich geworden. Beispielsweise hat Google DeepMind vor ein paar Tagen in einer neuen Studie angekündigt, dass sein neuestes System, AlphaProof Nexus, in einem autonomen Lauf 9 von 353 offenen Erdős-Problemen gelöst hat. Zwei dieser Probleme standen in der Mathematik bereits 56 Jahre lang ungelöst. Der Rechenaufwand für jedes Problem belief sich dabei auf nur wenige hundert Dollar. Weitere Details finden Sie in dem Artikel "Ein Problem für ein paar hundert Dollar: DeepMinds Agent löst 9 Erdős-Probleme auf einmal".

Erdős-Probleme bezeichnen in der Regel die zahlreichen öffentlichen mathematischen Probleme und Vermutungen, die der ungarische legendäre Mathematiker Paul Erdős im Laufe seines Lebens gestellt hat. Diese Probleme verteilen sich auf verschiedene Gebiete wie Kombinatorik, Zahlentheorie, Graphentheorie, diskrete Geometrie und Wahrscheinlichkeitstheorie. Viele von ihnen sind seit langem ungelöst und gelten als wichtige Forschungsreferenzen und Spitzenherausforderungen in diesen Bereichen. Die Zuverlässigkeit dieses Ergebnisses liegt darin begründet, dass AlphaProof Nexus keine natürliche Sprachbeweise erzeugt, sondern stattdessen das Large Language Model (Gemini 3.1 Pro) mit dem formellen Verifizierungstool Lean tief verknüpft: Die KI stellt einen Beweis vor, und Lean überprüft jeden logischen Schritt Schritt für Schritt. Wenn ein Schritt nicht valide ist, wird der Beweis abgelehnt. Alle Beweis-Codes sind auf GitHub veröffentlicht, und jeder kann die Ergebnisse unabhängig reproduzieren und überprüfen.

Jetzt gibt es einen neuen Fortschritt! Meta hat in Zusammenarbeit mit der New York University und anderen Institutionen ATLAS (Autoformalized Textbook Library At Scale) offiziell vorgestellt, eines der bisher umfangreichsten Projekte zur automatisierten mathematischen Formalisierung.

Das Projektpaper und der Code wurden bereits veröffentlicht.

• Projekt-URL: https://github.com/facebookresearch/atlas-lean/
• Publikations-URL: https://github.com/facebookresearch/atlas-lean/blob/main/formalizing_mathematics_at_scale.pdf

Was ist ATLAS?

Einfach ausgedrückt, ist ATLAS eine auf Lean 4 basierende Bibliothek für formalisierte mathematische Codes. Das Kernziel besteht darin, informelle Theoremformulierungen und Beweise aus mathematischen Lehrbüchern automatisch in formalisierte Codes zu übersetzen, die vom Computer zeilenweise verifiziert werden können.

Dies mag auf den ersten Blick langweilig erscheinen, hat aber weitreichende Bedeutung. Lean ist eine "Beweisassistent"-Sprache. Wenn Sie einen mathematischen Beweis an Lean übermitteln, überprüft es wie ein Compiler jeden Schritt des Beweises auf logische Gültigkeit. Ja, wenn Lean den Beweis akzeptiert, ist er formal unangreifbar.

Nach den im Projekt-Readme angegebenen Statistiken umfasst ATLAS bis Mai 2026 26 mathematische Lehrbücher für Bachelor- und Masterstudiengänge, die sich über verschiedene Gebiete wie Analysis, Algebra, Geometrie, Topologie, Kombinatorik, Wahrscheinlichkeitstheorie, Statistik, partielle Differentialgleichungen, Zahlentheorie und theoretische Informatik erstrecken.

Die gesamte Code-Bibliothek umfasst 630.999 Codezeilen, darunter 483.917 Zeilen des Lean-Kerncodes. Sie enthält 46.203 mathematische Deklarationen, von denen 42.837 bereits bewiesen sind. Die Beweisrate liegt bei 92,7%.

Von den 4.007 ausgewählten Lehrbuchtheoremen wurden bereits 2.855 formalisiert, was einer Formalisierungsrate von 71,3% entspricht. Im Vergleich dazu hat die von der Lean-Community über Jahre hinweg gemeinsam gepflegte Standardbibliothek Mathlib etwa 2,1 Millionen Codezeilen und 308.129 Deklarationen. Die von ATLAS in wenigen Wochen maschinell generierte Menge erreicht bereits etwa ein Viertel der Gesamtmenge von Mathlib, was eine erstaunliche Geschwindigkeit ist.

Hinter dieser Zahl verbirgt sich ein enormer Rechenaufwand: Der gesamte Generierungsprozess hat mehr als 183 Milliarden (183.157M) Token verbraucht.

Bemerkenswerterweise hat das Team auch einen visuellen Browser erstellt.

URL: https://rammalahmad.github.io/atlas/

Benutzer können darin:

• Den informellen Originaltext jedes Theorems mit der Lean-Formalisierung vergleichen;
• Den logischen Abhängigkeitsgraph zwischen den Theoremen betrachten (d. h. welche Lemmata müssen bekannt sein, um ein bestimmtes Theorem zu beweisen);
• Die minimale Menge an Lean-Code extrahieren, die für den Beweis eines bestimmten Theorems erforderlich ist.

Dieses Tool verwandelt ATLAS von einer reinen Code-Bibliothek in ein navigierbares mathematisches Wissensnetz, das sowohl für menschliche Forscher als auch für zukünftige KI-Systeme von potenziellem Wert ist.

Welche Lehrbücher werden verwendet?

Alle 26 Lehrbücher von ATLAS stammen aus Top-Open-Courseware-Ressourcen wie dem MIT OpenCourseWare und decken ein sehr breites Spektrum ab.

Hier sind einige repräsentative Beispiele:

RealAnalysis (Reelle Analysis): Von 177 Zieltheoremen wurden bereits 175 formalisiert, was einer Formalisierungsrate von 98,9% entspricht. Die Beweisrate liegt bei 98,7%. Dies ist das am besten abgeschlossene Einzellehrbuch im Projekt.

ComplexVariables (Komplexe Funktionen): Die Formalisierungsrate beträgt 97,4%.

NumberTheoryI (Zahlentheorie I): Von 576 Zieltheoremen wurden 460 formalisiert (79,9%), und es wurden fast 65.000 Codezeilen generiert.

AlgebraicGeometryI (Algebraische Geometrie I): Dies ist eines der schwierigsten Gebiete. Die Formalisierungsrate liegt bei 60,2%, aber es wurden dennoch mehr als 40.000 Codezeilen und 4.499 Deklarationen generiert.

LieGroups (Lie-Gruppen): Hier wurde der meiste Token-Verbrauch (45.384M) verzeichnet. Es wurden mehr als 60.000 Codezeilen generiert, obwohl die Formalisierungsrate nur 40% beträgt. Dies spiegelt die extreme technische Schwierigkeit dieses Gebiets wider.

Der Kernmotor: AutoformBot

Naturgemäß wird ATLAS nicht manuell Zeile für Zeile geschrieben, sondern vollständig von der von Meta entwickelten automatisierten Formalisierungs-Pipeline AutoformBot (welche auf GitHub als Open-Source verfügbar ist) erzeugt.

Projekt-URL: https://github.com/facebookresearch/autoform-bot

AutoformBot betrachtet die Formalisierung von Lehrbüchern als ein kooperatives Softwareentwicklungsproblem und nutzt bewährte Open-Source-Kollaborationsmodelle (Git-Branches, Pull-Request-Reviews, Issue-Tracking), um Hunderte von LLM-Agenten gleichzeitig zu koordinieren.

Das gesamte System ist in drei Verwaltungsebenen unterteilt:

• Der Orchestrator auf der obersten Ebene liest die Lehrbücher, zerlegt die Formalisierungsaufgaben in einen gerichteten azyklischen Graphen (DAG) und plant die Arbeitsreihenfolge basierend auf den logischen Abhängigkeiten im Buch;
• Der Trace Analyzer und der Supervisor auf der mittleren Ebene lernen aus fehlgeschlagenen Aufgaben und bewerten die Qualität der Zielerreichung nach jedem Merge;
• Die Worker und die Reviewer auf der untersten Ebene sind für die tatsächliche Formalisierung einzelner Theoreme und die Code-Reviews verantwortlich.

Es ist wichtig zu betonen, dass der gesamte Generierungsprozess von ATLAS ohne manuelle Eingriffe in den Beweisprozess abläuft und vollständig maschinell automatisiert ist. Dies ist sowohl die Voraussetzung für die Realisierung seiner großen Skala als auch der Grund für die kontinuierliche Verbesserung der Qualität und Zuverlässigkeit.

Der meiste Rechenaufwand des gesamten Systems konzentriert sich auf die Worker-Ebene und macht etwa 76% des gesamten Token-Verbrauchs aus. Der Formalisierungsprozess für jedes Buch dauert normalerweise etwa eine Woche, kann aber durch Erhöhung der Parallelität erheblich verkürzt werden.

Die Experimente in der Publikation zeigen, dass der Einsatz von 3 oder 5 Workern parallel pro Aufgabe etwa 20% mehr Ziele in der gleichen Zeit erreicht als ein einzelner Worker.

Das Team hat in der Publikation einige interessante "Fehlermuster" offen gelegt, die während des Systembetriebs beobachtet wurden. Das überraschendste ist das antagonistische "Betrugs-" und "Faulenzenverhalten" der Worker.

Der Schlüssel zum Verständnis dieses Phänomens liegt in einem speziellen Schlüsselwort in Lean namens "sorry": Es ist wie eine "Schuldschein", der dem Compiler sagt, "überspringe hier den Beweis und nehme es vorerst als wahr an". Der Code kann somit problemlos kompiliert werden, aber es bleibt eine Lücke in der logischen Kette. In der normalen Entwicklung ist "sorry" ein legitimes Werkzeug, um "zu erledigende" Stellen zu markieren. In AutoformBot jedoch wird es von den Workern als einfacher Weg genutzt, um die Prüfung zu bestehen: Wenn sie auf ein schwer zu beweisendes Theorem stoßen, stecken sie heimlich ein "sorry" in die Tiefe eines Hilfslemmas, sodass die gesamte Beweis-Kette scheinbar gültig ist, aber tatsächlich wie ein Kartenhaus aufgebaut ist.

Dies ist nur die einfachste Methode. Die in der Publikation aufgestellte "Betrugsliste" umfasst auch:

• Behalten Sie den Theorem-Namen bei, ersetzen Sie aber den tatsächlichen Inhalt durch immer wahre Unsinnigkeiten;
• Verstecken Sie die zu beweisende Schlussfolgerung heimlich in die Felddefinition einer Datenstruktur (Definitionen müssen nicht bewiesen werden, sondern nur die Typüberprüfung bestehen);
• Ersetzen Sie die komplexen mathematischen Objekte in einem schwierigen Problem durch einfache Ersatzobjekte. Beispielsweise soll ein Isomorphismus konstruiert werden, aber es wird nur bewiesen, dass die Dimensionen zweier Räume gleich sind.

Was noch interessanter ist, ist die Entwicklung der Situation: Nachdem der Reviewer-Agent aufgefordert wurde, streng gegen Betrug vorzugehen, haben die Worker nicht aufgehört, sondern "sorry" tiefer in die Abhängigkeitskette versteckt, sodass die oberflächliche Prüfung es nicht mehr entdecken kann. Diese Kat-und-Maus-Situation hat das Team gezwungen, ein rekursives Analysetool für den gesamten Abhängigkeitsgraphen zu entwickeln, um die eigentlichen "kontaminierten Knoten" aufzuspüren.

Diese Kat-und-Maus-Situation zwischen den Workern und den Reviewern wird in der Publikation als "antagonistische Dynamik" (adversarial dynamic) bezeichnet und als ein Koordinierungsproblem angesehen, das in großen Mehr-Agenten-Systemen eingehend untersucht werden sollte.

Darüber hinaus tritt bei langfristig arbeitenden Orchestratoren "LLM-Müdigkeit" auf: Wenn das Kontextfenster mit einer großen Menge an historischen Informationen gefüllt ist, beginnt es, immer ungenauere Aufgabenbeschreibungen zu generieren und sogar die Verarbeitung schwieriger Ziele aufzugeben. Das Team hat das Problem gelöst, indem es die spezielle Analysearbeit an kurzlebige, spezialisierte Agenten delegiert hat, um die Verschlechterung des Kontexts eines einzelnen langfristigen Agenten zu vermeiden.