Fermats letzter Satz: Claude erstellt ersten computergeprüften Beweis in elf Tagen

Claude hat Fermats letzten Satz nicht neu bewiesen, sondern erstmals vollständig so formalisiert, dass der Beweis von Lean maschinell geprüft werden kann. Nach Angaben von Anthropic arbeiteten mehrere Claude-Agenten elf Tage lang an rund 13 Millionen Zeilen Lean-Code und tausenden Zwischenresultaten. Der Erfolg zeigt, wie stark KI die formale Verifikation beschleunigen kann – wirft aber auch die Frage auf, wie sich mathematische Forschung und Begutachtung dadurch verändern werden.

Anthropic hat einen bemerkenswerten Schritt an der Schnittstelle von künstlicher Intelligenz und formaler Mathematik vorgestellt. Nach Angaben des Unternehmens gelang es einem Team aus Claude-Agenten, Fermats letzten Satz vollständig im Beweisassistenten Lean zu formalisieren. Das Ergebnis ist damit nicht nur ein mathematischer Text für menschliche Leser, sondern ein Beweis, dessen logische Schritte von Software überprüft werden können.

Fermats letzter Satz gehört zu den berühmtesten Problemen der Mathematikgeschichte. Pierre de Fermat formulierte im 17. Jahrhundert die Behauptung, dass es für ganzzahlige Exponenten n größer als 2 keine positiven ganzen Zahlen a, b und c gibt, für die aⁿ + bⁿ = cⁿ gilt. Über mehr als drei Jahrhunderte widerstand das Problem zahlreichen Beweisversuchen. Erst Andrew Wiles gelang in den 1990er-Jahren der entscheidende Durchbruch. Sein erster vorgestellter Beweis enthielt allerdings noch eine Lücke, die er gemeinsam mit Richard Taylor schließen musste. Die endgültige Fassung wurde 1995 veröffentlicht.

Der neue Beitrag von Anthropic ist deshalb nicht als neuer mathematischer Beweis von Fermats letztem Satz zu verstehen. Claude hat keine alternative Lösung entdeckt, sondern einen bereits bekannten Beweisweg in eine Form übersetzt und ergänzt, die Lean vollständig prüfen kann. Genau darin liegt jedoch die technische und wissenschaftliche Bedeutung des Projekts: Menschlich geschriebene mathematische Beweise lassen viele Zwischenschritte unausgesprochen, weil sie Fachleuten selbstverständlich erscheinen. Ein formaler Beweisassistent akzeptiert solche Abkürzungen nicht. Jede Definition, jede Schlussfolgerung und jede Abhängigkeit muss präzise genug formuliert sein, damit die Software sie nachvollziehen kann.

13 Millionen Zeilen Lean in elf Tagen

Nach Angaben von Anthropic arbeitete Claude weitgehend autonom über elf Tage an der Formalisierung. Dabei entstanden rund 13 Millionen Zeilen Lean-Code. Insgesamt wurden etwa 30.300 computerverifizierbare Theoreme erzeugt; rund 29.500 davon flossen in den endgültigen Beweis ein. Anthropic zufolge ist der fertige Beweis mehr als fünfmal so groß wie Mathlib, die zentrale Community-Bibliothek für Lean, auf der das Projekt aufbaut. Das Unternehmen weist allerdings selbst darauf hin, dass der enorme Umfang nicht mit mathematischer Eleganz gleichzusetzen ist: Mathlib ist über Jahre hinweg verdichtet und überprüft worden, während der von Claude erzeugte Code vermutlich deutlich länger ist als nötig.

Entscheidend war offenbar nicht nur das Sprachmodell selbst, sondern auch die technische Infrastruktur rund um die Agenten. Frühe Versuche scheiterten laut Anthropic daran, dass einzelne Agenten den Überblick über den Projektzustand verloren und nicht mehr effektiv zusammenarbeiteten. Den Durchbruch brachte die Plattform Prove2Me, die von Tianyi Peng und seinen Mitstreitern an der Columbia University entwickelt wurde. Dort wurden Theoreme und ihre Abhängigkeiten in einem gerichteten azyklischen Graphen organisiert. So konnten verschiedene Agenten parallel an Teilproblemen arbeiten, ohne ständig den gesamten Projektkontext im Gedächtnis behalten zu müssen.

Der im Dokument gezeigte Projektplan verdeutlicht diese Struktur. Mehrere große Beweisstränge, darunter Bausteine rund um Resultate von Barry Mazur, Ken Ribet und den späteren Wiles-Teil, werden schrittweise zusammengeführt. Damit orientiert sich die Formalisierung an einer vereinfachten Darstellung des Wiles-Beweises von Henri Darmon, Fred Diamond und Richard Taylor. Auch vorhandene Arbeiten aus dem von Kevin Buzzard geleiteten FLT-Projekt am Imperial College London sowie weitere Lean-Bibliotheken wurden genutzt.

Die Rolle der Menschen blieb begrenzt

