Anthropic: KI-Modell Claude beweist Fermats letzten Satz

Anthropic gab am Donnerstag bekannt, dass sein KI-Modell Claude den ersten durchgängigen, computergestützten Beweis für den Großen Fermatschen Satz erbracht hat, eines der berühmtesten Probleme der Mathematik. Claude arbeitete über 11 Tage weitgehend autonom, schrieb den Beweis in der Programmiersprache Lean und erzeugte dabei 13 Millionen Codezeilen sowie 29.500 Zwischenbeweise.anthropic+1

Ein 11-Tage-Sprint durch Jahrhunderte der Mathematik

Der Große Fermatsche Satz besagt, dass es für keine ganze Zahl n größer als 2 positive ganze Zahlen a, b und c gibt, die die Gleichung aⁿ + bⁿ = cⁿ erfüllen. Die Vermutung wurde erstmals um 1637 von Pierre de Fermat aufgestellt und erst 1995 bewiesen, als Andrew Wiles einen 129-seitigen Beweis vorlegte, dessen Überprüfung durch Experten Monate dauerte.anthropic

Die Formalisierung dieses Beweises – also die Umschreibung in eine für Computer prüfbare Form – sollte eigentlich Jahre dauern. Kevin Buzzard, Mathematiker am Imperial College London, der ein unabhängiges Projekt zur Formalisierung des Satzes mit Lean leitet, bestätigte, dass der Code kompiliert und korrekt ist. In einem Blogbeitrag am Freitag nannte Buzzard es eine "außergewöhnliche Leistung der Auto-Formalisierung" und merkte an, dass der Beweis "mehrschichtig" sei und Algebra, harmonische Analysis, Geometrie sowie Zahlentheorie umfasse.xenaproject.wordpress+1

Claudes Beweis folgt der Darmon-Diamond-Taylor-Darstellung des Wiles-Taylor-Wiles-Arguments, einer vereinfachten Version des ursprünglichen Beweises. Menschliche Eingriffe beschränkten sich auf gelegentliche Anweisungen des Anthropic-Forschers Tianyi Peng, dessen Team an der Columbia University die Plattform Prove2Me entwickelte, die dieses Unterfangen erst ermöglichte.anthropic+1

Wie der Beweis entstand

Mehrere frühe Versuche scheiterten, da die Agenten von Claude den Überblick über den Projektstatus verloren und die Zusammenarbeit abbrach. Der Durchbruch gelang durch den Wechsel zu Prove2Me, einer offenen Plattform, die einen gerichteten Graphen von Theoremen verwaltet. Dies ermöglichte es mehreren Agenten, parallel zu arbeiten und zu entscheiden, welche Beweise als Nächstes angegangen werden sollten. Unter Verwendung eines auf Claude Code basierenden Multi-Agenten-Systems verbrauchten Dutzende Agenten etwa sechs Milliarden Output-Token eines internen Forschungsmodells, das Anthropic als vergleichbar mit Claude Fable 5.1 beschreibt.siliconangle+1

Der fertige Beweis wurde von Lean unter Verwendung seiner drei Standardaxiome verifiziert; ein Vergleich bestätigte zudem, dass die Theorem-Formulierung mit der von Mathlib übereinstimmt. Mit 13 Millionen Zeilen ist er mehr als fünfmal so umfangreich wie Mathlib, die wichtigste Gemeinschaftsbibliothek für formalisierte Mathematik.anthropic+1

Was dies für die Mathematik bedeutet

Buzzard, der die Nachricht über das Ergebnis zunächst für einen Scherz hielt, während er auf einem Musikfestival war, schrieb, dass dieser Erfolg eine neue Ära einläute: "Wenn die automatische Formalisierung des Fermatschen Satzes jetzt möglich ist, dann haben wir einen großen Schritt in Richtung automatischer Formalisierung der modernen mathematischen Literatur gemacht". Er merkte an, dass solche Techniken Fehler im bestehenden mathematischen Korpus aufdecken und Gutachter bei der Prüfung neuer Arbeiten entlasten könnten.anthropic+1

Der Meilenstein folgt auf eine Reihe KI-gestützter Fortschritte in der Mathematik. Anthropic nutzte Claude im letzten Monat, um neue Erkenntnisse über die Riemannsche Zeta-Funktion zu gewinnen, während der Konkurrent OpenAI sein neuestes Modell einsetzte, um mehrere Erdős-Probleme zu lösen. Anthropic verwendete Claude zudem kürzlich, um die Jakobische Vermutung in drei und mehr Dimensionen zu widerlegen. Buzzard äußerte sich dazu gewohnt trocken: "Ich habe 1 Million Pfund erhalten, um mein Projekt über 5 Jahre zu leiten; Anthropic brauchte nur 11 Tage, aber ich frage mich, ob sie mehr Geld ausgegeben haben".xenaproject.wordpress+2