Was Claude Tatsächlich Getan Hat

Anthropic erklärte am 4. September, Claude habe den ersten vollständigen, computergeprüften Beweis von Fermats letztem Satz erstellt, über 11 Tage hinweg im Beweisassistenten Lean 4, nur mit grober Anleitung eines menschlichen Forschers. Das System erzeugte 13 Millionen Zeilen Lean-Code und bewies mehr als 30.000 Hilfssätze, von denen 29.500 in den finalen, verifizierten Beweis einflossen, mit einem internen Forschungsmodell, das über Dutzende parallel laufende Agenten auf der Plattform Prove2Me rund sechs Milliarden Output-Tokens verbrauchte.

Die zugrunde liegende Mathematik ist nicht neu. Andrew Wiles bewies Fermats letzten Satz 1995, und Claude formalisierte eine spätere Vereinfachung dieses Beweises von Darmon, Diamond und Taylor, wodurch ein 129-seitiges Argument, das die mathematische Gemeinschaft monatelang von Hand prüfen musste, in eine Form gebracht wurde, die ein Computer zeilenweise verifizieren kann. Mathematiker Kevin Buzzard, der das Ergebnis prüfte, sagte Anthropic, es sei ein großer Schritt zur automatischen Formalisierung der modernen mathematischen Literatur, erreicht in weit kürzerer Zeit, als er erwartet hatte.

Warum Dies Eine Kostenfrage Ist, Keine Mathefrage

Die entscheidende Zahl hier sind nicht 13 Millionen Zeilen, sondern 11 Tage. Formale Verifikation, also der Nachweis, dass ein Stück Mathematik oder Software korrekt ist, statt es nur zu testen und zu hoffen, war von Hand immer langsam und teuer, und die Formalisierung eines Ergebnisses dieser Größe kostete Spezialteams bisher Jahre an Arbeit. Genau diese Kosten sind der Grund, warum so wenig sicherheitskritische Software weltweit überhaupt einen formalen Korrektheitsbeweis trägt, und ein automatisiertes System, das vergleichbare Arbeit in unter zwei Wochen leistet, verändert die Rechnung für jedes europäische Ingenieurunternehmen, das Systeme nach Normen wie ISO 26262 für Autos oder DO-178C für Flugzeuge zertifiziert, wo formale Methoden bereits verwendet, aber wegen ihres Preises rationiert werden.

Anthropics eigener Bericht ist offen über die Fehlerquote hinter dieser Schlagzeile: Rund 7 Prozent des nicht standardisierten Codes stammten aus gescheiterten Versuchen, die auf dem Weg zum finalen Beweis verworfen wurden. Das ist ein normaler Teil davon, wie formale Verifikation immer schon fortschritt, ob Maschine oder Mensch, aber es verdient klare Erwähnung, weil ein Erfolg von 13 Millionen Zeilen den gegenteiligen Eindruck weckt.

Die Grenze, Die Niemand Übergehen Sollte

Claude formalisierte einen bestehenden Beweis, es entdeckte keinen neuen, und dieser Unterschied zählt mehr als die Leistung selbst, sobald jemand versucht, technisches Gewicht darauf zu legen. Fermats letzter Satz funktionierte als Demonstration gerade deshalb, weil sich Mathematiker seit drei Jahrzehnten einig waren, wie der korrekte Beweis aussieht, weshalb Claudes Aufgabe darin bestand, ein bekanntes Argument in eine maschinenprüfbare Sprache zu übersetzen, nicht zu entscheiden, ob das Argument überhaupt richtig war.

Ein Sicherheitsnachweis für ein Bremssystem oder ein kryptografisches Protokoll beginnt mit einer schwierigeren Frage: Was bedeutet korrekt hier überhaupt, und hat jemand es präzise genug spezifiziert, damit eine formale Methode es dagegen prüfen kann. Automatisierte Formalisierung kann die zweite Hälfte dieses Problems nun drastisch verkleinern. Für die erste Hälfte ändert sie nichts, und jede Organisation, die dieses Ergebnis als Freibrief liest, Spezifikationsarbeit statt Verifikationsarbeit zu überspringen, hat es falsch verstanden.

Weiterlesen: 87 Jahre enden mit einer Antwort, die jeder nachprüfen kann  |  Claude-Protokolle ziehen in Ihre eigene Cloud um