// HEISE ONLINE — INTELLIGENZA ARTIFICIALE
13 Millionen Zeilen Code: KI verifiziert Beweis von Fermats letztem Satz
Anthropic hat nach eigenen Angaben erstmals eine vollständig computerverifizierte Fassung von Fermats letztem Satz vorgelegt – erstellt von Claude-Agenten.
Pierre de Fermats berühmte Anmerkung im der 1670 von seinem Sohn Clément-Samuel veröffentlichten „Arithmetica des Diophantos“. „Es ist unmöglich, einen Kubus in zwei Kuben, ein Biquadrat (vierte Potenz) in zwei Biquadrate oder allgemein irgendeine Potenz größer als die zweite in zwei Potenzen desselben Grades zu zerlegen“. Er fügt hinzu, er habe dafür einen wahrhaft wunderbaren Beweis gefunden, doch der Rand der Seite sei zu schmal, um ihn zu fassen („Hanc marginis exiguitas non caperet“).
This article is also available in
English.
It was translated with technical assistance and editorially reviewed before publication.
Bewiesen ist Fermats letzter Satz seit 1995, doch nun hat das KI-Unternehmen Anthropic nach eigenen Angaben erstmals eine vollständig computerverifizierte Fassung dieses Beweises vorgelegt. Ein Schwarm von Claude-Agenten soll sie in elf Tagen im Beweisassistenten Lean geschrieben haben: 13 Millionen Zeilen Code, 29.500 Zwischentheoreme. Die Fachwelt hatte dafür Jahre veranschlagt. Der Code liegt offen, eine unabhängige Bewertung steht weitgehend aus.
Es geht hier ausdrücklich nicht um neue Mathematik. Fermats letzter Satz – die Gleichung xⁿ + yⁿ = zⁿ hat für ganzzahlige Exponenten n > 2 keine ganzzahligen Lösungen – wurde 1995 von Andrew Wiles auf 129 Seiten bewiesen und gilt in der Fachwelt seither als gesichert. Was fehlte, war die Formalisierung: die Übersetzung dieses Beweises in eine Form, die ein Computer Schritt für Schritt automatisch nachprüfen kann. Genau das soll Claude nun geleistet haben, wie Anthropic in einem Beitrag zur Formalisierung von Fermats letztem Satz schreibt.
Werkzeug der Wahl war wie schon bei früheren KI-Beweisen der Beweisautomat Lean. Dabei handelt es sich um eine Programmiersprache und ein Prüfsystem in einem. Mathematische Aussagen und ihre Herleitungen werden als Code notiert, den Lean anschließend gegen ein festes logisches Regelwerk prüft. Geht die Kette nicht lückenlos auf, kompiliert der Beweis schlicht nicht. Vertrauen muss man am Ende nur noch dem kleinen Kern des Systems und dessen Axiomen – nicht mehr der Sorgfalt einzelner Gutachter.
Der Aufwand dafür ist allerdings enorm: Ein für Menschen geschriebener Beweis überspringt viele als offensichtlich geltende Schritte und baut auf Jahrhunderten publizierter Arbeit auf. Lean muss jeden einzelnen Schritt sehen, egal wie trivial, und kann dabei nur auf den vergleichsweise winzigen Teil der Mathematik zurückgreifen, der bereits formalisiert vorliegt. Gesammelt ist dieser Bestand in Mathlib, der zentralen Community-Bibliothek formalisierter Mathematik.
Der Anthropic-Forscher Tianyi Peng, dessen Gruppe an der Columbia University Werkzeuge für KI-gestützte Formalisierung entwickelt, wollte prüfen, ob Claude beim Formalisieren von Fermats letztem Satz (Fermat’s Last Theorem, FLT) überhaupt Fortschritte macht. Das Ergebnis habe die Erwartungen übertroffen: In elf Tagen habe Claude weitgehend autonom die erste durchgängige, computergeprüfte Fassung produziert. Herausgekommen seien 13 Millionen Zeilen Lean-Code und rund 29.500 Zwischentheoreme. Dutzende Claude-Agenten hätten dabei zusammengearbeitet, um Konzepte zu definieren, Zwischentheoreme zu beweisen und damit immer schwierigere Aussagen zu belegen.
Formalisiert wurde nach diesen Angaben eine vereinfachte Fassung von Wiles’ Beweis nach Darmon, Diamond und Taylor. Menschlicher Input habe sich auf gelegentliche High-Level-Anweisungen Pengs beschränkt.
Nach Anthropics Darstellung wurde das Ergebnis von Lean geprüft und nutzt nur Leans drei Standardaxiome, und ein Komparator bestätigte, dass die Theorem-Aussage mit Mathlibs eigener FLT-Formulierung übereinstimmt. Der vollständige Beweis liegt samt schriftlichem Walkthrough im GitHub-Repository von Anthropic. Ob ein Lean-Beweis kompiliert, kann jeder Dritte f