Claude het Fermat in 11 dae bewys. Uitspraak: SHIP IT.

Wat hierdie video dek

• Claude formaliseer Fermat se Laaste Stelling in Lean 4
• Chromium sandbox RCE (CVE-2026-85046), uitgebuit in die natuur, $1,000 beloning
• Shin Jin-seo klop KataGo met 'n twee-steen voorgee

Vertaalde transkripsie

Vertaal uit die oorspronklike Engelse vertelling. Beskikbare klank en onderskrifte word deur YouTube beheer.

0:00 Fermat het gesê sy wonderlike bewys sou nie in die kantlyn pas nie, en vandag het Anthropic die kantlyn gepubliseer: dertien miljoen reëls Lean, vyf keer die grootte van Mathlib, wat 'n stelling bewys wat elke wiskundige reeds geglo het. Dit was tien tot elf in Tbilisi toe Anthropic geplaas het, so natuurlik was ek wakker. Gister het Google Chrome 152 gestuur met twaalf sekuriteitsoplossings, een van hulle 'n V8-fout wat reeds in die natuur uitgebuit is, en die verslaggewer 'n duisend dollar betaal, wat minder is as die sedan waaroor ons later sal praat.

0:26 Ook gister het Mullvad gesê dit sluit sy publieke geënkripteerde DNS op 2 November en betaal Quad9 om dit eerder te doen, en vanoggend het die Rust React samesteller inheems geword in Vite, terwyl Hacker News IBM Bob ontdek het, 'n KI-koderingsagent. Toe het Claude Fermat se Laaste Stelling geformaliseer, en op dieselfde voorblad het 'n Koreaanse grootmeester die sterkste Go-enjin op Aarde geklop, so vandag het die mensdom een uit twee gekry. In hierdie video: wat Claude eintlik bewys het, wat dit gekos het,

0:52 hoekom die wiskundige wat sy loopbaan hieraan bestee het, sê dit verander niks en is in elk geval verheug, en hoe 'n mens die masjien by Go geklop het. Dis Vrydag, 4 September, en dit is The Daily Diff. Fermat se Laaste Stelling: geen positiewe heeltalle a, b, c voldoen aan a tot die n plus b tot die n gelyk aan c tot die n vir enige n bo 2 nie. Fermat het dit omstreeks 1637 in 'n kantlyn gekrabbel en gesterf sonder om sy werk te wys, wat hom die eerste ontwikkelaar gemaak het om 'n kaartjie met 'werks op my masjien' te sluit. 'n 1908 prys van 100,000 goudmarkte het 621 verkeerde

1:25 bewyse in sy eerste jaar gelok, en Andrew Wiles het dit uiteindelik in 1995 gekry, in 129 bladsye wat skeidsregters maande geneem het om te verifieer. Formalisering beteken om daardie bewys te herskryf sodat Lean, 'n bewysassistent, elke stap meganies kan kontroleer, en Kevin Buzzard by Imperial het 'n menslike poging gelei om presies dit te doen sedert 2024; die bloudruk alleen is 86 bladsye. Anthropic-navorser Tianyi Peng het dosyne Claude-agente daarop gerig in plaas daarvan, op 'n platform genaamd Prove2Me wat 'n DAG van stellinge hou sodat agente weet wat om volgende te bewys, want daarsonder het die eerste

2:00 swerms uit die oog verloor wie wat bewys het, wat gebeur wanneer jou orkestrasielaag regex is met 'n bemarkingsbegroting. Elf dae later het die wortelknoop gelees BEWYS: dertien miljoen reëls Lean, 29,500 tussentydse stellinge, ongeveer ses biljoen uitset-tokens van 'n interne model rofweg vergelykbaar met Claude Fable 5.1. Die bou misluk tensy die bewys presies op Lean se drie standaardaksiomas berus: nee jammer, geen inheemse besluit, geen verneukery nie. Om dit te kontroleer is ook nie goedkoop nie: 'n

