Wir teilen den ersten vollständigen computergeprüften Beweis des letzten Satzes von Fermat. Claude arbeitete weitgehend autonom über 11 Tage, um den Beweis in der Programmiersprache Lean zu schreiben. Im Folgenden beschreiben wir, wie die Formalisierung durchgeführt wurde, und teilen einige Gedanken darüber, was diese Arbeit für die Forschungsmathematik bedeuten könnte.

Um 1637 notierte Pierre de Fermat eine Behauptung am Rand seiner Kopie der Arithmetica von Diophantus, die zu einer der berühmtesten mathematischen Vermutungen aller Zeiten werden sollte: Es gibt keine positiven ganzen Zahlen a, b, c, die aⁿ + bⁿ = cⁿ für irgendein n > 2 erfüllen. Der letzte Satz von Fermat (FLT), wie die Vermutung bekannt wurde, erwies sich als unglaublich schwer zu beweisen. Der erste Beweis von Sir Andrew Wiles aus dem Jahr 1995 umfasste 129 Seiten und erforderte Monate mühsamer Arbeit zur Verifizierung.

Ein Jahrzehnt später schlug der niederländische Informatiker Jan Bergstra vor, den Beweis von Wiles zu „formalisieren“: die mathematische Argumentation in eine Form zu überführen, die Computer automatisch überprüfen können. Seitdem haben Mathematiker die Methoden entwickelt, die zur Kodierung eines so komplexen Beweises erforderlich sind, darunter eine mehrjährige Gemeinschaftsanstrengung, die 2024 von Kevin Buzzard am Imperial College London gestartet wurde, um die Formalisierung mit dem Beweisassistenten Lean abzuschließen.

Kürzlich machte sich Tianyi Peng, ein Forscher bei Anthropic, dessen Gruppe an der Columbia University Werkzeuge für die KI-Formalisierung entwickelt, daran zu testen, ob Claude Fortschritte bei der Formalisierung von FLT erzielen könnte. Das Ergebnis übertraf seine Erwartungen. In 11 Tagen, weitgehend autonom arbeitend, erzeugte Claude den ersten durchgängigen, computergeprüften Beweis von FLT. Dabei schrieb es 13 Millionen Zeilen Lean und bewies 29.500 Zwischen-Theoreme.