Fermats letzter Satz: Claude-Agenten erstellen einen vollständig prüfbaren Lean-Beweis

Fermats letzter Satz wird maschinell nachprüfbar

Mehr als drei Jahrhunderte lang stand Fermats letzter Satz für eine mathematische Provokation: Die Behauptung ist leicht zu formulieren, ihr Beweis jedoch außerordentlich anspruchsvoll. Nun meldet Anthropic einen Fortschritt anderer Art. Claude-Agenten hätten erstmals eine vollständige Formalisierung des bekannten Beweises in Lean 4 erstellt, die sich vom Computer durchgehend prüfen lässt. Nach Angaben des Unternehmens entstand das Werk in einem weitgehend selbstständigen Lauf von rund elf Tagen.

Entscheidend ist, was diese Meldung bedeutet – und was nicht. Fermats letzter Satz war nicht wieder offen, und die Agenten haben keinen neuen mathematischen Beweis gefunden. Formalisiert wurde ein bekannter Beweisweg, der auf den Arbeiten von Frey, Serre, Ribet, Wiles sowie Taylor und Wiles beruht und der klassischen Darstellung von Darmon, Diamond und Taylor folgt. Die historische mathematische Leistung bleibt damit unangetastet. Neu ist vielmehr der Versuch, den gesamten langen Argumentationsgang so präzise in einer formalen Sprache auszudrücken, dass ein kleiner Prüfmechanismus jeden einzelnen Schritt kontrollieren kann.

Der freigegebene Hauptsatz betrifft natürliche Zahlen: Für einen natürlichen Exponenten n ab 3 und positive natürliche Zahlen a, b und c gilt, dass a^n + b^n nicht gleich c^n ist. Hinter dieser knappen Aussage liegt ein gewaltiges Geflecht aus Definitionen, Hilfssätzen und Abhängigkeiten. Anthropic beziffert den erzeugten Lean-Umfang auf 13 Millionen Zeilen und nennt etwa sechs Milliarden ausgegebene Token. Gemeldet werden außerdem 30.300 bewiesene Zwischenergebnisse, von denen ungefähr 29.500 in den endgültigen Beweis eingingen.

Das Verzeichnis des Repositoriums führt 29.511 Theoremseiten, 1.450 Definitionsmodule und 60.475 erzeugte Module auf. Diese Angaben lassen sich nicht einfach miteinander verrechnen: Sie beruhen auf unterschiedlichen Einheiten und Zählweisen. Auch aus der Tokenzahl kann man weder verlässlich auf Kosten noch auf Energieverbrauch schließen. Eine vollständige öffentliche Kostenaufstellung liegt nicht vor.

Was Lean tatsächlich kontrolliert

Lean behandelt einen Beweis nicht als überzeugenden Fließtext, sondern als streng typisiertes Objekt. Der Kernel prüft, ob jeder Schritt nach den festgelegten Regeln aus den angegebenen Voraussetzungen folgt. Für das veröffentlichte Projekt sind Lean 4.33.1 und Mathlib v4.33.0 festgeschrieben. Die Standardprüfung verlangt, dass der Schlusssatz genau von propext, Classical.choice und Quot.sound abhängt. Damit wird offengelegt, welche Grundannahmen außerhalb der hergeleiteten Sätze in die Prüfung eingehen.

Nach Darstellung im Repositorium verwendet kein Projektmodul die Ausdrücke axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def oder #eval. Das ist wichtig, weil solche Mittel je nach Einsatz Beweislücken offenlassen, Berechnungen an der üblichen Kernelprüfung vorbeiführen oder zusätzliche Vertrauensannahmen einführen könnten. Eine getrennte Aufgabendatei enthält absichtlich sorry; sie gehört laut Projektbeschreibung nicht zum geprüften Paket. Der Unterschied verhindert, dass die unvollständige Aufgabenfassung mit dem eigentlichen Beweis verwechselt wird.

Mehr als nur ein erfolgreicher Build

Das Projekt stützt seine Behauptung auf mehrere Prüfwege. Nach Angaben des Repositoriums bestätigte comparator in Version 4.33.0, dass der bewiesene Satz mit der vorgegebenen Aufgabenstellung übereinstimmt, nur die erlaubten Grundannahmen verwendet und sich im Lean-Kernel erneut prüfen lässt. Das Programm meldete: „Your solution is okay!“ Diese Kontrolle soll insbesondere verhindern, dass zwar irgendein anspruchsvoller Satz formal bewiesen wurde, aber nicht genau die geforderte Form von Fermats letztem Satz.

