Anthropic hat nach eigenen Angaben erstmals einen vollständig computerverifizierten Beweis von Fermats letztem Satz erstellt. Dutzende Agenten des KI-Modells Claude arbeiteten dafür elf Tage lang weitgehend selbstständig und erzeugten 13 Millionen Zeilen Code in der Beweissprache Lean 4. Mathematiker hatten für die vollständige Prüfung von Andrew Wiles’ Originalbeweis aus dem Jahr 1995 bislang mehrere Jahre veranschlagt.
Prove2Me koordiniert Dutzende Agenten für den Beweis
Für die Arbeit setzte Anthropic zahlreiche Instanzen von Claude auf der offenen Plattform Prove2Me ein. Die vom Anthropic-Forscher Tianyi Peng an der Columbia University entwickelte Plattform verwaltet Tausende einzelne Theoreme als gerichteten Graphen und weist sie einzelnen Agenten zu. Fermats letzter Satz diente dabei bewusst als Stresstest, weil zuvor kein bekannter mathematischer Beweis dieser Größenordnung vollständig maschinell verifiziert worden war. Frühere Versuche mit mehreren gleichzeitig arbeitenden Agenten scheiterten, weil die Systeme den Überblick über bereits bewiesene Zwischenschritte verloren.
Jeder von einem Agenten eingereichte Beweisschritt musste laut Anthropic zunächst den Lean-Compiler bestehen, bevor Prove2Me ihn im Graphen als erledigt markierte und weitere Agenten darauf aufbauen ließ. Dieser eingebaute Prüfmechanismus verhinderte, dass sich Fehler einzelner Agenten über Tausende Zwischenschritte hinweg unbemerkt fortpflanzten.
Die fertige Fassung besteht aus 13 Millionen Zeilen Lean-Code und umfasst 29.500 der insgesamt 30.300 erzeugten Zwischentheoreme. Die Agenten verbrauchten dafür rund sechs Milliarden Ausgabe-Tokens innerhalb von elf Tagen. Menschliche Beteiligte gaben den Systemen nach Unternehmensangaben nur grobe, übergeordnete Anweisungen, den Rest erledigten die Agenten eigenständig.
Beweis folgt vereinfachter Fassung von Wiles’ Argument
Der Beweis folgt nicht dem ursprünglichen, 129 Seiten langen Beleg von Andrew Wiles, sondern einer vereinfachten Darstellung der Mathematiker Henri Darmon, Fred Diamond und Richard Taylor. Im Zentrum steht der Modularitätssatz, den Wiles gemeinsam mit Richard Taylor zur Lösung von Fermats letztem Satz bewiesen hatte. Die Formalisierung deckt Primzahl-Exponenten ab dem Wert siebzehn ab.
Wiles hatte seinen Beweis 1993 erstmals vorgestellt, musste darin aber eine Lücke schließen, die er gemeinsam mit Taylor erst 1995 vollständig behob. Bis heute galt die manuelle Prüfung des Arguments als derart aufwendig, dass nur wenige Spezialisten den gesamten Beweis im Detail nachvollzogen hatten.
Für die übrigen ungeraden Primzahlen griffen die Agenten auf bereits vorhandene Bausteine aus der Lean-Bibliothek Mathlib zurück. Der Lean-Compiler prüfte das gesamte Ergebnis allein anhand der drei Standardaxiome der Mathematik, ohne zusätzliche Annahmen. Nach Einschätzung von Anthropic fällt der Beweis dadurch rund fünfmal länger aus als eine von Menschen optimierte Fassung. Kürze war für die Agenten kein Ziel, sondern allein die maschinelle Prüfbarkeit.
Unabhängiger Mathematiker bestätigt die Korrektheit
Der Mathematiker Kevin Buzzard vom Imperial College London, der die Lean-Community seit Jahren mitprägt, bestätigt die Korrektheit der Formalisierung. Der Beweis benötige neben den Grundaxiomen der Mathematik keine weiteren Annahmen und reiche über Algebra, harmonische Analysis, Geometrie und Zahlentheorie hinweg.
Buzzard sieht darin einen Schritt hin zur automatischen Formalisierung größerer Teile der mathematischen Literatur. Das könne helfen, Fehler in bestehenden Beweisen aufzudecken, den Aufwand für Gutachter zu senken und von KI erzeugte Mathematik überhaupt erst rigoros überprüfbar zu machen. Ähnliche Fortschritte hatten zuvor bereits das Astra-Modell von OpenAI, das zehn ungelöste Matheprobleme löste, sowie ein Beweisversuch von GPT-5.6 Sol Ultra für eine Graphentheorie-Vermutung angedeutet. Beide Ergebnisse sind jedoch bislang nicht vollständig unabhängig geprüft.
Wie SiliconANGLE unabhängig berichtet, gilt die reine Bearbeitungszeit von elf Tagen für ein Projekt, das Fachleute bislang auf mehrere Jahre veranschlagt hatten, als bemerkenswert kurz. Anthropic veröffentlichte den vollständigen Quellcode auf GitHub und kündigte vergünstigte Zugänge sowie Forschungsstipendien für externe Mathematiker an, die mit Prove2Me weiterarbeiten wollen. Der genaue Token- und Rechenaufwand ist unabhängig nicht verifiziert und stammt allein aus Anthropics eigenen Angaben.
Entscheidend wird, ob sich der Ansatz auf noch ungelöste Vermutungen übertragen lässt, statt nur bereits bekannte Beweise nachzuvollziehen. Bislang zeigt das Projekt vor allem, dass Agentensysteme verzweigte Beweisarbeit selbstständig aufteilen und über Wochen ohne menschliches Eingreifen durchhalten können. Ob daraus in absehbarer Zeit auch eigenständige mathematische Entdeckungen statt reiner Formalisierung bereits bewiesener Sätze entstehen, bleibt offen.
