Die Mathematikwelt ist erschüttert: Claude hat in einem Zug 190.000 Zeilen Quellcode verfasst und den Fehler in einem vor 13 Jahren erbrachten Beweis aufgespürt.

Das treibt die menschlichen Mathematiker wirklich in eine ausweglose Lage...

Zum Großen Fermatschen Satz haben 1000 Claude Fable 5.2 in 30 Stunden in Teams einen vollständigen formalen Beweis abgeschlossen.

Gerade heute hat eine Person gemeinsam mit Claude den Beweis der vor 13 Jahren bewiesenen „ternären Goldbach-Vermutung“ formalisiert.

Diese Aktion stammt von dem unabhängigen Entwickler Charlie Reams, der 194.000 Zeilen Lean 4 Code geschrieben hat, und die gesamte Bibliothek weist null „sorry“ auf.

Noch erstaunlicher ist, dass Claude selbst mehrere Fehler im ursprünglichen Beweis von 2013 entdeckt hat!

Ohne zu zögern hat er diese mathematischen Lücken sofort repariert.

Eine Person + ein Claude, 194.000 Zeilen Quellcode in intensiver Arbeit erledigt

An dieser Stelle muss man unbedingt hervorheben: Die oft genannte „1+1“ ist die starke Goldbach-Vermutung, die bis heute noch niemand vollständig beweisen konnte.

Die „ternäre Goldbach-Vermutung“ hingegen wird als schwache Goldbach-Vermutung bezeichnet, das bedeutet –

Jede ungerade Zahl größer als 5 kann als Summe von drei Primzahlen dargestellt werden.

2013 verkündete der peruanische Mathematiker Harald Helfgott, dass er dieses seit 271 Jahren die Menschheit beschäftigende Problem vollständig bewiesen hat.

Zu dieser Zeit war dies ein weltweit Aufsehen erregendes mathematisches Großereignis.

Aber das Problem folgte sofort: Helfgotts Beweis war einfach viel zu lang und zu umständlich! Allein das Hauptmanuskript umfasste 300 Seiten, vollgestopft mit endlosen Ungleichungsabschätzungen und Konstantenberechnungen.

In den darauf folgenden mehr als zehn Jahren hat Helfgott selbst mehrere Versionen aktualisiert, um Details zu korrigieren.

Trotzdem haben aufgrund der einschüchternd langen Berechnungsprozesse weltweit nur sehr wenige Mathematiker die Energie, jede Konstante von Anfang bis Ende durchzugehen und zu überprüfen.

Der unabhängige Entwickler Charlie Reams beschloss, die Aufgabe Claude Code zu überlassen.

Wenn man das GitHub-Repository calr3/ternary-goldbach (Zweig cde-moebius) öffnet, sieht man ein beeindruckendes numerisches Projekt:

Ganze 194.000 Zeilen Lean Code, Hilfsskripte und technische Dokumentationen.

In diesem Projekt war Charlie Reams für die Festlegung der obersten Ziele und die Zerlegung der Aufgabenanweisungen zuständig.

Der überwiegende Teil des formalen Lean Codes, der automatisierten Skripte und sogar der Dokumentationen wurde vollständig von Claude Code erstellt.

Das Endergebnis hat alle beeindruckt: 194.000 Zeilen Quellcode mit 0 „sorry“!

In der Lean-Sprache steht „sorry“ für das Überspringen unvollständig bewiesener Schritte. Null „sorry“ bedeutet, dass jede Zeile der Schlussfolgerung einer extrem strengen maschinellen Überprüfung unterzogen wurde, ohne eine einzige Lücke zu hinterlassen.

11 Probleme aufgedeckt und nebenbei die „Hausaufgaben“ des Spitzenmathematikers korrigiert

Man muss wissen: Die Schwierigkeit bei der Überprüfung von Helfgotts Beweis liegt darin, dass er „voller Zahlen“ ist.

Er verwendet die Kreismethode: Das Problem wird in Hauptbögen und Nebenbögen unterteilt. Die Hauptbögen sind die „Einnahmen“ und die Nebenbögen sind die „Ausgaben“. Solange die Einnahmen sicher größer als die Ausgaben sind, ist der Satz gültig.

Wenn Menschen solche Inhalte mit den Augen überprüfen, bekommen sie schon bei Seite 50 Angst, aber Lean nicht.

In der README des Repositories sind 11 Stellen aufgeführt, die nicht mit dem Original übereinstimmen. Hier sind die drei eindrucksvollsten Details:

