Anthropic formalisiert Fermats letzten Satz mit Claude in Lean

Claude erzeugte dafür rund 13 Millionen Zeilen Lean-Code und bewies 29.500 Zwischentheoreme, die in den finalen Beweis eingingen. Der Beweisassistent Lean prüfte das Ergebnis anhand seiner drei Standardaxiome.

Fermats letzter Satz gilt seit 1995 als bewiesen. Anthropic hat ihn also nicht neu gelöst, sondern in eine Form übersetzt, die ein Computersystem vollständig kontrollieren kann. Genau darin liegt die Bedeutung: KI könnte mathematische Arbeiten künftig schneller und verlässlicher überprüfbar machen.

Der Mathematiker Kevin Buzzard begutachtete den Beweis und bezeichnete die Arbeit als bedeutenden Schritt für die automatisierte Formalisierung moderner Mathematik. Der große Durchbruch ist damit weniger ein neuer mathematischer Gedanke als eine belastbare digitale Kontrolle vorhandener Beweise.