Claude bewies Fermat in 11 Tagen. Urteil: VERSCHICKEN.

Was dieses Video behandelt

• Claude formalisiert Fermats letzten Satz in Lean 4
• Chromium Sandbox RCE (CVE-2026-85046), in freier Wildbahn ausgenutzt, 1.000 $ Belohnung
• Shin Jin-seo schlägt KataGo mit einem Zwei-Stein-Handicap

Übersetztes Transkript

Aus der englischen Originalerzählung übersetzt. Verfügbare Audio- und Untertitel werden von YouTube gesteuert.

0:00 Fermat sagte, sein wunderbarer Beweis würde nicht in den Rand passen, und heute veröffentlichte Anthropic den Rand: dreizehn Millionen Zeilen Lean, fünfmal so groß wie Mathlib, die einen Satz beweisen, den jeder Mathematiker bereits glaubte. Es war zehn vor elf in Tiflis, als Anthropic postete, also war ich natürlich wach. Gestern lieferte Google Chrome 152 mit zwölf Sicherheitskorrekturen aus, eine davon ein V8-Fehler, der bereits in freier Wildbahn ausgenutzt wurde, und zahlte dem Reporter tausend Dollar, was weniger ist als die Limousine, zu der wir später kommen.

0:26 Ebenfalls gestern kündigte Mullvad an, seinen öffentlichen verschlüsselten DNS am 2. November abzuschalten und stattdessen Quad9 dafür zu bezahlen, und heute Morgen ging der Rust React Compiler in Vite nativ, während Hacker News IBM Bob entdeckte, einen KI-Codierungsagenten. Dann formalisierte Claude Fermats letzten Satz, und auf derselben Titelseite schlug ein koreanischer Großmeister die stärkste Go-Engine der Welt, so dass die Menschheit heute eins von zwei schaffte. In diesem Video: was Claude tatsächlich bewiesen hat, was es gekostet hat,

0:52 warum der Mathematiker, der seine Karriere darauf verwendet hat, sagt, dass es nichts ändert und trotzdem begeistert ist, und wie ein Mensch die Maschine beim Go geschlagen hat. Es ist Freitag, der 4. September, und das ist The Daily Diff. Fermats letzter Satz: keine positiven ganzen Zahlen a, b, c erfüllen a hoch n plus b hoch n gleich c hoch n für jedes n größer als 2. Fermat kritzelte es um 1637 in einen Rand und starb, ohne seine Arbeit zu zeigen, was ihn zum ersten Entwickler machte, der ein Ticket mit "funktioniert auf meiner Maschine" schloss. Ein Preis von 100.000 Goldmark im Jahr 1908 zog im ersten Jahr 621 falsche

1:25 Beweise an, und Andrew Wiles fand ihn schließlich 1995, in 129 Seiten, deren Überprüfung Monate dauerte. Formalisieren bedeutet, diesen Beweis so umzuschreiben, dass Lean, ein Beweisassistent, jeden Schritt mechanisch überprüfen kann, und Kevin Buzzard vom Imperial College leitet seit 2024 eine menschliche Anstrengung, genau das zu tun; der Entwurf allein umfasst 86 Seiten. Der Anthropic-Forscher Tianyi Peng richtete stattdessen Dutzende von Claude-Agenten darauf aus, auf einer Plattform namens Prove2Me, die einen DAG von Theoremaussagen führt, damit Agenten wissen, was als Nächstes zu beweisen ist, denn ohne sie verloren die ersten

2:00 Schwärme den Überblick darüber, wer was bewies, was passiert, wenn Ihre Orchestrationsschicht Regex mit einem Marketingbudget ist. Elf Tage später lautete der Wurzelknoten BEWIESEN: dreizehn Millionen Zeilen Lean, 29.500 Zwischensätze, etwa sechs Milliarden ausgegebene Token von einem internen Modell, das ungefähr mit Claude Fable 5.1 vergleichbar ist. Der Build schlägt fehl, es sei denn, der Beweis basiert auf genau den drei Standardaxiomen von Lean: nein, sorry, kein natives entscheiden, kein Betrug. Die Überprüfung ist auch nicht billig: ein

