Claude beweist Fermats letzten Satz in 11 Tagen – komplett computergestützt

>Die Geschwindigkeit, mit der wir diesen Beweis erbringen konnten, zeigt, dass es jetzt möglich ist, große Teile der Mathematik zu formalisieren, was sowohl Fehler im allgemeinen Bestand mathematischer Beweise aufdecken als auch die Last des Begutachtens neuer Arbeiten verringern kann.

^ Dieser Abschnitt hätte meiner Meinung nach in den ersten paar Absätzen stehen sollen. Zu erklären, warum das relevant ist, sollte nicht so weit unten stehen.

"Der Beweis ist nicht der moderne Beweis, den ich selbst nach Ideen von Khare, Taylor usw. formalisiert habe, sondern die Darstellung von Darmon–Diamond–Taylor aus dem Jahr 1995 des Wiles–Taylor–Wiles-Arguments über den Satz von Langlands–Tunnell und Ribets Level-Lowering-Theorem. Das Repository von Anthropic entwickelt die Fontaine-Theorie (um flache Deformationen von Galois-Darstellungen zu untersuchen) und entwickelt genug von Mazurs Arbeit über das Eisenstein-Ideal, um zu schließen, dass keine Frey-Kurve einen Punkt der Ordnung p>=17 haben kann. Das bedeutet, dass ihr FLT-Beweis nur für p>=17 funktioniert, aber FLT wurde bereits für ungerade reguläre Primzahlen von Best-Birkbeck-Brasca-Rodriguez formalisiert, und die kleinste irreguläre Primzahl ist 37, also ist alles gut."

Meine Frage an alle Mathematiker, die das lesen: Ergibt das für euch irgendeinen Sinn?

Ich frage das, weil ich das meiste technische Material in Bezug auf Computertechnik, Programmierung, Hardwarespezifikationen usw. lesen kann. Selbst wenn ich nicht alle Details vollständig verstehe, kann ich ihnen ziemlich gut folgen. Also frage ich mich, ob professionelle Mathematiker auf das Obige schauen und es immer noch sinnvoll finden können, so wie erfahrene Softwareentwickler es bei Computersachen tun.

> Nebenbei schrieb es 13 Millionen Zeilen Lean und bewies 29.500 Zwischen-Theoreme.

Ziemlich verrückt. Ich nehme an, das stützt weiter die Idee, dass alles, von dem gezeigt werden kann, dass es korrekt ist, von einem Modell gemacht werden kann.

> Ein Team von Agenten schloss den Beweis in etwas weniger als zwei Wochen ab und verbrauchte dabei etwa sechs Milliarden Ausgabe-Token eines allgemeinen internen Forschungsmodells, das ungefähr mit Claude Fable 5.1 vergleichbar ist.

Bei 50 $/M Ausgabe-Token hätte das bei API-Preisen in der Größenordnung von 300.000 $ gekostet (plus etwas für Eingabe-/Prefill-Token).

Nebenbei bemerkt kann ich dieses Buch von Simon Singh sehr empfehlen.

https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)

13M Zeilen Code – sind wir sicher, dass es keine versteckten Probleme im Lean-Beweissystem ausgenutzt hat?

Wir werden zunehmend Ankündigungen dieser Art beobachten, während die KI-Werkzeuge skaliert werden. So beeindruckend agentisches Programmieren auch ist, es verblasst im Vergleich zum Wertversprechen von medizinischer, mathematischer und physikalischer Forschung.

Ich erwarte optimistisch, in meiner Lebenszeit das Aufkommen eines globalen 'Allheilmittels' dank der Bemühungen der KI zu erleben. Kostengünstige groß angelegte Gentechnik, eine Heilung für jede Krankheit, möglicherweise sogar eine Heilung für das Altern.

Die Zukunft ist sowohl schön als auch erschreckend.

Angesichts dessen, wie leistungsfähig und billig die automatische Beweisverifikation wird, frage ich mich, wie viele Beweise, die von fast der gesamten Mathematikgemeinschaft als wahr angenommen werden, sich als falsch herausstellen werden. Und nicht durch einen marginalen, leicht zu behebenden Fehler, sondern durch einen fundamentalen Denkfehler.

Okay, lasst uns ein Rudel wilder Agenten auf P = NP? loslassen!