Claude-Agenten übersetzen Fermats Beweis in Lean
Anthropic hat nach eigenen Angaben die erste vollständig computerverifizierte Fassung des Beweises von Fermats letztem Satz vorgelegt. Ein Schwarm aus Claude-Agenten benötigte dafür elf Tage und erzeugte 13 Millionen Zeilen Lean-Code sowie rund 29.500 Zwischentheoreme.
Es handelt sich nicht um einen neuen mathematischen Beweis. Formalisiert wurde eine vereinfachte Fassung des 1995 veröffentlichten Beweises von Andrew Wiles nach Darmon, Diamond und Taylor. Fermats letzter Satz besagt, dass die Gleichung xⁿ + yⁿ = zⁿ für ganzzahlige Exponenten n > 2 keine positiven ganzzahligen Lösungen besitzt.
Was maschinelle Verifikation konkret bedeutet
Lean ist zugleich Programmiersprache und Beweisassistent. Mathematische Aussagen werden darin so präzise beschrieben, dass das System jeden einzelnen logischen Schritt prüfen kann. Fehlt ein Schritt oder folgt eine Aussage nicht aus den Voraussetzungen, lässt sich der Beweis nicht erfolgreich kompilieren.
Der erzeugte Code verwendet laut Anthropic ausschließlich die drei Standardaxiome von Lean. Die zentrale Aussage wurde zudem gegen die Definition in Mathlib geprüft. Mathlib ist die gemeinschaftlich gepflegte Standardbibliothek für formalisierte Mathematik in Lean.
Der Mathematiker Kevin Buzzard vom Imperial College London hat den Code unabhängig kompiliert und die Übereinstimmung mit der Mathlib-Definition geprüft. Eine breite Begutachtung durch die internationale Fachgemeinschaft steht allerdings noch aus. Der vollständige Code und eine schriftliche Erläuterung sind in einem öffentlichen GitHub-Repository von Anthropic verfügbar.
Kevin Buzzard bezeichnet das Ergebnis sinngemäß als „großen Schritt hin zur automatischen Formalisierung der modernen mathematischen Literatur“.
13 Millionen Codezeilen in elf Tagen
| Kennzahl | Wert | Einordnung |
|---|---|---|
| Lean-Code | 13 Millionen Zeilen | Vollständige formale Beschreibung des Beweises |
| Zwischentheoreme | Rund 29.500 | Maschinell geprüfte logische Teilschritte |
| Laufzeit | 11 Tage | Arbeit eines koordinierten Claude-Agentenschwarms |
| Output-Token | Rund 6 Milliarden | Von Anthropic genannter Ressourcenverbrauch |
| Geschätzte Token-Kosten | 100.000 bis 300.000 US-Dollar | Rechnerische Hochrechnung, nicht von Anthropic bestätigt |
| Menschliches Community-Projekt | Gefördert bis September 2029 | Vergleichbares Projekt am Imperial College London |
Die Größenordnung macht deutlich, warum menschlich geschriebene Beweise nicht direkt maschinenlesbar sind. Fachtexte lassen selbstverständliche Zwischenschritte aus und setzen umfangreiches Vorwissen voraus. Ein Beweisassistent verlangt dagegen eine vollständig geschlossene logische Kette.
Prove2Me löst das Koordinationsproblem
Die ersten Versuche mit mehreren Claude-Agenten scheiterten laut Anthropic nicht an einzelnen mathematischen Aufgaben. Die Agenten verloren den Überblick über den Projektzustand und arbeiteten zunehmend ineffizient zusammen. Der Durchbruch gelang erst mit der spezialisierten Steuerungsplattform Prove2Me.
Prove2Me organisiert Aussagen und Abhängigkeiten in einem gerichteten azyklischen Graphen. Dadurch lässt sich erkennen, welche Zwischentheoreme bereits verfügbar sind und welche Aufgaben als Nächstes parallel bearbeitet werden können. Die Plattform wirkt damit dem Kontextverlust einzelner Agenten entgegen.
Der Fall bestätigt ein Muster, das auch bei anderen komplexen KI-Systemen sichtbar wird. Die Qualität hängt nicht nur vom Basismodell ab, sondern mindestens ebenso stark von Werkzeugen, Kontextverwaltung und Prüfmechanismen. Eine ähnliche Bedeutung der umgebenden Infrastruktur zeigt sich bei der Frage, warum ein KI-Harness wichtiger als die reine Modellwahl sein kann.
Hoher Tokenverbrauch bleibt ein Kostenrisiko
Rund sechs Milliarden Output-Token sind auch für ein außergewöhnliches Forschungsprojekt eine erhebliche Menge. Die daraus abgeleitete Kostenspanne von 100.000 bis 300.000 US-Dollar ist lediglich eine Schätzung. Anthropic hat keine exakten Gesamtkosten veröffentlicht.
Ein kleineres Nebenexperiment deutet an, dass formale Verifikation nicht zwangsläufig solche Dimensionen erreichen muss. Dabei formalisierten Agenten den Drei-Primzahlen-Satz von Winogradow innerhalb von drei Tagen mit drei privaten Claude-Max-Abos. Wie sich der Aufwand auf industrielle Projekte übertragen lässt, bleibt offen.
Für Unternehmen wird deshalb eine belastbare Kostenkontrolle entscheidend. Ansätze wie das Modell-Routing zur Senkung des Tokenverbrauchs können bei wiederkehrenden Teilaufgaben relevant werden. Bei formalen Beweisen darf eine günstigere Modellauswahl jedoch nicht zulasten der nachvollziehbaren Prüfung gehen.
Relevanz für Software und Compliance im DACH-Raum
Ein unmittelbarer Bezug zu Unternehmen im DACH-Raum besteht nicht. Das Projekt demonstriert aber, wie KI-Agenten umfangreiche Logikketten in eine maschinell prüfbare Form überführen können. Denkbare Einsatzgebiete liegen bei hochkritischer Software, Sicherheitsregeln und komplexen Compliance-Vorgaben.
Formal verifizierte Eigenentwicklungen könnten langfristig eine belastbarere Alternative zu schwer kontrollierbaren Standardlösungen und dauerhaften Software-Abos schaffen. Dafür braucht es neben dem Sprachmodell eine eigene Orchestrierungs-, Test- und Freigabeinfrastruktur. Wie aufwendig die Anpassung von Prove2Me an industrielle Softwareprojekte wäre, ist bislang nicht belegt.
Auch eine erfolgreiche formale Prüfung hebt organisatorische Verantwortung nicht auf. Das gilt ebenso für KI-generierten Programmcode, bei dem etwa Debian die Verantwortung weiterhin bei den Entwicklern sieht. Entscheidend bleibt, ob Anforderungen, Ausgangsannahmen und geprüfte Spezifikationen tatsächlich das gewünschte Verhalten abbilden.