Claude a demonstrat teorema lui Fermat în 11 zile. Verdict: SHIP IT.

Ce acoperă acest videoclip

• Claude formalizează Ultima Teoremă a lui Fermat în Lean 4
• RCE în sandbox-ul Chromium (CVE-2026-85046), exploatată în sălbăticie, recompensă de 1.000 $
• Shin Jin-seo învinge KataGo cu un handicap de două pietre

Transcrierea tradusă

Tradus din narațiunea originală în engleză. Audio-ul și subtitrările disponibile sunt controlate de YouTube.

0:00 Fermat a spus că minunata sa demonstrație nu ar încăpea pe margine, iar astăzi Anthropic a publicat marginea: treisprezece milioane de linii de Lean, de cinci ori mărimea Mathlib, demonstrând o teoremă pe care fiecare matematician o credea deja. Era zece spre unsprezece în Tbilisi când Anthropic a postat, așa că, firesc, eram treaz. Ieri Google a lansat Chrome 152 cu doisprezece remedieri de securitate, una dintre ele o eroare V8 deja exploatată în sălbăticie, și a plătit reporterului o mie de dolari, ceea ce este mai puțin decât sedanul la care vom ajunge mai târziu.

0:26 Tot ieri, Mullvad a anunțat că își închide DNS-ul public criptat pe 2 noiembrie și că plătește Quad9 să facă asta în loc, iar în această dimineață compilatorul Rust React a devenit nativ în Vite, în timp ce Hacker News a descoperit IBM Bob, un agent de codare AI. Apoi Claude a formalizat Ultima Teoremă a lui Fermat, iar pe aceeași primă pagină un mare maestru coreean a învins cel mai puternic motor Go de pe Pământ, așa că astăzi omenirea a reușit unul din două. În acest videoclip: ce a demonstrat de fapt Claude, cât a costat,

0:52 de ce matematicianul care și-a petrecut cariera pe asta spune că nu schimbă nimic și este oricum entuziasmat, și cum un om a învins mașina la Go. Este vineri, 4 septembrie, și acesta este The Daily Diff. Ultima Teoremă a lui Fermat: nu există numere întregi pozitive a, b, c care să satisfacă a la puterea n plus b la puterea n egal c la puterea n pentru orice n mai mare de 2. Fermat a scris-o într-o margine în jurul anului 1637 și a murit fără să-și arate munca, făcându-l primul dezvoltator care a închis un tichet cu „funcționează pe mașina mea”. Un premiu din 1908 de 100.000 de mărci de aur a atras 621 de demonstrații greșite

1:25 în primul său an, iar Andrew Wiles a reușit-o în sfârșit în 1995, în 129 de pagini care au necesitat luni de verificare din partea arbitrilor. A formaliza înseamnă a rescrie acea demonstrație astfel încât Lean, un asistent de demonstrații, să poată verifica fiecare pas mecanic, iar Kevin Buzzard de la Imperial a condus un efort uman de a face exact asta din 2024; schița singură are 86 de pagini. Cercetătorul Anthropic Tianyi Peng a îndreptat zeci de agenți Claude către ea în schimb, pe o platformă numită Prove2Me care menține un DAG de enunțuri de teoreme astfel încât agenții să știe ce să demonstreze în continuare, deoarece fără ea primele

2:00 roiuri au pierdut evidența cine ce demonstra, ceea ce se întâmplă când stratul tău de orchestrare este regex cu un buget de marketing. Unsprezece zile mai târziu, nodul rădăcină citea DEMONSTRAT: treisprezece milioane de linii de Lean, 29.500 de teoreme intermediare, aproximativ șase miliarde de token-uri de ieșire dintr-un model intern aproximativ comparabil cu Claude Fable 5.1. Construcția eșuează dacă demonstrația nu se bazează exact pe cele trei axiome standard ale Lean: nu, îmi pare rău, nu decide nativ, nu trișa. Verificarea nu este nici ea ieftină: o

