# Claude beviste Fermat på 11 dager. Dom: SHIP IT.

Published: 2026-09-07

Claude brukte 11 dager og rundt 6 milliarder tokens på å skrive et 13 millioner linjer langt Lean-bevis for Fermats siste setning – det første ende-til-ende datakontrollerte – mens matematikeren som har formalisert det siden 2024, sier det «forteller oss i hovedsak ingenting» matematisk, og er likevel begeistret. Samme dag: Go-verdensener Shin Jin-seo slår KataGo 2–1 med to steiners handikap. Dom: SHIP IT.

Canonical: https://thedailydiff.dev/no/video/2026-09-04-fermat-lean/

## Hva denne videoen dekker

- Claude formaliserer Fermats siste setning i Lean 4
- Chromium sandkasse RCE (CVE-2026-85046), utnyttet i det fri, $1 000 dusør
- Shin Jin-seo slår KataGo med to steiners handikap

## Oversatt transkripsjon

Oversatt fra den originale engelske fortellingen. Tilgjengelig lyd og undertekster kontrolleres av YouTube.

0:00 Fermat sa at hans fantastiske bevis ikke ville få plass i margen, og i dag publiserte Anthropic margen: tretten millioner linjer med Lean, fem ganger størrelsen på Mathlib, som beviste et teorem hver matematiker allerede trodde på. Klokken var ti til elleve i Tbilisi da Anthropic publiserte, så naturlig nok var jeg våken. I går sendte Google Chrome 152 med tolv sikkerhetsfikser, en av dem en V8-feil som allerede var utnyttet i det fri, og betalte rapporteren tusen dollar, som er mindre enn sedanen vi kommer tilbake til senere.

0:26 Også i går sa Mullvad at de stenger ned sin offentlige krypterte DNS den 2. november og betaler Quad9 for å gjøre det i stedet, og i morges ble Rust React Compiler nativ i Vite, mens Hacker News oppdaget IBM Bob, en AI-kodeprogramvare. Så formaliserte Claude Fermats siste setning, og på samme forside slo en koreansk stormester den sterkeste Go-motoren på jorden, så i dag gikk menneskeheten én for to. I denne videoen: hva Claude faktisk beviste, hva det kostet,

0:52 hvorfor matematikeren som har brukt karrieren sin på dette sier det ikke endrer noe og er likevel begeistret, og hvordan et menneske slo maskinen i Go. Det er fredag 4. september, og dette er The Daily Diff. Fermats siste setning: ingen positive heltall a, b, c tilfredsstiller a opphøyd i n pluss b opphøyd i n er lik c opphøyd i n for noen n over 2. Fermat kriblet det ned i en marg rundt 1637 og døde uten å vise arbeidet sitt, noe som gjorde ham til den første utvikleren som lukket en billett med «fungerer på min maskin». En premie på 100 000 gullmark i 1908 tiltrakk seg 621 feilaktige

1:25 bevis i sitt første år, og Andrew Wiles fikk det endelig til i 1995, på 129 sider som tok dommere måneder å verifisere. Formalisering betyr å omskrive det beviset slik at Lean, en bevisassistent, kan sjekke hvert trinn mekanisk, og Kevin Buzzard ved Imperial har ledet en menneskelig innsats for å gjøre nettopp det siden 2024; selve planen er på 86 sider. Anthropic-forsker Tianyi Peng rettet dusinvis av Claude-agenter mot det i stedet, på en plattform kalt Prove2Me som holder en DAG av teorem- utsagn slik at agenter vet hva de skal bevise neste gang, for uten det mistet de første

2:00 svermene oversikt over hvem som beviste hva, noe som skjer når orkestreringslaget ditt er regex med et markedsbudsjett. Elleve dager senere leste rotenoden BEVIST: tretten millioner linjer med Lean, 29 500 mellomliggende teoremer, omtrent seks milliarder utdata-tokens fra en intern modell omtrent sammenlignbar med Claude Fable 5.1. Bygget mislykkes med mindre beviset hviler på nøyaktig Leans tre standardaksiomer: ingen beklager, ingen native decide, ingen juks. Å sjekke det er heller ikke billig: et

2:29 bygge fra bunnen av tok fem og en halv time på 96 kjerner og 153 gigabyte RAM, og teorem-navnene er maskingenererte, så repoet beskriver seg selv som skrevet for å sjekkes snarere enn å leses, noe som også er hvordan jeg vil beskrive enterprise Java. Nå til motsigelsen. Anthropics innlegg sier Lean demonstrerer korrekthet uten tvil. Kevin Buzzard, mannen som ble slått av Claude, kompilerte repoet på en 500-gigabyte maskin Anthropic lånte ham, bekreftet at det stemmer, og skrev deretter,

