Fermats letzter Satz beschäftigt Mathematiker seit Jahrhunderten. Nun hat eine KI erstmals einen vollständigen, computergeprüften Beweis erbracht. In elf Tagen sind dabei 13 Millionen Zeilen Code entstanden.
Fermats letzter Satz gehört zu den berühmtesten Rätseln der Mathematik. Das Theorem lässt sich gut über den Satz des Pythagoras erklären, weil beide auf einer sehr ähnlichen Gleichung beruhen. Der Satz des Pythagoras beschreibt mit der Gleichung a² + b² = c² ein rechtwinkliges Dreieck.
Fermat stellte sich nun vereinfacht gesagt die Frage, was passiert, wenn man die Quadrate in dieser Gleichung durch höhere Potenzen ersetzt. Er kam zu dem Schluss, dass es keine positiven ganzen Zahlen mehr gibt, die eine Gleichung der Form aⁿ + bⁿ = cⁿ erfüllen, wenn der Exponent größer als zwei ist.
Du willst nicht abgehängt werden, wenn es um KI, Green Tech und die Tech-Themen von Morgen geht? Über 12.000 Vordenker bekommen jeden Tag die wichtigsten News direkt in die Inbox und sichern sich ihren Vorsprung.
Nur für kurze Zeit: Anmelden und mit etwas Glück Apple AirPods gewinnen!
Mit deiner Anmeldung bestätigst du unsere Datenschutzerklärung. Beim Gewinnspiel gelten die AGB.
Was also bei Quadraten wie 3² + 4² = 5² funktioniert, ist bei Kubikzahlen und allen höheren Potenzen unmöglich. Doch obwohl sich Fermats letzter Satz leicht formulieren lässt, gelang es Mathematikern mehr als 350 Jahre lang nicht, ihn allgemein zu beweisen.
Erst dem britischen Mathematiker Andrew Wiles gelang Anfang der 1990er-Jahre der entscheidende Durchbruch. Gemeinsam mit seinem Kollegen Richard Taylor konnte Wiles seinen vollständigen Beweis 1995 veröffentlichen.
Nun wurde bei Fermats letztem Satz ein weiterer Meilenstein erreicht. Denn erstmals liegt der berühmte Beweis vollständig in einer Form vor, die ein Computer Schritt für Schritt überprüfen kann. Dafür hat die KI von Anthropic in elf Tagen 13 Millionen Zeilen Code verfasst.
Anthropic knackt KI-Beweis für Fermats letzten Satz
Der Beweis von Andrew Wiles aus dem Jahr 1995 umfasste insgesamt 129 Seiten. In der Fachwelt gilt Fermats letzter Satz seither als gesichert.
Dennoch forderte der niederländische Informatiker Jan Bergstra ein Jahrzehnt später, Wiles‘ Beweis zu „formalisieren“. Die mathematische Beweisführung sollte also so formuliert werden, dass sie von Computern automatisch überprüft werden kann.
Innerhalb von elf Tagen und weitgehend autonom erstellte Claude den ersten durchgängigen, computergeprüften Beweis für FLT. Dabei schrieb das System 13 Millionen Zeilen Lean-Code und bewies 29.500 Zwischensätze.
Genau das ist nun der KI Claude aus dem Hause Anthropic gelungen. Nach Angaben des Unternehmens handelt es sich um „den ersten vollständigen, computergeprüften Beweis von Fermats letztem Theorem“.
Dieser ist innerhalb von elf Tagen entstanden, wobei Claude „weitgehend autonom“ gearbeitet habe. Den Beweis habe ein Schwarm von Claude-Agenten im Beweisassistenten Lean geschrieben, eine unabhängige Bewertung steht jedoch weitgehend noch aus.
Fermats letzter Satz: Beweisassistent Lean prüft Argumentationskette
Eine Schlüsselrolle bei der erfolgreichen Erstellung des Beweises spielte der Beweisassistent Lean. Dabei handelt es sich vereinfacht gesagt um eine Mischung aus Programmiersprache und mathematischem Prüfwerkzeug.
Bei der Nutzung von Lean wird ein Beweis so präzise in Code übersetzt, dass der Computer jeden einzelnen logischen Schritt kontrollieren kann. Dabei müssen selbst vermeintlich selbstverständliche Zwischenschritte komplett ausformuliert und hergeleitet werden.
Im Gegensatz zur menschlichen Beweisführung kann sich Lean nicht auf Erfahrungen oder unausgesprochene Annahmen verlassen. Jeder Schritt muss daher formal aus zuvor festgelegten Regeln und bereits bewiesenen Aussagen folgen. Nur dann akzeptiert das System den Beweis als korrekt.
Für den computergeprüften Beweis von Fermats letztem Satz musste die KI Claude also den bereits vorhandenen mathematischen Beweis in eine Form bringen, die Lean vollständig verstehen und überprüfen kann. Dabei entstanden 13 Millionen Zeilen Code und 29.500 Zwischensätze, die die gesamte Argumentationskette formal abbildeten und überprüfbar machten.
Google lässt dich jetzt selbst bestimmen, welche Quellen du in der Suche häufiger siehst. Mit zwei schnellen Klicks kannst du BASIC thinking kostenlos als bevorzugte Quelle hinzufügen und damit unabhängigen Tech-Journalismus unterstützen. Vielen Dank!
Auch interessant:
