Anthropics KI-Modell Claude hat einen der berühmtesten mathematischen Beweise erstmals vollständig in eine Form übertragen, die ein Computer automatisch überprüfen kann. Dafür zerlegte die KI den Beweis von »Fermats letztem Satz« in Zehntausende Einzelschritte und schrieb rund 13 Millionen Zeilen Lean-Code.
Einen neuen mathematischen Beweis hat Claude dabei nicht entdeckt. Die eigentliche Leistung liegt in der Formalisierung. Eine Aufgabe, für die Mathematiker mit Jahren gerechnet hatten, erledigte das KI-System weitgehend autonom in nur elf Tagen.
13 Millionen Zeilen Lean-Code
Fermats letzter Satz wurde bereits 1995 von Andrew Wiles bewiesen. Claude orientierte sich an einer vereinfachten Darstellung dieses Beweises von Henri Darmon, Fred Diamond und Richard Taylor.
Der Unterschied zu einem normalen mathematischen Beweis: Menschen lassen viele offensichtliche Zwischenschritte aus. Ein Beweisassistent wie Lean verlangt dagegen jeden einzelnen logischen Schritt.
Claude erzeugte dafür rund 13 Millionen Zeilen Lean-Code und bewies mehr als 30.000 Zwischentheoreme. Rund 29.500 davon flossen in den finalen Beweis ein. Dutzende Claude-Agenten arbeiteten parallel an unterschiedlichen Teilproblemen.
Anzeige
Plattform koordinierte die Agenten
Anfangs scheiterten mehrere Versuche, weil die Agenten den Überblick über den Projektstatus verloren. Der Durchbruch gelang mit der Plattform Prove2Me.
Sie organisiert die offenen Theoreme in einem gerichteten Graphen und ermöglicht es den Agenten, parallel zu arbeiten und bereits gelöste Ergebnisse wiederzuverwenden.
Das Projekt verbrauchte rund sechs Milliarden Output-Token. Anthropic nennt weder die Kosten noch ein konkretes öffentliches Claude-Modell. Zum Einsatz kam ein internes Forschungsmodell, dessen Leistung ungefähr Claude Fable 5.1 entsprechen soll.
Das Besondere ist damit nicht ein neuer Beweis für Fermats letzten Satz, sondern die Geschwindigkeit der automatischen Formalisierung.
Solche maschinenlesbaren Beweise könnten künftig die Überprüfung mathematischer Forschung deutlich vereinfachen. Statt komplexe Argumentationen monatelang manuell zu kontrollieren, kann eine Sprache wie Lean jeden logischen Schritt automatisch prüfen.