Erstens: Ein Rechenfehler. In Gleichung (6.77) des Buches wurde eine Schlüsselkonstante als 0,5 angegeben, der richtige Wert sollte 0,8102 sein; nach der entsprechenden Korrektur wurde im Projekt schließlich 0,8764 verwendet.

Zweitens: Eine Ungleichung ist überhaupt nicht gültig.

Gleichung (5.32) im Buch ist falsch, wenn v=2 ist: Ein Integral ergibt tatsächlich 0,53344, was die im Buch angegebene obere Schranke von 0,37273 · log 4 (ca. 0,5167) übersteigt.

Drittens: Bei der Fehlersuche wurde auch der Fehler einer anderen Person gefunden.

Der ursprüngliche Beweis zitiert einen Schritt aus Ramarés Arbeit von 1995 und behauptet, dass ein bestimmtes Produkt nicht größer als 8 ist, tatsächlich beträgt es aber etwa 8,0845. Claude hat nicht stur abgeschrieben, sondern eine andere Zerlegungsmethode gewählt, um das Problem zu umgehen, und erhielt 7,04, was immer noch unter dem erforderlichen Wert von 7,284 liegt.

Darüber hinaus gibt es noch einen „schwerwiegenden Mangel“ im Beweis: Im Beweis von Satz 13.2.1 wurden die Hauptbögen zweier verschiedener Skalen vermischt, dieser Abschnitt wurde vollständig neu aufgebaut.

Nachdem Claude die Korrekturen abgeschlossen hatte, sank die „Einnahme“ der Hauptbögen von 1,058259 im Original auf 1,049, und die „Ausgabe“ der Nebenbögen stieg von 1,00948 auf 1,0376.

Die Differenz zwischen den beiden, also die Sicherheitsreserve des Beweises, schrumpfte von 0,04877 x²/κ auf 0,0114 x²/κ, also um mehr als drei Viertel. Sie ist aber immer noch größer als Null.

Der ursprüngliche Autor tritt persönlich auf und enthüllt zwei „unerfüllte Voraussetzungen“

Nachdem sich die Sache verbreitet hatte, waren alle neugierig –

Wie würde der ursprüngliche Autor Harald Helfgott reagieren, wenn er sieht, dass sein berühmtes Werk von einer KI auf Fehler untersucht und repariert wurde?

Schon bald erschien Helfgott selbst auf X und zeigte sich äußerst aufgeschlossen: Bereits am 4. Oktober dieses Jahres hatte Charlie Reams ihn privat kontaktiert und ihm mitgeteilt, dass die Formalisierungsarbeit erfolgreich abgeschlossen wurde.

In diesem Monat haben eine Person und die KI noch eine weitere große Sache erledigt –

Sie haben die zusätzlichen externen Annahmen (Axiome), von denen der gesamte Beweis abhängt, von anfangs 5 auf nur noch 2 reduziert!

In diesem Repository ist die gesamte Ableitungslogik der analytischen Zahlentheorie zu 100 % formalisiert und weist null „sorry“ auf, aber sie stützt sich außerhalb von Lean noch auf zwei bestehende numerische Überprüfungsergebnisse als Voraussetzungen:

Die numerische Überprüfung der verallgemeinerten Riemann-Vermutung (GRH) von Platt und die lokale Überprüfung der geraden Goldbach-Vermutung bis 4×10^18.

Wenn diese beiden „riesigen numerischen Sprungbretter“, die Menschen schon lange berechnet, aber noch nicht in den Lean-Kern integriert haben, eingefügt werden, schließt sich das gesamte Gebäude der ternären Goldbach-Vermutung lückenlos.

Superintelligenz definiert neu, was „vollständig bewiesen“ bedeutet

Ob ein hunderte Seiten langer Beweis als „vollständig bewiesen“ gilt, hängt davon ab, dass einige wenige Experten mehrere Jahre brauchen, um ihn durchzuarbeiten, und selbst danach sind sie sich nicht unbedingt sicher.

Jetzt ändert sich der Standard zu einem anderen Satz: Ob er den Kern durchlaufen hat.

Vielleicht wird es nicht lange dauern, bis das härteste Peer-Review in der Mathematik nur noch einen Satz hat:

„Schickt kein PDF mehr, gebt zuerst euren Beweis an Claude weiter, bis ihr null „sorry“ bekommt.“

Referenzen:

https://x.com/jdlichtman/status/2120301890504441905

Dieser Artikel stammt aus dem WeChat-Offiziellen Konto AI Era, Autor: Taozi, veröffentlicht mit Genehmigung von 36kr.