FROM INTUITION TO RESEARCH
Drei Verständnisebenen
01 · Das Problem verstehen
Für n größer als zwei gibt es keine positiven ganzen a, b, c mit aⁿ + bⁿ = cⁿ. Der Satz war bereits bewiesen; Claude formalisierte ihn.
02 · Den Beitrag verstehen
Anthropic berichtet über eine vollständige Lean-Formalisation in elf Tagen; Kevin Buzzard kommentierte das Artefakt.
03 · Akademische Einordnung
Dies ist eine Autoformalisierung, keine neue Lösung eines offenen Problems. Der Lean-Kernel prüft Beweisterme relativ zu Axiomen und Definitionen.
Mögliche Auswirkungen
Weniger manueller Aufwand bei der Überprüfung langer Beweise.
Was NICHT bewiesen ist
Der Satz wurde bereits von Andrew Wiles bewiesen.