Claude tõestas Fermati 11 päevaga. Otsus: SHIP IT.

Mida see video hõlmab

• Claude formaliseerib Fermati viimase teoreemi Lean 4-s
• Chromiumi liivakasti RCE (CVE-2026-85046), mida ekspluateeritakse aktiivselt, 1000 $ preemia
• Shin Jin-seo võidab KataGo'd kahekivise puudega

Tõlgitud transkriptsioon

Tõlgitud ingliskeelsest originaaljutustusest. Saadaolevat heli ja subtiitreid kontrollib YouTube.

0:00 Fermat ütles, et tema imeline tõestus ei mahuks marginaali, ja täna avaldas Anthropic marginaali: kolmteist miljonit rida Lean'i, viis korda suurem kui Mathlib, tõestades teoreemi, millesse iga matemaatik juba uskus. Tbilisis oli kümme kuni üksteist, kui Anthropic postitas, nii et loomulikult olin ma ärkvel. Eile tarnis Google Chrome 152 koos kaheteistkümne turvaparandusega, üks neist V8 viga, mida juba aktiivselt ära kasutati, ja maksis teatajale tuhat dollarit, mis on vähem kui sedaan, milleni me hiljem jõuame.

0:26 Samuti eile teatas Mullvad, et sulgeb oma avaliku krüpteeritud DNS-i 2. novembril ja maksab Quad9-le, et see seda selle asemel teeks, ja täna hommikul muutus Rust React kompilaator Vite'is algupäraseks, samal ajal kui Hacker News avastas IBM Bob'i, AI kodeerimisagendi. Seejärel formaliseeris Claude Fermati viimase teoreemi ja samal esilehel Korea suurmeister võitis Maa tugevaimat Go mootorit, nii et täna sai inimkond ühe kahele. Selles videos: mida Claude tegelikult tõestas, mida see maksis,

0:52 miks matemaatik, kes oma karjääri sellele pühendas, ütleb, et see ei muuda midagi ja on sellest hoolimata vaimustuses, ja kuidas inimene võitis masinat Go-s. On reede, 4. september, ja see on The Daily Diff. Fermati viimane teoreem: pole positiivseid täisarve a, b, c, mis rahuldaksid a astmes n pluss b astmes n võrdub c astmes n, kui n on suurem kui 2. Fermat kritseldas selle marginaali umbes 1637. aastal ja suri oma tööd näitamata, tehes temast esimese arendaja, kes sulges pileti, millega töötab minu masin. 1908. aasta 100 000 kuldmarga preemia meelitas esimesel aastal 621 vale

1:25 tõestust ja Andrew Wiles sai selle lõpuks 1995. aastal, 129 leheküljel, mille kontrollimiseks kulus kohtunikel kuid. Formaliseerimine tähendab selle tõestuse ümberkirjutamist nii, et Lean, tõestusassistent, saaks iga sammu mehaaniliselt kontrollida, ja Kevin Buzzard Imperial College'ist on juhtinud inimlikku pingutust seda teha alates 2024. aastast; ainuüksi sinine trükis on 86 lehekülge. Anthropicu teadlane Tianyi Peng suunas sellele kümneid Claude'i agente platvormil nimega Prove2Me, mis hoiab teoreemide DAG-i, nii et agendid teaksid, mida järgmisena tõestada, sest ilma selleta kaotasid esimesed

2:00 parved jälje, kes mida tõestas, mis juhtub, kui teie orkestratsioonikiht on regex turunduseelarvega. Üksteist päeva hiljem luges juursõlm PROOVID: kolmteist miljonit rida Lean'i, 29 500 vahepealset teoreemi, umbes kuus miljardit väljundmärki sisemudelist, mis on ligikaudu võrreldav Claude Fable 5.1-ga. Ehitus ebaõnnestub, kui tõestus ei tugine täpselt Leani kolmele standardaksioomile: vabandust, ei mingit natiivset otsustamist, ei mingit petmist. Selle kontrollimine pole ka odav: nullist