Hinzu kommt eine unabhängige praktische Bestätigung von Kevin Buzzard. Er berichtet, den Quelltext selbst übersetzt und comparator ausgeführt zu haben; sein Fazit lautet: „it checks out“. Das ist eine gewichtige Bestätigung dafür, dass sich das veröffentlichte Material bauen lässt und die vorgesehenen Prüfungen besteht. Es ist jedoch keine manuelle Begutachtung aller 13 Millionen Zeilen. Buzzards Test besagt ebenso wenig, dass jeder Name treffend, jede Abstraktion zweckmäßig oder jede mathematische Erklärung für Menschen verständlich ist.

Einen weiteren Prüfweg beschreibt Anthropic mit nanoda 0.4.13, einer eigenständigen, in Rust geschriebenen Implementierung eines Lean-Kernels. Sie habe einen Export mit 1.052.234 Deklarationen ohne Fehler akzeptiert. Ein zweiter Kernel ist wertvoll, weil nicht dieselbe Implementierung noch einmal ihre eigenen möglichen Fehler bestätigt. Ganz unabhängig von Änderungen durch das Projekt ist dieser Weg allerdings nicht: Anthropic setzte vier Patches für nanoda ein. Dem Unternehmen zufolge betreffen sie Fortschrittsanzeigen und die Geschwindigkeit der Suche, nicht die Typisierungsregeln. Da das Ergebnis samt diesen Anpassungen vom Projekt selbst berichtet wird, bleiben die Patches ein sinnvoller Gegenstand weiterer externer Prüfung.

Zusammengenommen liefern diese Tests starke, aber klar umrissene Evidenz. Sie zeigen, dass die konkrete Lean-Aussage aus den angegebenen Definitionen und Grundannahmen herleitbar ist und dass der veröffentlichte Stand die vorgesehenen technischen Kontrollen bestanden hat. Gerade die Wiederholung mit einem zweiten Kernel verkleinert das Risiko, dass ein einzelner Implementierungsfehler unbemerkt bleibt.

Wo die Gewissheit endet

„Maschinell geprüft“ bedeutet nicht „jenseits jedes denkbaren Zweifels bewiesen“. Zum vertrauenswürdigen technischen Unterbau gehören weiterhin der Kernel, die Übersetzungskette, Teile des Betriebssystems und letztlich die Hardware. Fehler in diesen Schichten sind unwahrscheinlich, aber nicht logisch ausgeschlossen. Auch kann ein Prüfprogramm nur die exakt formulierte Aussage beurteilen. Ob Definitionen die beabsichtigten mathematischen Begriffe angemessen erfassen, muss zuerst von Menschen verstanden und bewertet werden.

Das Repositorium weist selbst auf eine besonders anschauliche Grenze hin: Werkzeuge können nicht feststellen, ob ein Zwischensatz wirklich das bedeutet, was sein Name nahelegt. Ein formal gültiger Satz kann ungeschickt benannt, kaum lesbar oder für spätere Arbeiten schlecht zugeschnitten sein. Der Kernel prüft Herleitbarkeit, nicht Neuheit, didaktische Qualität, Wartbarkeit oder die Sinnhaftigkeit einer Bibliotheksarchitektur.

Diese Abgrenzung schmälert den Erfolg nicht. Sie erklärt, worin er liegt. Bei einem Beweis dieser Größe besteht die Leistung darin, ein historisch gewachsenes mathematisches Argument vollständig in eine Form gebracht zu haben, die keine stillschweigenden Übergänge duldet. Jeder verwendete Schritt muss als Definition oder Satz vorhanden sein und seine Voraussetzungen müssen passen. Das ist eine andere Art von Zuverlässigkeit als das fachliche Urteil einer Leserin oder eines Lesers – und gerade deshalb eine nützliche Ergänzung.

Ein Forschungsartefakt, keine fertige Bibliothek

Der Quelltext ist unter der Apache-2.0-Lizenz öffentlich zugänglich. Dadurch können Fachleute den Aufbau untersuchen, die Prüfungen wiederholen und einzelne technische Entscheidungen hinterfragen. Zugleich bezeichnet Anthropic das Repositorium ausdrücklich als nicht gepflegtes Forschungsartefakt und nimmt dort keine Beiträge an. Offenheit und langfristige Wartung sind also zwei verschiedene Eigenschaften: Der Stand ist einsehbar, aber nicht als gemeinschaftlich weiterentwickelte Standardbibliothek angekündigt.

