Claude sannaði Fermat á 11 dögum. Niðurstaða: SHIP IT.

Það sem þetta myndband fjallar um

• Claude formgerir Síðustu setningu Fermats í Lean 4
• Chromium sandkassakerfi RCE (CVE-2026-85046), nýtt í náttúrunni, $1.000 verðlaun
• Shin Jin-seo sigrar KataGo með tveggja steina forgjöf

Þýtt afrit

Þýtt úr upprunalegri enskri frásögn. Tiltækt hljóð og textar eru stjórnaðir af YouTube.

0:00 Fermat sagði að dásamleg sönnun hans myndi ekki passa á spássíuna, og í dag birti Anthropic spássíuna: þrettán milljónir lína af Lean, fimm sinnum stærri en Mathlib, sem sannaði setningu sem allir stærðfræðingar þegar trúðu. Klukkan var tíu eða ellefu í Tíblísi þegar Anthropic birti, svo ég var náttúrulega vakandi. Í gær sendi Google út Chrome 152 með tólf öryggislagfæringum, einn þeirra var V8 galli sem þegar var nýttur í náttúrunni, og greiddi skýrsluhöfundinum þúsund dollara, sem er minna en fólksbíllinn sem við munum koma að seinna.

0:26 Einnig í gær, sagði Mullvad að það væri að loka opinberri dulkóðuðu DNS þjónustu sinni þann 2. nóvember og borga Quad9 fyrir að gera það í staðinn, og í morgun varð Rust React Compiler innfæddur í Vite, á meðan Hacker News uppgötvaði IBM Bob, AI kóðunarumboðsmann. Síðan formgerði Claude Síðustu setningu Fermats, og á sömu forsíðu kóreskur stórmeistari sigraði sterkustu Go vél á Jörðu, svo í dag gekk mannkynið einn af tveimur. Í þessu myndbandi: hvað Claude sannaði í raun, hvað það kostaði,

0:52 hvers vegna stærðfræðingurinn sem eyddi ferli sínum í þetta segir að það breyti engu og er ánægður engu að síður, og hvernig maður sigraði vélina í Go. Það er föstudagur 4. september og þetta er The Daily Diff. Síðasta setning Fermats: engar jákvæðar heiltölur a, b, c uppfylla a í n-veldi plús b í n-veldi jafnt og c í n-veldi fyrir neitt n yfir 2. Fermat skrifaði þetta á spássíu um 1637 og dó án þess að sýna vinnu sína, sem gerði hann að fyrsta forritaranum til að loka miða með „virkar á minni vél“. Verðlaun upp á 100.000 gullmerki árið 1908 laðuðu að sér 621 ranga

1:25 sönnun á fyrsta ári, og Andrew Wiles náði því loks árið 1995, á 129 síðum sem tók dómurum mánuði að sannreyna. Að formgera þýðir að endurskrifa þessa sönnun svo Lean, sönnunaraðstoðartæki, getur athugað hvert skref vélrænt, og Kevin Buzzard hjá Imperial hefur leitt mannlega viðleitni til að gera einmitt það síðan 2024; teikningin ein og sér er 86 síður. Anthropic rannsakandinn Tianyi Peng beindi tugum Claude umboðsmanna að því í staðinn, á vettvangi sem kallast Prove2Me sem heldur DAG af setninga yfirlýsingum svo umboðsmenn vita hvað á að sanna næst, því án þess misstu fyrstu

2:00 sveitirnar yfirsýn yfir hver var að sanna hvað, sem er það sem gerist þegar stýringarlagið þitt er regex með markaðsfjárhagsáætlun. Ellefu dögum síðar stóð á rótareiningunni SÖNNUÐ: þrettán milljónir lína af Lean, 29.500 millisetningar, um sex milljarðar útkomutákn frá innra líkani sem er nokkurn veginn sambærilegt við Claude Fable 5.1. Smíðin mistekst nema sönnunin byggi á nákvæmlega þremur staðalfrumsetningum Lean: nei fyrirgefðu, engin innbyggð ákvörðun, engin svindl. Að athuga það er heldur ekki ódýrt:

