Fermats letzter Satz gehört zu den bekanntesten Geschichten der Mathematik. Andrew Wiles bewies ihn in den 1990er-Jahren nach Jahrhunderten erfolgloser Versuche. Jetzt sorgt derselbe Satz wieder für Aufmerksamkeit — diesmal nicht wegen eines neuen mathematischen Durchbruchs, sondern weil ein KI-gestütztes Projekt den bestehenden Beweis in eine Form übertragen hat, die ein Computer Schritt für Schritt prüfen kann.
Berichten zufolge entstand dabei eine Lean-Formalisierung mit rund 13 Millionen Codezeilen innerhalb von elf Tagen. Science Official hat das Projekt eingeordnet: Die KI hat Fermats letzten Satz nicht neu bewiesen. Sie hat die bekannte Beweisarchitektur in die formale Sprache eines Proof Assistants übersetzt.
Warum braucht das Millionen Zeilen, wenn ein mathematischer Beweis auf Papier viel kürzer wirkt? Menschen lassen beim Schreiben ständig Dinge weg, die Fachleute als selbstverständlich ansehen. Begriffe sind aus dem Kontext bekannt, kleine Zwischenschritte werden übersprungen und ein Satz wie „daraus folgt“ kann im Hintergrund viele einzelne logische Operationen enthalten. Ein Beweisassistent akzeptiert solche Abkürzungen nicht.
Lean verlangt explizite Definitionen und überprüft, ob jeder Schritt nach den hinterlegten Regeln wirklich aus den vorherigen folgt. Dafür müssen ganze Bibliotheken aus Algebra, Zahlentheorie und Geometrie verfügbar sein. KI kann bei dieser Arbeit helfen, indem sie passende Lemmas findet, Formalisierungen vorschlägt und Routineaufgaben automatisiert.
Das macht formale Mathematik interessant für die aktuelle KI-Debatte. Es geht nicht darum, ob ein Chatbot eine hübsche Antwort formulieren kann, sondern ob ein System über eine sehr lange Kette präziser logischer Abhängigkeiten hinweg zuverlässig arbeitet. Fehler lassen sich dabei nicht einfach mit überzeugender Sprache verdecken: Am Ende entscheidet der Proof Assistant, ob die formale Ableitung gültig ist.
Trotzdem bleibt menschliche Arbeit zentral. Menschen legen fest, welches mathematische Ziel formalisiert wird, welche Bibliotheken verwendet werden und ob die formale Aussage tatsächlich dem Theorem entspricht, das man überprüfen möchte. Eine perfekte Prüfung des falschen oder zu schwachen Satzes wäre mathematisch wenig wert.
Die eigentliche Veränderung könnte deshalb in der Infrastruktur liegen. Wenn KI große Teile mathematischer Literatur schneller in maschinenlesbare, geprüfte Bibliotheken überführt, könnten neue Forschende auf einem wesentlich dichter verifizierten Fundament aufbauen. Fermats letzter Satz bleibt der Beweis von Wiles. Neu ist die Geschwindigkeit, mit der dieser riesige menschliche Gedankengang in eine Sprache übersetzt wurde, die ein Computer ohne Vertrauen in Abkürzungen nachrechnen kann.