Claude bewees Fermat in 11 dagen. Oordeel: SHIP IT.

Wat deze video behandelt

• Claude formaliseert de laatste stelling van Fermat in Lean 4
• Chromium sandbox RCE (CVE-2026-85046), uitgebuit in het wild, $1.000 beloning
• Shin Jin-seo verslaat KataGo met een handicap van twee stenen

Vertaald transcript

Vertaald vanuit de originele Engelse gesproken tekst. Beschikbare audio en ondertiteling worden beheerd door YouTube.

0:00 Fermat zei dat zijn wonderbaarlijke bewijs niet in de marge zou passen, en vandaag publiceerde Anthropic de marge: dertien miljoen regels Lean, vijf keer de grootte van Mathlib, die een stelling bewijst die elke wiskundige al geloofde. Het was tien voor elf in Tbilisi toen Anthropic postte, dus natuurlijk was ik wakker. Gisteren leverde Google Chrome 152 met twaalf beveiligingsoplossingen, waarvan één een V8-bug die al in het wild werd uitgebuit, en betaalde de melder duizend dollar, wat minder is dan de sedan waar we later op terugkomen.

0:26 Ook gisteren zei Mullvad dat het zijn openbare versleutelde DNS op 2 november zou sluiten en Quad9 zou betalen om het in plaats daarvan te doen, en vanochtend ging de Rust React Compiler native in Vite, terwijl Hacker News IBM Bob ontdekte, een AI-coderingagent. Toen formaliseerde Claude de laatste stelling van Fermat, en op dezelfde voorpagina versloeg een Koreaanse grootmeester de sterkste Go-engine op Aarde, dus vandaag heeft de mensheid één van de twee gewonnen. In deze video: wat Claude daadwerkelijk bewees, wat het kostte,

0:52 waarom de wiskundige die zijn carrière hieraan heeft besteed zegt dat het niets verandert en toch opgetogen is, en hoe een mens de machine versloeg bij Go. Het is vrijdag 4 september, en dit is The Daily Diff. De laatste stelling van Fermat: geen positieve gehele getallen a, b, c voldoen aan a tot de n plus b tot de n is gelijk aan c tot de n voor elke n boven de 2. Fermat krabbelde het rond 1637 in een marge en stierf zonder zijn werk te laten zien, waardoor hij de eerste ontwikkelaar was die een ticket sloot met 'werkt op mijn machine'. Een prijs van 100.000 goudmarken in 1908 trok 621 verkeerde

1:25 bewijzen aan in het eerste jaar, en Andrew Wiles kreeg het uiteindelijk in 1995, in 129 pagina's die scheidsrechters maanden kostten om te verifiëren. Formaliseren betekent het herschrijven van dat bewijs zodat Lean, een bewijsassistent, elke stap mechanisch kan controleren, en Kevin Buzzard van Imperial leidt sinds 2024 een menselijke inspanning om precies dat te doen; alleen al de blauwdruk is 86 pagina's lang. Anthropic-onderzoeker Tianyi Peng richtte tientallen Claude-agenten hierop in plaats daarvan, op een platform genaamd Prove2Me dat een DAG van stellinguitspraken bijhoudt zodat agenten weten wat ze vervolgens moeten bewijzen, want zonder dit raakten de eerste

2:00 zwermen het spoor kwijt van wie wat aan het bewijzen was, wat er gebeurt wanneer je orkestratielaag regex is met een marketingbudget. Elf dagen later las het hoofdknooppunt BEWEZEN: dertien miljoen regels Lean, 29.500 tussentijdse stellingen, ongeveer zes miljard uitvoertokens van een intern model dat ruwweg vergelijkbaar is met Claude Fable 5.1. De build mislukt tenzij het bewijs berust op precies de drie standaardaxtioma's van Lean: nee sorry, geen native decide, niet valsspelen. Het controleren is ook niet goedkoop: een

2:29 van-nul-af-opbouw duurde vijf en een half uur op 96 cores en 153 gigabytes RAM, en de stellingnamen zijn machinaal gegenereerd, dus de repo beschrijft zichzelf als geschreven om gecontroleerd te worden in plaats van gelezen, wat ook is hoe ik enterprise Java zou beschrijven. Nu de tegenspraak. Anthropic's bericht zegt dat Lean de correctheid buiten kijf stelt. Kevin Buzzard, de man die verslagen werd, compileerde de repo op een 500-gigabyte machine die Anthropic hem leende, bevestigde dat het klopt, en schreef toen,

2:56 citaat, wiskundig gezien vertelt dit werk ons in essentie niets. Hij was al 99,9 procent zeker dat de stelling waar was, en het bewijs voegt geen nieuwe wiskunde toe; wat het wel laat zien is wat autoformalisering nu kan doen, en dat deel is hij oprecht enthousiast over. Hij kreeg één miljoen pond over vijf jaar; Anthropic deed er elf dagen over, en een servetberekening van een commenter schat zes miljard uitvoertokens tegen de catalogusprijs. ongeveer 300.000 dollar, dus de machine was goedkoper, tenzij je de training van de machine meetelt, wat niemand doet.

3:24 Beste detail: de e-mail arriveerde terwijl hij op een muziekfestival in Wales was met één streepje 4G, van een naam waar hij nog nooit van had gehoord, dus hij schreef het af als een grap en las het een week later, wat de juiste reactie is op elke onderwerpregel die end-to-end formalisering bevat. Intussen sloegen mensen terug. Shin Jin-seo, de nummer één van de wereld in Go, versloeg KataGo, de sterkste open-source Go-engine, met twee games tegen één in Seoul met een twee-steens handicap, ruwweg het verschil tussen een top professional en een rookie professional.

3:50 De beslissende game was een overwinning van 11,5 punten in 221 zetten, met een 99 procent winstkans vanaf halverwege de game, en hij nam 250 miljoen won mee naar huis, ongeveer 170.000 dollar, plus een Genesis G90, dus de beloning voor het verslaan van een bovenmenselijke AI is 170 keer Google's beloning voor een Chrome sandbox escape. Zijn verklaring: in het begin kopieerde hij AI-zetten en verloor; hij won door het bord in zijn eigen stijl op te bouwen, wat het nuttigste advies over AI is dat ik dit jaar heb gehoord, en het kwam van een bordspel. Nog twee regels in de diff.

4:22 De Rust React Compiler van oxc is nu native in Vite achter één vlag; een codebase van 1.036 bestanden ging van 14,3 seconden naar 0,81 in de compileerstap, voornamelijk door Babel te verwijderen uit package.json, wat ook mijn huidverzorgingsroutine is. En IBM lanceerde Bob, een AI-codeerpartner die je begroet met Hi, I'm Bob, subagents spawnt, mainframecode moderniseert, en een analytics-product genaamd Bobalytics levert, dus ergens is een bank erg enthousiast en niemand heeft de licentie gelezen.

4:51 Dat is veel marge voor één vrijdag; als je dit liever leest dan mij het hoort zeggen, de diff landt elke ochtend in je inbox — gratis op the daily diff dot dev, link hieronder. Dus, het oordeel van vandaag: SHIP IT. De kernel zegt ja, Buzzard zegt ja, de wiskunde is niet veranderd, maar de manier waarop we de wiskunde controleren wel. Dat is de diff van vandaag. Ik ben Niko van Axrisi.

5:09 Verantwoord samenvoegen.

Bronnen

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