Claude beviste Fermat på 11 dage. Dom: SHIP IT.

Hvad denne video dækker

• Claude formaliserer Fermats sidste sætning i Lean 4
• Chromium sandbox RCE (CVE-2026-85046), udnyttet i praksis, $1.000 dusør
• Shin Jin-seo slår KataGo med et handicap på to sten

Oversat udskrift

Oversat fra den originale engelske fortælling. Tilgængelig lyd og undertekster styres af YouTube.

0:00 Fermat sagde, at hans vidunderlige bevis ikke ville passe ind i margen, og i dag offentliggjorde Anthropic margenen: tretten millioner linjer Lean, fem gange størrelsen af Mathlib, der beviste en sætning, som enhver matematiker allerede troede på. Klokken var ti til elleve i Tbilisi, da Anthropic postede, så naturligvis var jeg vågen. I går udgav Google Chrome 152 med tolv sikkerhedsrettelser, én af dem en V8-fejl, der allerede blev udnyttet i praksis, og betalte rapportøren tusind dollars, hvilket er mindre end den sedan, vi kommer til senere.

0:26 Også i går sagde Mullvad, at de lukker deres offentlige krypterede DNS den 2. november og betaler Quad9 for at gøre det i stedet, og i morges gik Rust React Compiler native i Vite, mens Hacker News opdagede IBM Bob, en AI-kodedatagent. Så formaliserede Claude Fermats sidste sætning, og på samme forside slog en koreansk stormester den stærkeste Go-motor på Jorden, så i dag scorede menneskeheden én ud af to. I denne video: hvad Claude faktisk beviste, hvad det kostede,

0:52 hvorfor matematikeren, der brugte sin karriere på dette, siger, at det ikke ændrer noget og alligevel er begejstret, og hvordan et menneske slog maskinen i Go. Det er fredag den 4. september, og dette er The Daily Diff. Fermats sidste sætning: ingen positive heltal a, b, c opfylder a i n plus b i n er lig med c i n for ethvert n over 2. Fermat nedfældede det i en margen omkring 1637 og døde uden at vise sit arbejde, hvilket gjorde ham til den første udvikler, der lukkede en sag med virker på min maskine. En pris på 100.000 guldmark i 1908 tiltrak 621 forkerte

1:25 beviser i sit første år, og Andrew Wiles fik det endelig i 1995, på 129 sider, som det tog dommerne måneder at verificere. At formalisere betyder at omskrive dette bevis, så Lean, en bevisassistent, kan kontrollere hvert skridt mekanisk, og Kevin Buzzard ved Imperial har ledet en menneskelig indsats for at gøre netop det siden 2024; alene udkastet fylder 86 sider. Anthropic-forsker Tianyi Peng rettede i stedet dusinvis af Claude-agenter mod det på en platform kaldet Prove2Me, der opretholder en DAG af sætningsudsagn, så agenterne ved, hvad de skal bevise næste, for uden den mistede de første

2:00 sværme overblik over, hvem der beviste hvad, hvilket er hvad der sker, når dit orkestreringslag er regex med et marketingbudget. Elleve dage senere stod der på rodnoden BEVIST: tretten millioner linjer Lean, 29.500 mellemliggende sætninger, omkring seks milliarder output-tokens fra en intern model, der groft set kan sammenlignes med Claude Fable 5.1. Bygget fejler, medmindre beviset hviler på præcis Leans tre standardaksiomer: ingen undskyld, ingen native beslutning, ingen snyd. At kontrollere det er heller ikke billigt: en

2:29 fra-bunden-opbygning tog fem en halv time på 96 kerner og 153 gigabyte RAM, og sætningsnavnene er maskingenererede, så repoet beskriver sig selv som skrevet til at blive kontrolleret snarere end læst, hvilket også er sådan jeg ville beskrive enterprise Java. Nu modsigelsen. Anthropic's indlæg siger, at Lean demonstrerer korrekthed ud over enhver tvivl. Kevin Buzzard, manden der blev slået af den, kompilerede repoet på en 500-gigabyte maskine, Anthropic lånte ham, bekræftede at det var korrekt, og skrev derefter,

2:56 citat, matematisk set fortæller dette arbejde os i det væsentlige intet. Han var allerede 99,9 procent sikker på, at sætningen var sand, og beviset tilføjer ingen ny matematik; hvad det viser er, hvad autoformalisering kan gøre nu, og den del er han oprigtigt begejstret for. Han fik en million pund over fem år; Anthropic tog elleve dage, og en kommentators hurtige udregning sætter seks milliarder output-tokens til listepris omkring 300.000 dollars, så maskinen var billigere, medmindre du regner med træning af maskinen, hvilket ingen gør.

3:24 Bedste detalje: e-mailen ankom, mens han var til en musikfestival i Wales med én bar 4G, fra et navn, han aldrig havde hørt om, så han afskrev det som en joke og læste det en uge senere, hvilket er den korrekte reaktion på enhver emnelinje der indeholder ende-til-ende formalisering. Imens fik mennesker et point tilbage. Shin Jin-seo, verdens nummer et i Go, slog KataGo, den stærkeste open-source Go-motor, to spil mod et i Seoul med et handicap på to sten, omtrent forskellen mellem en top professionel og en rookie professionel.

3:50 Afgørelsen var en sejr på 11,5 point i 221 træk, og holdt en 99 procents sandsynlighed for sejr fra midten af spillet, og han tog 250 millioner won hjem, cirka 170.000 dollars, plus en Genesis G90, så belønningen for at slå en supermenneskelig AI er 170 gange Googles belønning for en Chrome sandbox escape. Hans forklaring: tidligt kopierede han AI-træk og tabte; han vandt ved at bygge brættet i sin egen stil, hvilket er det mest nyttige råd om AI, jeg har hørt i år, og det kom fra et brætspil. To linjer mere i The Daily Diff.

4:22 Rust React Compiler fra oxc er nu native i Vite bag et flag; en 1.036-fils kodebase gik fra 14,3 sekunder til 0,81 i kompilerings-trinnet, mest ved at slette Babel fra package.json, hvilket også er min hudplejerutine. Og IBM lancerede Bob, en AI-kodningspartner, der hilser dig med 'Hej, jeg er Bob', skaber underagenter, moderniserer mainframe-kode, og sender et analyseprodukt kaldet Bobalytics, så et sted er en bank meget begejstret, og ingen læste licensen.

4:51 Det er en stor margin for én fredag; hvis du hellere vil læse dette end høre mig sige det, lander The Daily Diff i din indbakke hver morgen — gratis på thedailydiff.dev, link nedenfor. Så dagens dom: SHIP IT. Kernen siger ja, Buzzard siger ja, matematikken ændrede sig ikke, men måden vi tjekker matematik på, gjorde netop det. Det er dagens The Daily Diff. Jeg er Niko fra Axrisi.

5:09 Flet ansvarligt.

Kilder

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