Anthropic hat ein Repositorium mit einem formalen Beweis des Großen Fermatschen Satzes veröffentlicht. Dutzende Claude-Agenten übertrugen eine Variante des klassischen Arguments von Wiles, Taylor und weiteren Mathematikern in Lean, wo jeder logische Schritt maschinell geprüft wird. Laut Unternehmen dauerte das elf Tage, erzeugte rund 13 Millionen Zeilen und nutzte im finalen Zweig etwa 29.500 Hilfssätze.

Der Begriff „Beweis“ darf nicht überhöht werden. Claude entdeckte keine neue Lösung für das seit den 1990er-Jahren gelöste Problem. Neu ist die vollständige maschinenprüfbare Übersetzung eines großen Stücks moderner Mathematik. Sie baut auf jahrelanger Arbeit von Lean, Mathlib und Kevin Buzzards Projekt auf; seine positive Fachprüfung ist wichtig, eine breitere unabhängige Kontrolle des riesigen Artefakts beginnt jedoch erst.

Erfolgreich wurden die Agenten erst mit Prove2Me. Die Plattform zerlegte das Ziel in einen Graphen kleinerer Sätze, hielt den Projektzustand fest und erleichterte Wiederverwendung. Das Ergebnis zeigt daher neben Modellleistung auch den Wert von Orchestrierung, Bibliotheken und menschlich vorbereiteten Grundlagen. Das Repositorium ist unter Apache 2.0 öffentlich verfügbar.

Wenn sich die Methode übertragen lässt, könnte sie Fachartikel in prüfbare Form bringen, verborgene Lücken finden und die wachsende Menge KI-gestützter Mathematik kontrollieren helfen. Formale Zertifikate könnten später Ergebnisse in Kryptografie, Chipverifikation oder sicherheitskritischer Software begleiten. Verständliche Erklärungen und menschliche Urteile über die Voraussetzungen ersetzen sie nicht.

Für die Praxis müssen Codeumfang und Rechenbedarf stark sinken, unabhängige Werkzeuge die Prüfung reproduzieren und neue Beweise ohne so reiche Infrastruktur gelingen. Optimistisch sind in 1–3 Jahren nützliche Assistenten für Formalisierungsteams und in 3–7 Jahren formale Anhänge bei einem Teil der Fachartikel denkbar. Die routinemäßige Prüfung des Großteils neuer Mathematik liegt weiter entfernt und ist seriös nicht zu datieren.