2:56 sitat, matematisk forteller dette arbeidet oss i hovedsak ingenting. Han var allerede 99,9 prosent sikker på at teoremet var sant, og beviset legger ikke til ny matematikk; det det viser er hva autoformalisering kan gjøre nå, og den delen er han genuint begeistret for. Han ble gitt en million pund over fem år; Anthropic brukte elleve dager, og en kommentators serviettmatematikk anslår seks milliarder utdata-tokens til listepris. rundt 300 000 dollar, så maskinen var billigere, med mindre du regner med opplæring av maskinen, noe ingen gjør.

3:24 Beste detalj: e-posten kom mens han var på en musikkfestival i Wales med én bar med 4G, fra et navn han aldri hadde hørt om, så han avskrev det som tull og leste den en uke senere, som er den riktige responsen på enhver emnelinje som inneholder ende-til-ende formalisering. I mellomtiden slo menneskene tilbake. Shin Jin-seo, verdenseneren i Go, slo KataGo, den sterkeste åpen kildekode Go-motoren, to kamper mot én i Seoul med to steiners handicap, omtrent forskjellen mellom en topp profesjonell og en nybegynner profesjonell.

3:50 Avgjørelsen var en 11,5-poengs seier på 221 trekk, med en 99 prosents seierssannsynlighet fra midtspillet og ut, og han tok med seg 250 millioner won, omtrent 170 000 dollar, pluss en Genesis G90, så belønningen for å slå en supermenneskelig AI er 170 ganger Googles belønning for en Chrome sandbox escape. Hans forklaring: tidlig kopierte han AI-trekk og tapte; han vant ved å bygge brettet i sin egen stil, noe som er det mest nyttige rådet om AI jeg har hørt i år, og det kom fra et brettspill. To linjer til i The Daily Diff.

4:22 Rust React Compiler fra oxc er nå nativ i Vite bak ett flagg; en kodebase på 1036 filer gikk fra 14,3 sekunder til 0,81 i kompileringssteget, mest ved å slette Babel fra package.json, som også er min hudpleierutine. Og IBM lanserte Bob, en AI-kodepartner som hilser deg med 'Hi, I'm Bob', skaper underagenter, moderniserer stormaskinkode, og SHIP IT et analyseprodukt kalt Bobalytics, så et sted er en bank veldig begeistret og ingen leste lisensen.

4:51 Det er mye margin for en fredag; hvis du heller vil lese dette enn å høre meg si det, lander The Daily Diff i innboksen din hver morgen – gratis på thedailydiff.dev, lenke under. Så, dagens dom: SHIP IT. Kjernen sier ja, Buzzard sier ja, matematikken endret seg ikke, men måten vi sjekker matematikken på, nettopp gjorde det. Det er dagens The Daily Diff. Jeg er Niko fra Axrisi.

5:09 Flett ansvarlig.

## Kilder

- [Anthropic — Formalizing Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem) — www.anthropic.com
- [The proof (Lean 4, Apache-2.0)](https://github.com/anthropics/fermats-last-theorem) — github.com
- [Kevin Buzzard — FLT: Anthropic has beaten me to it](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/) — xenaproject.wordpress.com
- [HN thread](https://news.ycombinator.com/item?id=49568506) — news.ycombinator.com
- [KED Global — Shin defeats KataGo](https://www.kedglobal.com/artificial-intelligence/newsView/ked202607210007) — www.kedglobal.com
- [HN](https://news.ycombinator.com/item?id=49544762) — news.ycombinator.com
- [Chrome 152 release notes (CVE-2026-85046)](https://chromereleases.googleblog.com/2026/09/stable-channel-update-for-desktop_01882797386.html) — chromereleases.googleblog.com
- [NVD](https://nvd.nist.gov/vuln/detail/cve-2026-85046) — nvd.nist.gov
- [Mullvad — shutting down public encrypted DNS](https://mullvad.net/en/blog/shutting-down-our-public-encrypted-dns-servers-and-sponsoring-quad9-instead) — mullvad.net
- [Rust React Compiler native in Vite](https://blog.master.dev/react-now-rusted-all-the-way-out/) — blog.master.dev
- [IBM Bob](https://bob.ibm.com/) — bob.ibm.com