Fermat's letzter Satz in Lean 4 vollständig maschinengeprüft
Fermat's Last Theorem in Lean 4
Anthropic hat einen vollständigen, maschinengeprüften Beweis von Fermats letztem Satz in Lean 4 veröffentlicht. Der Beweis folgt dem klassischen Argument von Frey, Serre, Ribet, Wiles und Taylor-Wiles und basiert auf Mathlib. Er wurde mit Lean 4.33.1 erstellt und von zwei unabhängigen Kernen verifiziert: dem Lean-Kernel selbst und nanoda, einem in Rust geschriebenen Kernel. Das Repository enthält auch eine durchsuchbare HTML-Dokumentation des Beweises. Der Beweis ist ein Forschungsartefakt und wird nicht weiter gepflegt.
Zusammen etablieren diese Prüfungen, dass die obige Aussage aus den drei Axiomen folgt, vorausgesetzt man vertraut dem Lean-Kernel (oder nanoda) und den Prüfwerkzeugen.