2:29 nýsmíði tók fimm og hálfa klukkustund á 96 kjörnum og 153 gígabætum af vinnsluminni, og setninganöfnin eru vélrænt mynduð, svo geymslan lýsir sér sem skrifaðri til að athuga frekar en lesa, sem er líka hvernig ég myndi lýsa Enterprise Java. Nú mótsögnin. Færsla Anthropic segir að Lean sanni réttmæti umfram allan vafa. Kevin Buzzard, maðurinn sem varð undanfærinn, tók saman geymsluna á 500 gígabæta vél sem Anthropic lánaði honum, staðfesti að hún stenst, og skrifaði síðan,

2:56 tilvitnun, stærðfræðilega séð segir þessi vinna okkur í raun ekkert. Hann var þegar 99,9 prósent viss um að setningin væri sönn, og sönnunin bætir engri nýrri stærðfræði við; það sem hún sýnir er hvað sjálfvirk formgerð getur gert núna, og sá hluti er hann einlæglega spenntur fyrir. Hann fékk eina milljón punda á fimm árum; Anthropic tók ellefu daga, og servíettureikningur athugasemdarmanns metur sex milljarða útkomutákn á listaverði um 300.000 dali, svo vélin var ódýrari, nema þú teljir þjálfun vélarinnar, sem enginn gerir.

3:24 Bestu smáatriði: tölvupósturinn kom á meðan hann var á tónlistarhátíð í Wales með einni 4G móttöku, frá nafni sem hann hafði aldrei heyrt um, svo hann afskrifaði það sem gabb og las það viku síðar, sem er rétta viðbragðið við hvaða efnislínu sem er sem inniheldur end-to-end formfestingu. Á meðan fengu mennirnir einn sigur. Shin Jin-seo, heimsmeistari númer eitt í Go, sigraði KataGo, öflugasta opinn-uppspretta Go vélina, í tveimur leikjum gegn einum í Seúl með tveggja steina forgjöf, nokkurn veginn bilið á milli topp atvinnumanns og nýliða atvinnumanns.

3:50 Úrslitaleikurinn var 11,5 stiga sigur í 221 leik, og hélt 99 prósent líkur á sigri frá miðjum leik og áfram, og hann tók heim 250 milljónir won, um 170.000 dali, auk Genesis G90, svo verðlaunin fyrir að sigra ofurmannlega gervigreind eru 170 sinnum verðlaun Google fyrir Chrome sandkassa flótta. Skýring hans: snemma í leiknum afritaði hann gervigreindar leiki og tapaði; hann vann með því að byggja borðið upp í sínum eigin stíl, sem eru gagnlegustu ráðin um gervigreind sem ég hef heyrt allt árið, og þau komu frá borðspili. Tvær línur í viðbót í diff.

4:22 Rust React Compiler frá oxc er nú innfæddur í Vite á bak við einn fána; 1.036 skráa kóðagrunnur fór úr 14,3 sekúndum í 0,81 í þýðingarferlinu, að mestu leyti með því að eyða Babel úr package.json, sem er líka húðumhirðuvenjan mín. Og IBM sendi frá sér Bob, gervigreindar kóðunarfélaga sem heilsar þér með „Hæ, ég er Bob“, býr til undirumboðsmenn, nútímavæðir aðalkóða, og sendir frá sér greiningarvöru sem heitir Bobalytics, svo einhvers staðar er banki mjög spenntur og enginn las leyfisskilmálana.

4:51 Þetta er mikil framlegð fyrir einn föstudag; ef þú vilt frekar lesa þetta en heyra mig segja það, þá lendir diff í pósthólfinu þínu á hverjum morgni — ókeypis á The Daily Diff dot dev, hlekkur hér að neðan. Svo, dómur dagsins: SHIP IT. Kjarninn segir já, Buzzard segir já, stærðfræðin breyttist ekki, en hvernig við athugum stærðfræði breyttist nýlega. Þetta er The Daily Diff í dag. Ég er Niko frá Axrisi.

5:09 Samruni á ábyrgan hátt.

Heimildir

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