Dreizehn Millionen Zeilen sind erst der Anfang

Kurzfassung: Anthropics Formalisierung von Fermats letztem Satz zeigt, dass KI große mathematische Beweisbestände erzeugen kann. Doch ein maschinell geprüfter Abschluss liefert nicht automatisch eine gut nutzbare Bibliothek. Für Unternehmen liegt darin eine wichtige Unterscheidung: Ein korrektes Ergebnis und ein dauerhaft pflegbarer Wissensbestand sind verschiedene Liefergegenstände – mit eigenen Kosten, Zuständigkeiten und Abnahmekriterien.

Ein Projekt kann erfolgreich abgeschlossen sein und trotzdem erhebliche Arbeit für seine späteren Nutzer hinterlassen. Bei KI-erzeugtem Wissen wird diese Unterscheidung wichtiger: Wenn umfangreiche Ergebnisse schneller entstehen, wächst nicht automatisch die Fähigkeit einer Organisation, sie zu verstehen, zu verändern und in anderen Vorhaben einzusetzen. Der Wert hängt dann auch davon ab, was nach dem eindrucksvollen Abschluss nutzbar bleibt.

Ein bekannter Beweis in einer neuen Form

Anthropic berichtete am 4. September 2026, Claude habe Fermats letzten Satz in elf Tagen weitgehend autonom im Beweisassistenten Lean formalisiert. Entstanden seien rund 13 Millionen Codezeilen und etwa 29.500 im endgültigen Beweis verwendete Hilfssätze. Das mathematische Ergebnis war bereits bekannt. Neu ist hier die vollständige maschinelle Überprüfung einer bestehenden Beweisroute, nicht die erstmalige Lösung des jahrhundertealten Problems.

Lean kontrolliert, ob formalisierte Aussagen aus den angegebenen Definitionen und Voraussetzungen folgen. Es genügt nicht, dass ein Text plausibel klingt. Die einzelnen logischen Schritte müssen so vorliegen, dass das Prüfsystem sie akzeptiert.

Der Mathematiker Kevin Buzzard, der selbst an der Formalisierung arbeitet, beschreibt eine eigene technische Prüfung: Er habe den Code kompiliert und das Vergleichswerkzeug „comparator“ ausgeführt; die Prüfung sei erfolgreich gewesen. Das ist eine externe fachliche Bestätigung des bereitgestellten Ergebnisses. Es ist keine unabhängige Wiederholung der elf Tage, in denen das Agentensystem den Bestand erzeugte.

Gerade Buzzards weitere Beobachtungen machen den Fall für das KI-Management interessant. Er nennt mehr als 13,4 Millionen Zeilen und eine Kompilierungsdauer von fast dem Zwanzigfachen der Mathematikbibliothek Mathlib auf einer Maschine mit 96 Rechenkernen. Dieser konkrete Vergleich ist kein allgemeiner Leistungsmaßstab für formale Methoden. Er zeigt aber: Auch ein erfolgreich geprüftes Ergebnis kann für die weitere Arbeit beträchtliche technische Last erzeugen.

Der Abschluss und das gemeinsame Werkzeug

Buzzard sieht seine eigene Arbeit durch die Formalisierung nicht als erledigt an. Zu seinem Projekt gehören auch Beiträge zu Mathlib und eine Darstellung, mit der Menschen den modernen Beweis erkunden können. Anthropics Formalisierung folgt einer anderen, älteren Darstellung der Beweisroute. Ein vollständiger formaler Abschluss erfüllt damit nicht sämtliche Ziele eines Vorhabens, das zugleich gemeinschaftlich nutzbare Grundlagen und menschliches Verständnis schaffen soll.

Darin liegen zwei unterschiedliche Leistungen. Die erste beantwortet eine begrenzte Frage: Ist dieser Beweis vollständig formalisiert und wird er vom Prüfsystem akzeptiert? Die zweite betrifft den Bestand danach: Welche Begriffe und Hilfssätze können andere übernehmen? Wie finden sie diese? Lassen sie sich ändern, ohne den gesamten Bestand erneut bearbeiten zu müssen?

Mehr Code ist dabei weder automatisch besser noch schlechter. Umfang kann für eine schwierige Aufgabe erforderlich sein. Er sagt nur wenig darüber aus, ob wiederverwendbare Teile verständlich abgegrenzt sind. Eine große Ablage geprüfter Ergebnisse ist noch keine gemeinsam gepflegte Bibliothek.