2:29 ehitus võttis viis ja pool tundi 96 tuumal ja 153 gigabaidil RAM-il, ja teoreemide nimed on masina loodud, nii et hoidla kirjeldab end kirjutatuna pigem kontrollimiseks kui lugemiseks, mis on ka see, kuidas ma kirjeldaksin ettevõtte Java-t. Nüüd vastuolu. Anthropicu postitus ütleb, et Lean demonstreerib õigsust kahtlemata. Kevin Buzzard, mees, kellelt see eest ära võeti, kompileeris hoidla 500-gigabaidisele masinale, mille Anthropic talle laenas, kinnitas selle õigsust ja kirjutas siis,

2:56 tsitaat, matemaatiliselt ei anna see töö meile sisuliselt midagi. Ta oli juba 99,9 protsenti kindel, et teoreem on tõene, ja tõestus ei lisa uut matemaatikat; see näitab, mida autoformaliseerimine suudab nüüd teha, ja see osa teda tõeliselt erutab. Talle anti miljon naela viie aasta jooksul; Anthropicul kulus üksteist päeva, ja kommentaatori tagaküljel tehtud arvutused hindavad kuut miljardit väljundmärki jaehinna järgi. umbes 300 000 dollarit, seega oli masin odavam, välja arvatud juhul, kui arvestada masina koolitamist, mida keegi ei tee.

3:24 Parim detail: e-kiri saabus ajal, mil ta oli Walesis muusikafestivalil ühe 4G leviala pulgaga, nimelt, mida ta polnud kunagi kuulnud, nii et ta pidas seda naljaks ja luges seda nädal hiljem, mis on õige vastus igale teemareale, mis sisaldab täielikku formaliseerimist. Samal ajal said inimesed ühe tagasi. Shin Jin-seo, maailma Go number üks, võitis KataGo, tugevaima avatud lähtekoodiga Go mootori, kaks mängu ühe vastu Soulis kahe kiviga händikäpiga, mis on umbes tippprofessionaali ja algaja professionaali vahe.

3:50 Otsustavaks oli 11,5-punktiline võit 221 käiguga, hoides 99-protsendilist võidu tõenäosust mängu keskpaigast alates, ja ta võitis 250 miljonit woni, umbes 170 000 dollarit, pluss Genesis G90, nii et tasu üliohumanoidse tehisintellekti võitmise eest on 170 korda Google'i tasust Chrome'i liivakasti põgenemise eest. Tema selgitus: alguses kopeeris ta tehisintellekti käike ja kaotas; ta võitis ehitades laua oma stiilis, mis on kõige kasulikum nõuanne tehisintellekti kohta, mida ma sel aastal kuulnud olen, ja see tuli lauamängust. Veel kaks rida diffis.

4:22 Rust React Compiler ettevõttelt oxc on nüüd Vite'is natiivne ühe lipu taga; a 1036-failine koodibaas läks 14,3 sekundist 0,81-ni kompileerimisetapis, peamiselt eemaldades Babeli package.json'ist, mis on ka minu nahahooldusrutiin. Ja IBM tõi turule Bobi, tehisintellekti kodeerimispartneri, mis tervitab teid sõnaga Tere, olen Bob, loob alamagente, moderniseerib põhiprogrammide koodi, ja toodab analüütikatoote nimega Bobalytics, nii et kusagil on pank väga põnevil ja keegi ei lugenud litsentsi.

4:51 See on ühe reede kohta palju varu; kui eelistaksite seda lugeda, mitte kuulda mind seda ütlemas, siis diff jõuab teie postkasti igal hommikul – tasuta aadressil the daily diff dot dev, link allpool. Niisiis, tänane otsus: SHIP IT. Kernel ütleb jah, Buzzard ütleb jah, matemaatika ei muutunud, kuid viis, kuidas me matemaatikat kontrollime, just muutus. See on tänane diff. Olen Niko Axrisist.

5:09 Ühendage vastutustundlikult.

Allikad

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