Article
Claude formalisiert Fermats Letzten Satz: 13 Millionen Zeilen Lean in 11 Tagen
Fermats Letzter Satz hat Geschichte: Pierre de Fermat notierte die Behauptung um 1637, Andrew Wiles lieferte 1995 den ersten Beweis - 129 Seiten, monatelange Prüfung, ein Fehler mit einjährigem Reparaturaufwand. Jetzt hat Anthropic den ersten vollständig computerpruefbaren Beweis veröffentlicht. Claude arbeitete großteils autonom 11 Tage, schrieb 13 Millionen Zeilen Lean und bewies 30.300 Sätze, von denen 29.500 im finalen Beweis landen. Das Ergebnis ist mehr als fünfmal so groß wie Mathlib, die große Community-Bibliothek.
Der interessante Teil ist die Infrastruktur: Zuerst scheiterten die Agents - sie verloren den Projektzustand und arbeiteten nicht mehr zusammen. Der Durchbruch kam mit Prove2Me, einer offenen Plattform von Columbia-Forscher Tianyi Peng: Ein DAG aus Sätzen zeigt jedem Agent, was als nächstes bewertet werden sollte und puffert Memory-Degradation ab. Die Trennung von Sätzen und Beweisen in verschiedenen Dateien beschleunigt die Lean-Kompilation, und natuerlichsprachliche Beschreibungen ermöglichen Wiederverwendung. Menschlicher Input war minimal - Hinweise wie “Jacobian als Scheme klingt hochprioritaet”.
Lean prüfte den Beweis mit nur den drei Standardaxiomen, ein Komparator bestätigt die Übereinstimmung mit Mathlib. Kevin Buzzard reviewte das Ergebnis und sieht darin einen großen Schritt zur Autoformalisierung der modernen Mathematik - inklusive der Möglichkeit, KI-generierte Mathematik künftig maschinell zu verifizieren. Nebenbei: Drei private Claude-Max-Abos formalisierten in einem Nebentest Vinogradovs Dreiprimzahlensatz in drei Tagen.