Für Organisationen verschiebt sich dadurch ein Teil der Arbeit. Wer bisher die Lösung erzeugt hat, muss nicht zwangsläufig auch derjenige sein, der ihre Bestandteile auswählt, vereinheitlicht und langfristig betreut. KI kann die erste Aufgabe beschleunigen, während die zweite eine eigene fachliche Leistung bleibt.

Wiederverwendung hat einen eigenen Preis

Anthropic beschreibt auch, warum die Zusammenarbeit der Agenten zunächst scheiterte: Sie verloren den Überblick über den Projektstand und arbeiteten nicht mehr wirksam zusammen. Die Plattform Prove2Me half laut dem Bericht unter anderem durch einen gerichteten Abhängigkeitsgraphen der Aussagen, getrennte Dateien für Aussagen und Beweise sowie natürlichsprachliche Beschreibungen zum Suchen und Wiederverwenden.

Das ist mehr als eine technische Nebenbemerkung. Selbst in einer Aufgabe mit einem präzisen Prüfergebnis musste bereits während der Erstellung geklärt werden, welche Teilresultate existieren und welche weiteren Schritte auf ihnen aufbauen. Der formale Prüfer ersetzt diese Organisation nicht.

Für die spätere Nutzung kommt eine weitere Entscheidung hinzu: Welche Teile verdienen die laufende Pflege? Es kann wirtschaftlicher sein, wenige gut verständliche Bausteine zu übernehmen, als einen vollständigen, schwer erschließbaren Bestand dauerhaft mitzuführen. Umgekehrt kann bei einer seltenen, hochwertigen Aufgabe der einmalige Gesamtnachweis genügen. Nicht jedes Projekt muss eine allgemeine Bibliothek hinterlassen.

Als betriebliche Übertragung lässt sich eine formalisierte Rabattlogik betrachten. Das folgende Beispiel beschreibt keinen dokumentierten Einsatz bei Anthropic: Ein Unternehmen lässt nachweisen, dass bestimmte Preisregeln eingehalten werden. Der Nachweis für die aktuelle Regelversion kann korrekt sein. Soll eine zweite Produktlinie dieselben Grundlagen verwenden, müssen allgemeine Regeln von produktspezifischen Ausnahmen getrennt, benannt und dokumentiert sein. Sonst beginnt das nächste Projekt mit einer Kopie statt mit einem gepflegten Baustein.

Die Kostenrechnung unterscheidet sich entsprechend. Beim Einzelergebnis zählen Aufwand und Nutzen des konkreten Nachweises. Beim gemeinsamen Bestand kommen Pflege, verständliche Schnittstellen und die Prüfung späterer Änderungen hinzu. Eine kurze Erzeugungsdauer beantwortet keine dieser beiden Wirtschaftlichkeitsfragen allein.

Zwei Abnahmen statt eines unklaren Versprechens

Aus dem Fall folgt eine überschaubare Empfehlung für die Beschaffung KI-gestützter Entwicklungsarbeit: Auftraggeber sollten vorab unterscheiden, ob sie einen geprüften Projektabschluss oder zusätzlich wiederverwendbare Grundlagen erwerben. Das zweite Versprechen benötigt einen eigenen Leistungsumfang und sollte nicht stillschweigend im ersten enthalten sein.

Für den Abschluss wäre zu zeigen, dass das Ergebnis in der vereinbarten Umgebung reproduzierbar geprüft werden kann. Für die Wiederverwendung wäre zusätzlich vorzuführen, wie ein anderes Team einen ausgewählten Baustein findet, versteht, in einem zweiten Fall verwendet und nach einer Änderung erneut prüft. Diese zweite Probe untersucht nicht nochmals dieselbe Korrektheit, sondern die behauptete Nutzbarkeit.

Dafür braucht es kein pauschales Programm zur Formalisierung sämtlichen Unternehmenswissens. Ein begrenzter Anwendungsfall reicht, sofern tatsächlich eine zweite Verwendung absehbar ist. Gibt es sie nicht, kann ein sauber abgegrenztes Einzelergebnis die bessere Bestellung sein.

Anthropics Beweis macht die Größenordnung maschinell erzeugbarer formaler Arbeit sichtbar. Buzzards Einordnung ergänzt die ebenso wichtige Frage nach ihrem weiteren Leben. Für Führungskräfte lautet die praktische Entscheidung deshalb nicht, ob dreizehn Millionen Zeilen beeindruckend sind. Sie lautet, welchen Teil dieses Bestands die Organisation auch beim nächsten Vorhaben noch verwenden und pflegen will.