Das Projekt entstand zudem nicht auf einer leeren Grundlage. Es nennt abgeleitetes Material aus dem FLT-Projekt des Imperial College London, aus flt-regular und aus Mathlib. Auch die mathematische Argumentation selbst beruht auf jahrzehntelanger menschlicher Forschung. Die Agentenleistung besteht darin, diese vorhandenen Ergebnisse in großem Maßstab zu einer vollständig prüfbaren Lean-Entwicklung zusammenzuführen. Sie sollte weder von den Vorarbeiten gelöst noch als Ersatz für sie dargestellt werden.

Damit unterscheidet sich das Ergebnis auch vom separaten FLT-Projekt am Imperial College. Ein riesiges, eigenständig prüfbares Artefakt erfüllt nicht automatisch dieselben Anforderungen wie lesbarer, wiederverwendbarer und sorgfältig erklärter Code, der in Mathlib aufgenommen werden kann. Buzzard zufolge verfolgt das Imperial-Projekt weiterhin genau dieses Ziel des Bibliotheksaufbaus und der verständlichen Darstellung. Beide Vorhaben können deshalb nebeneinander sinnvoll sein: Das eine zeigt, wie weit sich die vollständige Formalisierung mit Agenten skalieren lässt; das andere arbeitet an einer für Menschen und künftige Formalisierungen tragfähigen mathematischen Bibliothek.

Warum das Ergebnis dennoch bemerkenswert ist

Die gute Nachricht liegt weder in einer nachträglichen Verbesserung von Wiles’ Mathematik noch in der Vorstellung eines unbegrenzt selbstständig forschenden Systems. Bemerkenswert ist die Größenordnung einer Arbeit, die bisher enorme Mengen spezialisierter menschlicher Zeit beanspruchte. Nach Anthropics Darstellung konnten Agenten über viele Tage hinweg Definitionen ergänzen, Hilfssätze beweisen und Abhängigkeiten zu einem vom Kernel akzeptierten Gesamtbeweis verbinden.

„Weitgehend selbstständig“ sollte dabei wörtlich und mit der nötigen Vorsicht gelesen werden. Es ist die Beschreibung des Unternehmens für diesen ungefähr elftägigen Lauf, kein Beleg für schrankenlose Autonomie. Der Lauf fand in einer vorbereiteten technischen Umgebung statt, griff auf bestehende Bibliotheken und frühere Formalisierungsarbeit zurück und verfolgte eine von Menschen festgelegte Aufgabe. Aus dem Ergebnis folgt nicht, dass das System beliebige Forschungsfragen ohne fachliche Vorbereitung lösen könnte.

Gerade die offene Veröffentlichung macht eine nüchterne Einordnung möglich. Außenstehende müssen sich nicht allein auf eine Vorführung oder eine knappe Erfolgsmeldung verlassen: Sie können den bereitgestellten Quelltext untersuchen, die festgeschriebenen Versionen verwenden und die angegebenen Prüfungen nachvollziehen. Buzzards zeitnahe Wiederholung zeigt bereits den Wert dieser Nachprüfbarkeit. Sie ersetzt keine umfassende Langzeitprüfung, schafft aber eine wesentlich bessere Ausgangslage für Kritik als ein geschlossenes Ergebnis.

Die Nachricht war zum Zeitpunkt der Prüfung noch frisch. Anthropics Ankündigung und Buzzards unabhängiger Bericht erschienen beide am 4. September 2026, ungefähr einen Tag vor dieser Bestandsaufnahme. Neu ist folglich die veröffentlichte Formalisierung, nicht der mathematische Satz: Der wurde in den 1990er-Jahren bewiesen.

Für die formale Mathematik ist das ein wichtiger Maßstab. Ein System, das Millionen Zeilen erzeugt, ist allein noch nicht überzeugend; Umfang kann auch Unordnung bedeuten. Hier steht dem Umfang jedoch ein konkreter, wiederholbarer Akzeptanztest gegenüber. Gleichzeitig macht das Projekt sichtbar, welche Aufgaben nach der Kernelprüfung offenbleiben: Begriffe erklären, Strukturen vereinfachen, Code pflegen und Ergebnisse so in Bibliotheken einordnen, dass andere Forschende sinnvoll darauf aufbauen können.

So betrachtet ist die Formalisierung weder bloß eine spektakuläre Zahlensammlung noch der Endpunkt mathematischer Arbeit. Sie ist ein außergewöhnlich großer, öffentlich untersuchbarer Nachweis dafür, dass KI-Agenten einen bekannten, tiefen Beweisweg in eine maschinell kontrollierbare Form überführen können. Die nächste Bewährungsprobe besteht darin, aus solcher formalen Masse dauerhaft verständliche und wiederverwendbare Mathematik zu machen.