Lean akzeptiert Fermat-Beweis mit 10.5 Millionen Zeilen

Lean, eine weltweit von Mathematikern eingesetzte Software zur formalen Prüfung von Beweisen, hat eine vollständige Fassung des Großen Fermatschen Satzes akzeptiert. Die von Anthropics Claude-System erstellte und in einem offenen Repository veröffentlichte Formalisierung enthält weder ungelöste Platzhalter noch zusätzliche Axiome oder rechnerische Abkürzungen außerhalb der Standardgrundlagen von Lean (Repository). Kevin Buzzard, Mathematiker am Imperial College London und Leiter eines eigenen Formalisierungsprojekts, kompilierte das Projekt unabhängig und bestätigte die Gültigkeit. Er sprach von einer „außergewöhnlichen Leistung auf dem Gebiet der automatisierten Formalisierung“ (Buzzard).

Die mathematische Frage selbst ist seit Langem geklärt: Andrew Wiles bewies den Satz 1995, und unter Fachleuten bestanden keine ernsthaften Zweifel an seiner Richtigkeit. Ausständig war die Übertragung des Beweises in Anweisungen für ein strikt regelgebundenes Prüfprogramm, dem jede Definition und jeder Zwischenschritt ausdrücklich vorgegeben werden muss, den ein Mathematiker stillschweigend voraussetzen kann. Nach Angaben von Anthropic erledigten Dutzende KI-Agenten diese Arbeit im August innerhalb von elf Tagen. Sie arbeiteten parallel über eine Plattform namens Prove2Me (Anthropic).

Diese Zeitangabe beschreibt allerdings einen Prozess, den Außenstehende nicht nachvollziehen können, weil weder das interne Modell und die Steuerungsinfrastruktur noch die Eingriffe der Bediener und der Rechenaufwand offengelegt wurden. Reproduzierbar ist allein das Ergebnis: Wer über ausreichende Hardware verfügt, kann das Lean-Projekt selbst kompilieren und prüfen. Ein von Anthropic in Rust entwickeltes zweites Prüfprogramm untersuchte dasselbe formale Werk und bestätigte die Konsistenz aller 1.052.234 Deklarationen (technischer Bericht). Damit liegt eine zweite Prüfung desselben Textes vor, keine unabhängige Wiederholung der elftägigen Erstellung.

Wie die Agenten arbeiteten

Bei der Formalisierung wird ein mathematisches Argument so umgeschrieben, dass ein Programm ohne mathematische Intuition jeden logischen Schritt kontrollieren kann. Der Satz selbst klingt einfacher, als sein Beweis ist: Für jeden ganzzahligen Exponenten ab drei gibt es keine drei positiven ganzen Zahlen, die die Gleichung aⁿ + bⁿ = cⁿ erfüllen. Der Beweis führt dagegen über Hunderte Seiten und durch mehrere anspruchsvolle Gebiete der Zahlentheorie.

Claude entdeckte dabei keine neue Mathematik, sondern formalisierte die bekannte Beweiskette, die zu Wiles’ Ergebnis führt. Als Grundlage diente eine Darstellung der Mathematiker Henri Darmon, Fred Diamond und Richard Taylor (Anthropic, technischer Bericht). Die schöpferische mathematische Leistung stammt von Wiles und seinen Vorgängern; Claude übertrug deren Erkenntnisse in rund 10,5 Millionen Zeilen maschinenprüfbaren Code (technischer Bericht).

Die vom Anthropic-Forscher Tianyi Peng und Mitarbeitern der Columbia University entwickelte Plattform Prove2Me zerlegte den Beweis in einen Abhängigkeitsgraphen mit etwa 29.511 eigenständigen Aussagen (technischer Bericht). Die Agenten wählten jeweils Aussagen aus, deren Voraussetzungen bereits erfüllt waren, verfassten dafür Lean-Beweise und kontrollierten gegenseitig ihre Formulierungen. Durch diese Arbeitsteilung konnten viele Aufgaben gleichzeitig bearbeitet werden; insgesamt erzeugte das interne Forschungsmodell rund sechs Milliarden Ausgabetokens (technischer Bericht).

Während des Durchlaufs hätten die menschlichen Bediener keinen Lean-Code geschrieben, erklärt Anthropic. Sie hätten allerdings den Satz und den bekannten Beweisweg ausgewählt, die Agenteninfrastruktur entwickelt und gelegentlich die Prioritäten angepasst (Anthropic). Das vollständige Protokoll dieser Eingriffe und die Rechenkosten veröffentlichte das Unternehmen nicht.

Aufbauend auf jahrelanger menschlicher Vorarbeit

Das Ergebnis stützt sich auf Mathlib, die umfangreiche, gemeinschaftlich gepflegte Bibliothek formalisierter Mathematik, sowie unmittelbar auf zwei ältere Vorhaben. Buzzards Team am Imperial College arbeitet seit Ende 2023 an einer Lean-Formalisierung des Großen Fermatschen Satzes; das bis 2029 geplante Projekt wird vom EPSRC mit 1 Mio. GBP gefördert (EPSRC-Förderung). Ein weiteres Gemeinschaftsprojekt hatte den Satz bereits für eine Teilmenge der Fälle formalisiert. Anthropics Herkunftsnachweis nennt 106 Dateien, die Material aus diesen Arbeiten übernehmen oder anpassen (Herkunftsnachweis).

Wegen der parallelen Bearbeitung lassen sich die elf Kalendertage nicht sinnvoll mit den Arbeitsstunden von Buzzards Team vergleichen, das beim Beginn der Claude-Kampagne seit etwa 22 geförderten Monaten tätig war (EPSRC-Förderung). Angaben zu den eingesetzten GPU-Stunden oder zum Energieverbrauch machte Anthropic nicht.

Vor dieser Veröffentlichung war der Große Fermatsche Satz der letzte noch nicht formalisierte Eintrag auf Freek Wiedijks Liste von 100 bedeutenden mathematischen Sätzen. Die seit zwei Jahrzehnten geführte Liste dient als Maßstab für den Fortschritt der formalen Mathematik (Buzzard).

Ob sich das Verfahren verallgemeinern lässt, dürfte sich erst bei neuerer, schlechter dokumentierter Mathematik zeigen, für die weder ein ausgearbeiteter Beweisplan noch ausgereifte Bibliotheken oder formale Vorarbeiten existieren. Hier ging es um einen berühmten Satz, für dessen Formalisierung bereits erhebliche Infrastruktur vorhanden war. Das Projekt belegt somit, dass KI-Agenten auf Grundlage eines bekannten Beweiswegs und menschlicher Vorarbeiten eine vollständige, von Lean akzeptierte und extern überprüfbare Formalisierung erstellen können. Ob sich auch die Erstellung selbst wiederholen ließe, bleibt mangels veröffentlichter Angaben offen.