Claude ha dimostrato Fermat in 11 giorni. Verdetto: SHIP IT.

Contenuto di questo video

• Claude formalizza l'Ultimo Teorema di Fermat in Lean 4
• RCE nella sandbox di Chromium (CVE-2026-85046), sfruttata attivamente, ricompensa di 1.000 $
• Shin Jin-seo batte KataGo con un handicap di due pietre

Trascrizione tradotta

Tradotto dalla narrazione originale inglese. L'audio e i sottotitoli disponibili sono controllati da YouTube.

0:00 Fermat disse che la sua meravigliosa dimostrazione non sarebbe entrata nel margine, e oggi Anthropic ha pubblicato il margine: tredici milioni di righe di Lean, cinque volte la dimensione di Mathlib, che dimostrano un teorema che ogni matematico già credeva. Erano le dieci e undici a Tbilisi quando Anthropic ha postato, quindi naturalmente ero sveglio. Ieri Google ha rilasciato Chrome 152 con dodici correzioni di sicurezza, uno di questi un bug di V8 già sfruttato attivamente, e ha pagato al segnalatore mille dollari, che è meno della berlina di cui parleremo più avanti.

0:26 Sempre ieri, Mullvad ha dichiarato che chiuderà il suo DNS pubblico crittografato il 2 novembre e pagherà Quad9 per farlo al suo posto, e questa mattina il Rust React Compiler è diventato nativo in Vite, mentre Hacker News ha scoperto IBM Bob, un agente di codifica AI. Poi Claude ha formalizzato l'Ultimo Teorema di Fermat, e sulla stessa prima pagina un gran maestro coreano ha battuto il più forte motore di Go sulla Terra, quindi oggi l'umanità ha fatto uno su due. In questo video: cosa ha effettivamente dimostrato Claude, quanto è costato,

0:52 perché il matematico che ha passato la sua carriera su questo dice che non cambia nulla e è comunque entusiasta, e come un essere umano ha battuto la macchina a Go. È venerdì 4 settembre, e questo è The Daily Diff. L'Ultimo Teorema di Fermat: nessun intero positivo a, b, c soddisfa a alla n più b alla n uguale c alla n per qualsiasi n maggiore di 2. Fermat lo scarabocchiò in un margine intorno al 1637 e morì senza mostrare il suo lavoro, facendone il primo sviluppatore a chiudere un ticket con works on my machine. Un premio del 1908 di 100.000 marchi d'oro attirò 621 sbagliate

1:25 dimostrazioni nel suo primo anno, e Andrew Wiles finalmente lo ottenne nel 1995, in 129 pagine che richiesero mesi ai revisori per essere verificate. Formalizzare significa riscrivere quella dimostrazione in modo che Lean, un assistente di dimostrazione, possa controllare ogni passaggio meccanicamente, e Kevin Buzzard all'Imperial ha guidato uno sforzo umano per fare esattamente questo dal 2024; il solo progetto di massima è di 86 pagine. Il ricercatore di Anthropic Tianyi Peng ha invece puntato decine di agenti Claude su di esso, su una piattaforma chiamata Prove2Me che mantiene un DAG di affermazioni di teoremi in modo che gli agenti sappiano cosa dimostrare dopo, perché senza di essa i primi

2:00 sciami perdevano traccia di chi stava dimostrando cosa, che è quello che succede quando il tuo livello di orchestrazione è regex con un budget di marketing. Undici giorni dopo il nodo radice leggeva PROVED: tredici milioni di righe di Lean, 29.500 teoremi intermedi, circa sei miliardi di token di output da un modello interno all'incirca paragonabile a Claude Fable 5.1. La compilazione fallisce a meno che la dimostrazione non si basi esattamente sui tre assiomi standard di Lean: no mi dispiace, nessun decide nativo, nessun imbroglio. Anche controllarla non è economico: una

2:29 compilazione da zero ha richiesto cinque ore e mezza su 96 core e 153 gigabyte di RAM, e i nomi dei teoremi sono generati automaticamente, quindi il repository si descrive come scritto per essere controllato piuttosto che letto, che è anche come descriverei Java Enterprise. Ora la contraddizione. Il post di Anthropic dice che Lean dimostra la correttezza al di là di ogni dubbio. Kevin Buzzard, l'uomo che è stato battuto, ha compilato il repository su una macchina da 500 gigabyte che Anthropic gli ha prestato, ha confermato che funziona, e poi ha scritto,

2:56 citazione, matematicamente questo lavoro non ci dice essenzialmente nulla. Era già sicuro al 99,9 percento che il teorema fosse vero, e la dimostrazione non aggiunge nuova matematica; ciò che mostra è ciò che l'autoformalizzazione può fare ora, e di quella parte è sinceramente entusiasta. Gli era stato dato un milione di sterline in cinque anni; Anthropic ha impiegato undici giorni, e il calcolo su un tovagliolo di un commentatore stima sei miliardi di token di output al prezzo di listino circa 300.000 dollari, quindi la macchina era più economica, a meno che non si conti l'addestramento della macchina, cosa che nessuno fa.

3:24 Miglior dettaglio: l'email è arrivata mentre era a un festival musicale in Galles con una tacca di 4G, da un nome che non aveva mai sentito, quindi l'ha liquidata come uno scherzo e l'ha letta una settimana dopo, che è la risposta corretta a qualsiasi oggetto contenente formalizzazione end-to-end. Nel frattempo, gli umani hanno recuperato. Shin Jin-seo, il numero uno al mondo nel Go, ha battuto KataGo, il più forte motore Go open-source, due partite a uno a Seul con un handicap di due pietre, più o meno il divario tra un professionista di alto livello e un professionista alle prime armi.

3:50 La partita decisiva è stata una vittoria di 11,5 punti in 221 mosse, mantenendo una probabilità di vittoria del 99 percento da metà partita in poi, e ha portato a casa 250 milioni di won, circa 170.000 dollari, più una Genesis G90, quindi la ricompensa per aver battuto un'IA superumana è 170 volte la ricompensa di Google per una fuga dalla sandbox di Chrome. La sua spiegazione: all'inizio ha copiato le mosse dell'IA e ha perso; ha vinto costruendo la scacchiera nel suo stile, che è il consiglio più utile sull'IA che io abbia sentito quest'anno, e veniva da un gioco da tavolo. Altre due righe nel diff.

4:22 Il Rust React Compiler di oxc è ora nativo in Vite dietro una sola flag; una base di codice di 1.036 file è passata da 14,3 secondi a 0,81 nel passo di compilazione, principalmente eliminando Babel da package.json, che è anche la mia routine di cura della pelle. E IBM ha lanciato Bob, un partner di coding AI che ti saluta con Ciao, sono Bob, genera sotto-agenti, modernizza il codice mainframe, e distribuisce un prodotto di analisi chiamato Bobalytics, quindi da qualche parte una banca è molto entusiasta e nessuno ha letto la licenza.

4:51 È un sacco di margine per un venerdì; se preferisci leggere questo piuttosto che sentirmi dirlo, il diff arriva nella tua casella di posta ogni mattina — gratuito su the daily diff dot dev, link qui sotto. Quindi, il verdetto di oggi: SHIP IT. Il kernel dice sì, Buzzard dice sì, la matematica non è cambiata, ma il modo in cui controlliamo la matematica sì. Questo è il diff di oggi. Sono Niko di Axrisi.

5:09 Fondi responsabilmente.

Fonti

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