2:29 Neubau dauerte fünfeinhalb Stunden auf 96 Kernen und 153 Gigabyte RAM, und die Theorem-Namen sind maschinengeneriert, so dass das Repo sich selbst als geschrieben zur Überprüfung und nicht zum Lesen beschreibt, was ich auch über Enterprise Java sagen würde. Nun der Widerspruch. Anthropic's Post sagt, Lean beweist die Korrektheit zweifelsfrei. Kevin Buzzard, der Mann, der dabei geschlagen wurde, kompilierte das Repo auf einer 500-Gigabyte-Maschine, die Anthropic ihm geliehen hatte, bestätigte, dass es sich überprüfen lässt, und schrieb dann,

2:56 Zitat, mathematisch sagt uns diese Arbeit im Wesentlichen nichts. Er war bereits zu 99,9 Prozent sicher, dass der Satz wahr war, und der Beweis fügt keine neue Mathematik hinzu; was er zeigt, ist, was Autoformalisation jetzt leisten kann, und darüber ist er wirklich begeistert. Ihm wurden eine Million Pfund über fünf Jahre gegeben; Anthropic brauchte elf Tage, und eine Überschlagsrechnung eines Kommentators beziffert sechs Milliarden ausgegebene Token zum Listenpreis rund 300.000 Dollar, die Maschine war also billiger, es sei denn, man zählt die Schulung der Maschine mit, was niemand tut.

3:24 Bestes Detail: Die E-Mail kam an, als er auf einem Musikfestival in Wales war, mit einem Balken 4G, von einem Namen, den er noch nie gehört hatte, also schrieb er es als Scherz ab und las sie eine Woche später, was die richtige Reaktion auf jede Betreffzeile ist, die End-to-End-Formalisierung enthält. Inzwischen haben die Menschen einen Punkt zurückgeholt. Shin Jin-seo, die Nummer eins der Welt im Go, schlug KataGo, die stärkste Open-Source-Go-Engine, zwei zu eins in Seoul mit einem Zwei-Stein-Handicap, ungefähr der Abstand zwischen einem Top-Profi und einem Rookie-Profi.

3:50 Die Entscheidung fiel mit einem 11,5-Punkte-Sieg in 221 Zügen, wobei er eine 99-prozentige Gewinnwahrscheinlichkeit ab der Mitte des Spiels hielt, und er nahm 250 Millionen Won, etwa 170.000 Dollar, plus einen Genesis G90 mit nach Hause, so dass das Kopfgeld für das Besiegen einer übermenschlichen KI 170-mal so hoch ist wie Googles Kopfgeld für einen Chrome-Sandbox-Escape. Seine Erklärung: Am Anfang kopierte er KI-Züge und verlor; er gewann, indem er das Brett in seinem eigenen Stil aufbaute, was der nützlichste Ratschlag über KI ist, den ich dieses Jahr gehört habe, und er kam von einem Brettspiel. Zwei weitere Zeilen im Diff.

4:22 Der Rust React Compiler von oxc ist jetzt nativ in Vite hinter einem Flag; eine 1.036-Datei-Codebasis ging von 14,3 Sekunden auf 0,81 im Kompilierschritt, hauptsächlich durch das Löschen von Babel aus package.json, was auch meine Hautpflegeroutine ist. Und IBM hat Bob eingeführt, einen KI-Coding-Partner, der Sie mit 'Hallo, ich bin Bob' begrüßt, Subagenten erstellt, Mainframe-Code modernisiert, und ein Analyseprodukt namens Bobalytics liefert, so dass irgendwo eine Bank sehr begeistert ist und niemand die Lizenz gelesen hat.

4:51 Das ist viel Spielraum für einen Freitag; wenn Sie dies lieber lesen als mich es sagen zu hören, landet der Diff jeden Morgen in Ihrem Posteingang – kostenlos unter TheDailyDiff.dev, Link unten. Also, heutiges Urteil: SHIP IT. Der Kernel sagt ja, Buzzard sagt ja, die Mathematik hat sich nicht geändert, aber die Art und Weise, wie wir Mathematik überprüfen, hat sich gerade geändert. Das ist der heutige Diff. Ich bin Niko von Axrisi.

5:09 Verantwortungsbewusst zusammenführen.

Quellen

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com