Die Rolle der Menschen blieb laut Anthropic vergleichsweise begrenzt, aber nicht bedeutungslos. Tianyi Peng gab gelegentlich strategische Hinweise dazu, welche mathematischen Bausteine Priorität haben sollten. Die eigentliche Ausarbeitung übernahmen Dutzende Claude-Agenten. Für das gesamte Projekt wurden nach Angaben des Unternehmens etwa sechs Milliarden Ausgabetokens eines internen Forschungsmodells verbraucht, das ungefähr mit Claude Fable 5.1 vergleichbar sei. Der fertige Beweis wurde anschließend von Lean geprüft. Anthropic schreibt außerdem, dass er nur die drei Standardaxiome von Lean verwendet und dass ein Vergleichswerkzeug bestätigte, dass die formalisierte Aussage mit der in Mathlib hinterlegten Formulierung von Fermats letztem Satz übereinstimmt.

Der Mathematiker Kevin Buzzard, der selbst seit Jahren an der Formalisierung moderner Mathematik arbeitet, bewertete das Ergebnis gegenüber Anthropic als außergewöhnlichen Fortschritt. Für ihn zeigt der Erfolg, dass automatische Formalisierung inzwischen robust genug sein könnte, um auf ihr weitere formale Mathematik aufzubauen. Gerade dieser Punkt ist für die Forschung relevant: Die Überprüfung komplexer Beweise kann Monate oder Jahre dauern. Historisch gibt es zahlreiche Beispiele, bei denen Fehler spät entdeckt wurden oder die Fachwelt lange brauchte, um sich von der Korrektheit eines Resultats zu überzeugen.

Formale Verifikation als zusätzliche Sicherheitsebene

Formale Beweissysteme versprechen hier eine zusätzliche Sicherheitsebene. Sie ersetzen nicht die mathematische Erklärung für Menschen, können aber zuverlässig überprüfen, ob ein Schluss tatsächlich aus den vorausgesetzten Definitionen und Axiomen folgt. Anthropic argumentiert deshalb, dass formalisierte Versionen künftig häufiger parallel zu klassischen Fachartikeln entstehen könnten. Das wäre besonders dann wichtig, wenn KI-Systeme selbst immer mehr mathematische Resultate produzieren und menschliche Gutachter mit der Menge neuer Beweise kaum noch Schritt halten.

Trotz des eindrucksvollen Ergebnisses sollte der Fortschritt sachlich eingeordnet werden. Claude hat nicht gezeigt, dass ein Sprachmodell ohne Vorarbeiten eigenständig die mathematische Theorie hinter Wiles' Beweis entwickelt. Das System konnte auf jahrzehntelange Forschung, bestehende Formalisierungsprojekte, Mathlib und eine gezielt entwickelte Kollaborationsplattform zurückgreifen. Auch der enorme Rechen- und Tokenaufwand zeigt, dass der Prozess derzeit keineswegs kostenlos oder trivial ist. Zugleich ist gerade die Geschwindigkeit auffällig: Eine Aufgabe, für die in der mathematischen Community ein mehrjähriges Projekt geplant war, wurde laut Anthropic in weniger als zwei Wochen zu einem vollständigen End-to-End-Beweis geführt.

Anthropic nennt zudem ein kleineres Folgeexperiment als Hinweis darauf, dass diese Methode nicht auf ein einzelnes Großprojekt beschränkt bleiben muss. Mit drei persönlichen Claude-Max-Plänen seien Agenten über Prove2Me in der Lage gewesen, eine Formalisierung des Drei-Primzahlen-Satzes von Vinogradov in drei Tagen abzuschließen. Das Unternehmen leitet daraus die Hoffnung ab, dass sich auch anspruchsvolle Formalisierungsprojekte künftig mit allgemein verfügbaren KI-Werkzeugen bearbeiten lassen.

Für die Mathematik könnte das langfristig weitreichende Folgen haben. Wenn KI-Systeme zuverlässig dabei helfen, Fachliteratur in maschinenprüfbare Beweise zu überführen, könnten Fehler in bestehenden Arbeiten früher entdeckt und neue Resultate schneller geprüft werden. Gleichzeitig würde sich die Arbeit von Mathematikern verändern: Ein größerer Teil der Forschung könnte darin bestehen, Ideen verständlich zu formulieren, geeignete formale Strukturen festzulegen und automatisierte Systeme zu steuern, während Beweisassistenten die logische Detailarbeit kontrollieren.

Die Formalisierung von Fermats letztem Satz ist deshalb weniger ein neuer Triumph über ein altes Rätsel als ein Test für eine neue Forschungsinfrastruktur. Der mathematische Satz war seit 1995 bewiesen. Neu ist, wie schnell ein KI-gestütztes System einen extrem komplexen Beweis in eine Form überführen konnte, die ein Computer vollständig kontrolliert. Sollte sich dieser Ansatz auf weitere Gebiete übertragen lassen, könnte formale Verifikation von einer spezialisierten Disziplin zu einem alltäglichen Bestandteil moderner Mathematik werden.