Satz von Fermat: Claude formalisiert ihn in elf Tagen

Bereits im Juli hatte ein Physik-Nobelpreisträger berichtet, sich von der künstlichen Intelligenz Claude bei einem physikalischen Problem helfen lassen zu haben. Nun gibt Anthropic bekannt, dass ein experimentelles Claude-Modell in elf Tagen den Beweis des letzten Satzes von Fermat in die Sprache Lean formalisiert hat. Es handelt sich um die Übersetzung eines komplexen mathematischen Beweises in einen Code, den ein Computer Schritt für Schritt überprüfen kann.

Für dieses Ergebnis hat Claude rund 13 Millionen Zeilen Code und 30300 Zwischensätze erzeugt. Der Vergleich mit der menschlichen Arbeit zeigt das Ausmass der Leistung: Für das von Mathematiker Kevin Buzzard geleitete Projekt zur vollständigen Formalisierung des Satzes waren rund zehn Jahre veranschlagt worden.

Der letzte Satz von Fermat wurde 1637 von Pierre de Fermat aufgestellt. Er besagt, dass die Gleichung xⁿ + yⁿ = zⁿ für jede ganze Zahl n grösser als 2 keine positiven ganzzahligen Lösungen ungleich null hat. Das Problem blieb über drei Jahrhunderte ungelöst, bis Andrew Wiles es in den Neunzigerjahren mit einem Beitrag von Richard Taylor bewies.

Was Claude tatsächlich geleistet hat

Die Arbeit der künstlichen Intelligenz besteht nicht darin, einen neuen Beweis gefunden zu haben: Derjenige von Wiles bleibt gültig und wurde nicht infrage gestellt. Claude hat den bestehenden Beweis stattdessen in eine formale Abfolge von Schritten umgewandelt, die von einem Computer kontrolliert werden kann. Genau das ist der Zweck von Lean, der Sprache und Umgebung, die zur Formalisierung von Mathematik verwendet wird.

Das Ergebnis hat allerdings eine Einschränkung. Der von der künstlichen Intelligenz erzeugte Code kann derzeit nicht in Mathlib integriert werden, die von der wissenschaftlichen Gemeinschaft verwendete Standardbibliothek für formale Mathematik. Die Formalisierung ist also abgeschlossen, aber noch nicht bereit, dauerhaft in das gemeinsame Ökosystem der Mathematiker einzugehen.

Das Experiment zeigt dennoch eine Richtung für künstliche Intelligenz in der Mathematik auf: nicht nur Antworten liefern, sondern formal überprüfbare Beweise erstellen. Die nächste Herausforderung wird laut der Ankündigung darin bestehen, solche Ergebnisse nicht nur schnell zu erzielen, sondern auch lesbar und für Mathematiker wiederverwendbar zu machen.