Anthropic zufolge: Fermats letzter Satz in Lean formalisiert

Der entscheidende Moment dieses Fermat-Projekts ist unspektakulär: In Lean kompiliert ein Beweis – oder er tut es nicht. Im GitHub-Repository von Anthropic liegt nach Angaben des Unternehmens nun eine vollständig computergeprüfte Fassung von Fermats letztem Satz. Der Mathematiker Kevin Buzzard hat den Code inzwischen selbst kompiliert und den zugehörigen Komparator ausgeführt.

Mathematisch ist der Satz nicht neu. Andrew Wiles bewies 1995 auf 129 Seiten, dass die Gleichung xⁿ + yⁿ = zⁿ für ganzzahlige Exponenten n > 2 keine ganzzahligen Lösungen hat. Neu ist die Formalisierung: Der Beweis wird so in Code übersetzt, dass ein Computer jeden einzelnen Schritt kontrollieren kann, statt sich auf übersprungene, für Menschen offensichtliche Zwischenschritte zu verlassen.

Lean ist dabei Programmiersprache und Prüfsystem zugleich. Mathematische Aussagen und ihre Herleitungen werden gegen ein festes logisches Regelwerk geprüft; wenn auch nur eine Lücke bleibt, kompiliert der Beweis nicht. Vertrauen muss dann vor allem dem kleinen Kern von Lean und seinen Axiomen gelten. Die verfügbare Bibliothek Mathlib begrenzt den Spielraum allerdings auf den Teil der Mathematik, der bereits formalisiert wurde.

Anthropic zufolge arbeiteten Dutzende Claude-Agenten elf Tage lang an einer vereinfachten Fassung von Wiles’ Beweis nach Darmon, Diamond und Taylor. Heraus kamen 13 Millionen Zeilen Lean-Code und rund 29.500 Zwischentheoreme. Erste Teams scheiterten laut dem Unternehmen am Projektüberblick; vorangekommen sei die Arbeit erst mit Prove2Me, einer von Tianyi Pengs Gruppe an der Columbia University entwickelten Plattform, die nächste Beweisschritte in einem gerichteten azyklischen Graphen verwaltet. Der Aufwand lag laut Anthropic bei rund sechs Milliarden Output-Token; daraus lassen sich Kosten zwischen 100.000 und 300.000 US-Dollar hochrechnen.

Konkret ändert sich damit schon jetzt etwas für die Formalisierung mathematischer Literatur: Dritte können den offengelegten Code kompilieren und die logische Kette prüfen. Das schafft eine technisch reproduzierbare Kontrolle, ersetzt aber keine unabhängige Bewertung, die bislang weitgehend aussteht. Buzzard hält die Formalisierung für einen großen Schritt hin zur automatischen Formalisierung moderner Mathematik; zugleich folgt sie der frühen Literatur und liefert keine neue mathematische Aussage über Fermats letzten Satz.