# Claude bevisade Fermat på 11 dagar. Dom: SHIP IT.

Published: 2026-09-07

Claude tillbringade 11 dagar och cirka 6 miljarder tokens med att skriva ett 13 miljoner rader långt Lean-bevis för Fermats sista sats – det första helt datorverifierade – medan matematikern som har formaliserat den sedan 2024 säger att den "talar om i princip ingenting" matematiskt och är ändå överlycklig. Samma dag: Världens nummer 1 Shin Jin-seo slår KataGo 2–1 med ett två-stens handikapp. Dom: SHIP IT.

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

## Vad den här videon täcker

- Claude formaliserar Fermats sista sats i Lean 4
- Chromium sandbox RCE (CVE-2026-85046), utnyttjas i praktiken, 1 000 USD i belöning
- Shin Jin-seo slår KataGo med ett två-stens handikapp

## Översatt transkription

Översatt från den ursprungliga engelska berättelsen. Tillgängligt ljud och undertexter styrs av YouTube.

0:00 Fermat sa att hans underbara bevis inte skulle få plats i marginalen, och idag publicerade Anthropic marginalen: tretton miljoner rader Lean, fem gånger så stort som Mathlib, som bevisar ett teorem som varje matematiker redan trodde på. Klockan var tio till elva i Tbilisi när Anthropic postade, så naturligtvis var jag vaken. Igår skeppade Google Chrome 152 med tolv säkerhetsfixar, en av dem en V8-bugg som redan utnyttjats i praktiken, och betalade reportern tusen dollar, vilket är mindre än sedanen vi kommer till senare.

0:26 Igår sa Mullvad också att de stänger ner sin offentliga krypterade DNS den 2 november och betalar Quad9 för att göra det istället, och i morse blev Rust React Compiler native i Vite, medan Hacker News upptäckte IBM Bob, en AI-kodningsagent. Sedan formaliserade Claude Fermats sista sats, och på samma förstasida slog en koreansk stormästare den starkaste Go-motorn på jorden, så idag gick mänskligheten en av två. I den här videon: vad Claude faktiskt bevisade, vad det kostade,

0:52 varför matematikern som tillbringade sin karriär på detta säger att det inte ändrar något och är ändå överlycklig, och hur en människa slog maskinen i Go. Det är fredag den 4 september, och detta är The Daily Diff. Fermats sista sats: inga positiva heltal a, b, c uppfyller a upphöjt till n plus b upphöjt till n är lika med c upphöjt till n för något n över 2. Fermat klottrade ner det i en marginal runt 1637 och dog utan att visa sitt arbete, vilket gjorde honom till den första utvecklaren som stängde en biljett med fungerar på min maskin. Ett pris på 100 000 guldmark år 1908 lockade 621 felaktiga

1:25 bevis under sitt första år, och Andrew Wiles fick det slutligen 1995, på 129 sidor som tog domare månader att verifiera. Att formalisera betyder att skriva om det beviset så att Lean, en bevisassistent, kan kontrollera varje steg mekaniskt, och Kevin Buzzard vid Imperial har lett en mänsklig insats för att göra precis det sedan 2024; enbart ritningen är 86 sidor. Anthropic-forskaren Tianyi Peng riktade dussintals Claude-agenter mot det istället, på en plattform kallad Prove2Me som håller en DAG av teoremsatser så agenter vet vad de ska bevisa härnäst, för utan det tappade de första

2:00 svärmarna koll på vem som bevisade vad, vilket är vad som händer när ditt orkestreringslager är regex med en marknadsföringsbudget. Elva dagar senare stod det på rotnoden BEVISAD: tretton miljoner rader Lean, 29 500 mellanliggande satser, cirka sex miljarder utmatade tokens från en intern modell ungefär jämförbar med Claude Fable 5.1. Bygget misslyckas om inte beviset vilar på exakt Leans tre standardaxiom: ingen ursäkt, ingen inbyggd beslutsförmåga, inget fusk. Att kontrollera det är inte heller billigt: ett

2:29 från-grunden-bygge tog fem och en halv timme på 96 kärnor och 153 gigabyte RAM, och teoremens namn är maskingenererade, så repot beskriver sig självt som skrivet för att kontrolleras snarare än att läsas, vilket också är hur jag skulle beskriva enterprise Java. Nu motsägelsen. Anthropics inlägg säger att Lean demonstrerar korrekthet bortom all tvivel. Kevin Buzzard, mannen som blev slagen på mållinjen, kompilerade repot på en 500-gigabyte maskin som Anthropic lånade honom, bekräftade att det stämmer, och skrev sedan,

2:56 citat, matematiskt sett säger detta arbete oss i princip ingenting. Han var redan 99,9 procent säker på att teoremet var sant, och beviset lägger inte till någon ny matematik; vad det visar är vad autoformalism kan göra nu, och den delen är han genuint entusiastisk över. Han fick en miljon pund över fem år; Anthropic tog elva dagar, och en kommentators snabba räkneexempel sätter sex miljarder utmatade tokens till listpris runt 300 000 dollar, så maskinen var billigare, om man inte räknar med att träna maskinen, vilket ingen gör.

3:24 Bästa detalj: e-postmeddelandet anlände medan han var på en musikfestival i Wales med en stapel 4G, från ett namn han aldrig hade hört talas om, så han avfärdade det som ett skämt och läste det en vecka senare, vilket är det korrekta svaret på alla ämnesrader som innehåller end-to-end-formalisering. Under tiden fick människor en vinst tillbaka. Shin Jin-seo, världsettan i Go, besegrade KataGo, den starkaste Go-motorn med öppen källkod, med två matcher mot en i Seoul med ett tvåstens- handikapp, ungefär skillnaden mellan en topprofessionell och en nybörjare.

3:50 Avgörandet var en vinst på 11,5 poäng i 221 drag, med en 99 procents vinstsannolikhet från mitten av spelet och han vann 250 miljoner won, cirka 170 000 dollar, plus en Genesis G90, så belöningen för att besegra en övermänsklig AI är 170 gånger Googles belöning för en Chrome-sandlåde- flykt. Hans förklaring: tidigt kopierade han AI-drag och förlorade; han vann genom att bygga brädet i sin egen stil, vilket är det mest användbara rådet om AI jag har hört i år, och det kom från ett brädspel. Två rader till i diffen.

4:22 Rust React Compiler från oxc är nu inbyggd i Vite bakom en flagga; en kodbas med 1 036 filer gick från 14,3 sekunder till 0,81 i kompileringssteget, mestadels genom att ta bort Babel från package.json, vilket också är min hudvårdsrutin. Och IBM lanserade Bob, en AI-kodningspartner som hälsar dig med Hej, jag är Bob, skapar underagenter, moderniserar stordator-kod, och lanserar en analysprodukt kallad Bobalytics, så någonstans är en bank mycket exalterad och ingen läste licensen.

4:51 Det är mycket marginal för en fredag; om du hellre läser detta än hör mig säga det, landar diffen i din inkorg varje morgon – gratis på the daily diff dot dev, länk nedan. Så, dagens dom: SHIP IT. Kärnan säger ja, Buzzard säger ja, matten ändrades inte, men sättet vi kontrollerar mattan ändrades precis. Det är dagens diff. Jag är Niko från Axrisi.

5:09 Sammanfoga ansvarsfullt.

## Källor

- [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