2:29 construcție de la zero a durat cinci ore și jumătate pe 96 de nuclee și 153 de gigabytes de RAM, iar numele teoremelor sunt generate automat, așa că depozitul se descrie ca fiind scris pentru a fi verificat mai degrabă decât citit, ceea ce este și cum aș descrie Java pentru întreprinderi. Acum contradicția. Postarea Anthropic spune că Lean demonstrează corectitudinea dincolo de orice îndoială. Kevin Buzzard, omul care a fost depășit, a compilat depozitul pe o mașină de 500 de gigabytes împrumutată de Anthropic, a confirmat că se verifică, și apoi a scris,

2:56 citat, „matematic, această lucrare nu ne spune nimic esențial”. Era deja 99,9 la sută sigur că teorema era adevărată, iar demonstrația nu adaugă nicio matematică nouă; ceea ce arată este ce poate face autoformalizarea acum, și acea parte îl entuziasmează cu adevărat. I s-au dat un milion de lire sterline pe cinci ani; Anthropic a avut nevoie de unsprezece zile, iar calculele rapide ale unui comentator plasează șase miliarde de token-uri de ieșire la prețul de listă în jur de 300.000 de dolari, deci mașina a fost mai ieftină, dacă nu cumva numărăm antrenarea mașinii, ceea ce nimeni nu face.

3:24 Cel mai bun detaliu: e-mailul a sosit în timp ce el era la un festival de muzică în Țara Galilor cu o bară de 4G, de la un nume despre care nu auzise niciodată, așa că l-a considerat o farsă și l-a citit o săptămână mai târziu, ceea ce este răspunsul corect la orice subiect care conține formalizare end-to-end. Între timp, oamenii au recuperat. Shin Jin-seo, numărul unu mondial la Go, a învins KataGo, cel mai puternic motor Go open-source, cu două jocuri la unul în Seul, cu un handicap de două pietre, aproximativ decalajul dintre un profesionist de top și un profesionist începător.

3:50 Decisivul a fost o victorie de 11,5 puncte în 221 de mutări, menținând o probabilitate de câștig de 99 la sută de la mijlocul jocului, și a luat acasă 250 de milioane de won, aproximativ 170.000 de dolari, plus un Genesis G90, deci recompensa pentru învingerea unei inteligențe artificiale supraumane este de 170 de ori recompensa Google pentru o evadare din sandbox-ul Chrome. Explicația sa: la început a copiat mișcările AI și a pierdut; a câștigat prin construirea tablei în stilul său propriu, ceea ce este cel mai util sfat despre AI pe care l-am auzit tot anul, și a venit de la un joc de societate. Încă două rânduri în diff.

4:22 Compilatorul Rust React de la oxc este acum nativ în Vite, în spatele unui singur flag; o bază de cod de 1.036 de fișiere a trecut de la 14,3 secunde la 0,81 în etapa de compilare, în mare parte prin ștergerea Babel din package.json, care este și rutina mea de îngrijire a pielii. Și IBM a lansat Bob, un partener de codare AI care te întâmpină cu Salut, Sunt Bob, generează subagenți, modernizează codul mainframe, și livrează un produs de analiză numit Bobalytics, așa că undeva o bancă este foarte încântată și nimeni nu a citit licența.

4:51 Aceasta este o mulțime de marjă pentru o vineri; dacă preferați să citiți asta decât să mă auziți spunând-o, diff-ul ajunge în căsuța dvs. de e-mail în fiecare dimineață — gratuit la the daily diff dot dev, link mai jos. Deci, verdictul de azi: SHIP IT. Kernel-ul spune da, Buzzard spune da, matematica nu s-a schimbat, dar modul în care verificăm matematica tocmai s-a schimbat. Acesta este diff-ul de azi. Sunt Niko de la Axrisi.

5:09 Fuzionați responsabil.

Surse

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