2:29 van-voor-af bou het vyf en 'n half uur geneem op 96 kerne en 153 gigagrepe RAM, en die stellingname is masjien-gegenereer, so die repo beskryf homself as geskryf om gekontroleer eerder as gelees te word, wat ook is hoe ek onderneming Java sou beskryf. Nou die teenstrydigheid. Anthropic se pos sê Lean demonstreer korrektheid bo alle twyfel. Kevin Buzzard, die man wat daartoe verslaan is, het die repo op 'n 500-gigagrepe masjien wat Anthropic hom geleen het, gekompileer, bevestig dit is in orde, en toe geskryf,

2:56 aanhaling, wiskundig vertel hierdie werk ons eintlik niks. Hy was reeds 99.9 persent seker die stelling was waar, en die bewys voeg geen nuwe wiskunde by nie; wat dit wys, is wat outoformalisering nou kan doen, en daardie deel is hy opreg opgewonde oor. Hy is een miljoen pond oor vyf jaar gegee; Anthropic het elf dae geneem, en 'n kommentator se agter-op-die-servet berekening stel ses biljoen uitset-tokens teen lysprys ongeveer 300 000 dollar, so die masjien was goedkoper, tensy jy die opleiding van die masjien tel, wat niemand doen nie.

3:24 Beste detail: die e-pos het aangekom terwyl hy by 'n musiekfees in Wallis was met een strepie 4G, van 'n naam waarvan hy nog nooit gehoor het nie, so hy het dit afgeskryf as 'n grap en dit 'n week later gelees, wat die korrekte reaksie is op enige onderwerplyn wat end-tot-end formalisering bevat. Intussen het mense een teruggekry. Shin Jin-seo, die wêreld se nommer een in Go, het KataGo verslaan, die sterkste oopbron Go-enjin, twee wedstryde teen een in Seoel met 'n twee-steen gestremdheid, ongeveer die gaping tussen 'n top professionele en 'n beginner professionele.

3:50 Die beslissende wedstryd was 'n 11.5-punt oorwinning in 221 skuiwe, met 'n 99 persent wenwaarskynlikheid vanaf die middel van die wedstryd, en hy het 250 miljoen won huis toe geneem, ongeveer 170 000 dollar, plus 'n Genesis G90, so die beloning vir die verslaan van 'n supermenslike AI is 170 keer Google se beloning vir 'n Chrome-sandbox ontsnapping. Sy verduideliking: vroeg het hy AI-skuiwe gekopieer en verloor; hy het gewen deur die bord in sy eie styl te bou, wat die nuttigste advies oor AI is wat ek die hele jaar gehoor het, en dit het van 'n bordspel gekom. Nog twee reëls in The Daily Diff.

4:22 Die Rust React Compiler van oxc is nou inheems in Vite agter een vlag; 'n 1 036-lêer kodebasis het van 14.3 sekondes na 0.81 in die saamstelstap gegaan, meestal deur Babel uit package.json te verwyder, wat ook my velsorgroetine is. En IBM het Bob bekendgestel, 'n AI-koderingsvennoot wat jou groet met Hi, Ek is Bob, skep subagente, moderniseer hoofraamkode, en versprei 'n analitiese produk genaamd Bobalytics, so iewers is 'n bank baie opgewonde en niemand het die lisensie gelees nie.

4:51 Dit is baie marge vir een Vrydag; as jy dit eerder wil lees as my hoor sê, The Daily Diff land elke oggend in jou inkassie — gratis by the daily diff dot dev, skakel hieronder. So, vandag se uitspraak: SHIP IT. Die kern sê ja, Buzzard sê ja, die wiskunde het nie verander nie, maar die manier waarop ons wiskunde nagaan het pas verander. Dis vandag se The Daily Diff. Ek is Niko van Axrisi.

5:09 Voeg verantwoordelik saam.

Bronne

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