Anthropic: Claude formalisiert Fermat-Beweis in Lean

Hinweis: Aussagen, die Anthropic als Unternehmen betreffen, sind als Herstellerangaben gekennzeichnet.

Anthropic: Claude formalisiert Fermat-Beweis in Lean

Anthropic gibt an, eine computergeprüfte Formalisierung des Fermatschen Letzten Satzes erstellt zu haben [Herstellerangabe]. Das Sprachmodell Claude habe den Beweis in der Programmiersprache Lean geschrieben und dabei weitgehend autonom über elf Tage gearbeitet, teilt das Unternehmen in einem Blogbeitrag mit [Herstellerangabe]. Anthropic bezeichnet das Ergebnis als erste vollständige computergeprüfte Formalisierung des Satzes [Herstellerangabe].

Eine computergeprüfte Formalisierung bedeutet, dass der mathematische Beweis in eine formale Sprache übersetzt wird, die ein Computerprogramm – hier der Lean-Kernel – Schritt für Schritt auf logische Korrektheit prüfen kann. Dafür müssen die oft knappen Argumente der mathematischen Literatur in detaillierte, lückenlose Einzelschritte zerlegt werden. Fehlende Zwischenschritte, die für menschliche Leser selbstverständlich sind, müssen explizit ergänzt und alle verwendeten Begriffe formal definiert werden.

Claude erhielt den Auftrag, den Beweis zu formalisieren, und arbeitete dann weitgehend selbstständig: Das Modell generierte Lean-Code, ließ ihn vom Beweisassistenten prüfen, analysierte Fehlermeldungen und passte die Formalisierung iterativ an. Ein menschlicher Forscher gab die Zielrichtung vor und überwachte den Fortschritt, griff aber nur bei Bedarf ein. Der Satz besagt, dass es keine positiven ganzen Zahlen a, b, c gibt, die für einen Exponenten n größer als 2 die Gleichung a^n + b^n = c^n erfüllen. Der erste Beweis stammt von Andrew Wiles aus dem Jahr 1995 und umfasst 129 Seiten. Die Formalisierung folgt dem Frey-Kurven- und Modularity-Lifting-Ansatz, der auf Wiles und Taylor zurückgeht.

13 Millionen Zeilen, 29.511 Theoreme, Kernel-verifiziert

Der formalisierte Beweis umfasst nach Angaben von Anthropic 13 Millionen Zeilen Lean-Code [Herstellerangabe]. Nach Angaben von Anthropic handelt es sich um die größte Datei ihrer Art [Herstellerangabe]. Die Formalisierung deckt über 29.511 Theoreme und 1.450 Definitionen ab. Verifiziert wurde sie durch den Kernel von Lean, ohne Axiome außerhalb der Standard-Grundlagen der Mathlib-Bibliothek zu verwenden. Das bedeutet, dass jede logische Folgerung von der Kernkomponente des Beweisassistenten geprüft wurde und keine zusätzlichen, unbewiesenen Annahmen einflossen.

Die enorme Code-Menge ist notwendig, weil der ursprüngliche Beweis von Wiles zahlreiche Teilgebiete der Mathematik heranzieht und in der Literatur viele Schritte nur angedeutet oder als bekannt vorausgesetzt werden. Für die maschinelle Prüfung muss jede noch so kleine Folgerung als eigener Schritt kodiert werden; zudem müssen alle verwendeten mathematischen Objekte, Hilfssätze und Definitionen formal ausformuliert und bewiesen werden. Dadurch wächst der Umfang im Vergleich zum menschenlesbaren Beweis um ein Vielfaches.

Buzzards Community-Projekt bleibt parallel aktiv

Parallel zu der Arbeit von Anthropic existiert ein laufendes, von Kevin Buzzard geleitetes Open-Source-Projekt zur Formalisierung des Fermatschen Letzten Satzes in Lean. Es verfolgt eine moderne Variante des Wiles/Taylor-Wiles-Beweises und baut auf Ideen von Khare und Wintenberger auf. Das Projekt ist als mehrjähriges, von Menschen getragenes Vorhaben angelegt und nutzt eine detaillierte Blaupause (Blueprint), die den Beweis in Teilziele zerlegt und die Formalisierung schrittweise vorantreibt. Im Gegensatz zu Anthropics Ansatz, bei dem ein KI-Modell weitgehend autonom arbeitete, wird hier die Formalisierung von einer Gemeinschaft von Mathematikern koordiniert und kontinuierlich weiterentwickelt. Der aktuelle Stand ist, dass das Projekt noch nicht abgeschlossen ist, aber aktiv Fortschritte macht. Der ursprüngliche Beweis von Wiles aus dem Jahr 1995 umfasste 129 Seiten und benötigte monatelange Prüfung.