Claude todisti Fermatin 11 päivässä. Tuomio: SHIP IT.

Mitä tämä video käsittelee

• Claude formalisoi Fermatin viimeisen lauseen Lean 4:ssä
• Chromium-hiekkalaatikon RCE (CVE-2026-85046), jota hyödynnetään tosielämässä, 1 000 dollarin palkkio
• Shin Jin-seo voittaa KataGon kahden kiven tasoituksella

Käännetty transkriptio

Käännetty alkuperäisestä englanninkielisestä selostuksesta. Käytettävissä olevan äänen ja tekstitysten hallinta tapahtuu YouTuben kautta.

0:00 Fermat sanoi, että hänen upea todistuksensa ei mahtuisi reunukseen, ja tänään Anthropic julkaisi reunuksen: kolmetoista miljoonaa riviä Leania, viisi kertaa Mathlibin kokoinen, todistaen lauseen, jonka jokainen matemaatikko jo uskoi. Kello oli kymmenen tai yksitoista Tbilisissä, kun Anthropic julkaisi, joten luonnollisesti olin hereillä. Eilen Google julkaisi Chrome 152:n kahdellatoista tietoturvakorjauksella, yksi niistä V8-virhe, jota jo hyödynnettiin luonnossa, ja maksoi ilmoittajalle tuhat dollaria, mikä on vähemmän kuin sedan, johon palaamme myöhemmin.

0:26 Myös eilen Mullvad ilmoitti sulkevansa julkisen salatun DNS:nsä marraskuun 2. päivänä ja maksavansa Quad9:lle sen tekemisestä, ja tänä aamuna Rust React Compiler siirtyi natiiviksi Vitessa, kun taas Hacker News löysi IBM Bobin, tekoälyllä toimivan koodausagentin. Sitten Claude formalisoi Fermatin viimeisen lauseen, ja samalla etusivulla korealainen suurmestari voitti Maapallon vahvimman Go-moottorin, joten tänään ihmiskunta on yksi kahdesta. Tässä videossa: mitä Claude todella todisti, mitä se maksoi,

0:52 miksi matemaatikko, joka vietti uransa tähän, sanoo sen ei muuttavan mitään ja on joka tapauksessa innoissaan, ja miten ihminen voitti koneen Gossa. On perjantai, syyskuun 4. päivä, ja tämä on The Daily Diff. Fermatin viimeinen lause: ei ole olemassa positiivisia kokonaislukuja a, b, c, jotka täyttäisivät a potenssiin n plus b potenssiin n yhtä suuri kuin c potenssiin n millekään n:lle yli 2:n. Fermat kirjoitti sen reunukseen noin vuonna 1637 ja kuoli näyttämättä työtään, tehden hänestä ensimmäisen kehittäjän, joka sulki tiketin toimii omalla koneella. Vuoden 1908 100 000 kultamarkan palkinto houkutteli 621 väärää

1:25 todistusta ensimmäisenä vuotenaan, ja Andrew Wiles sai sen lopulta vuonna 1995, 129 sivulla, joiden tarkistamiseen tuomareilta meni kuukausia. Formalisointi tarkoittaa tuon todistuksen uudelleenkirjoittamista niin, että Lean, todistusavustin, voi tarkistaa jokaisen vaiheen mekaanisesti, ja Kevin Buzzard Imperialissa on johtanut ihmisen pyrkimyksiä tehdä juuri niin vuodesta 2024 lähtien; pelkkä suunnitelma on 86 sivua. Anthropicin tutkija Tianyi Peng ohjasi kymmeniä Claude-agentteja siihen sen sijaan, Prove2Me-nimisellä alustalla, joka pitää teoremalausuntojen DAG-puuta jotta agentit tietävät, mitä todistaa seuraavaksi, koska ilman sitä ensimmäiset

2:00 parvet menettivät käsityksen siitä, kuka todisti mitä, mikä tapahtuu, kun orkestrointikerroksesi on säännöllinen lauseke markkinointibudjetilla. Yhdentoista päivän kuluttua juurisolmu luki PROVED: kolmetoista miljoonaa riviä Leania, 29 500 väliteoreemaa, noin kuusi miljardia tuotostokenia sisäisestä mallista, joka on suunnilleen verrattavissa Claude Fable 5.1:een. Koonti epäonnistuu, ellei todistus perustu täsmälleen Leanin kolmeen standardiaksioomaan: ei anteeksi, ei natiivia päätöstä, ei huijausta. Sen tarkistaminen ei myöskään ole halpaa: a

2:29 tyhjästä tehty koonti kesti viisi ja puoli tuntia 96 ytimellä ja 153 gigatavulla RAM-muistia, ja teoreemien nimet ovat koneellisesti luotuja, joten repo kuvailee itseään kirjoitetuksi tarkistettavaksi mieluummin kuin luettavaksi, mikä on myös tapa, jolla kuvailisin yritys-Javaa. Nyt ristiriita. Anthropicin postaus sanoo, että Lean osoittaa oikeellisuuden epäilyksettömästi. Kevin Buzzard, mies, joka jäi toiseksi, kokosi repon Anthropicin hänelle lainaamaan 500 gigatavun koneeseen, vahvisti sen toimivan, ja sitten kirjoitti,

2:56 lainaus, matemaattisesti tämä työ ei kerro meille olennaisesti mitään. Hän oli jo 99,9 prosenttisesti varma, että lause oli tosi, eikä todistus lisää uutta matematiikkaa; se mitä se näyttää, on mitä autoformalisointi voi tehdä nyt, ja siitä osasta hän on aidosti innoissaan. Hänelle annettiin miljoona puntaa viiden vuoden aikana; Anthropicin kesti yksitoista päivää, ja kommentoijan nopea laskelma asettaa kuusi miljardia tuotostokenia listahintaan. noin 300 000 dollaria, joten kone oli halvempi, ellet laske koneen koulutusta, mitä kukaan ei tee.

3:24 Paras yksityiskohta: sähköposti saapui, kun hän oli musiikkifestivaaleilla Walesissa yhdellä 4G-verkon palkilla, nimettömältä lähettäjältä, josta hän ei ollut koskaan kuullut, joten hän piti sitä pilana ja luki sen viikkoa myöhemmin, mikä on oikea reaktio kaikkiin otsikoihin, jotka sisältävät päästä päähän -formalisaation. Sillä välin ihmiset saivat yhden takaisin. Shin Jin-seo, maailman Go-mestari, voitti KataGon, vahvimman avoimen lähdekoodin Go-moottorin, kaksi peliä yhteen Soulissa kahden kiven tasolla, mikä vastaa suurin piirtein huippuammattilaisen ja aloittelevan ammattilaisen välistä eroa.

3:50 Ratkaiseva peli oli 11,5 pisteen voitto 221 siirrossa, pitäen 99 prosentin voittotodennäköisyyden pelin puolivälistä lähtien, ja hän voitti 250 miljoonaa won-rahaa, noin 170 000 dollaria, sekä Genesis G90:n, joten palkkio superihmisen tekoälyn voittamisesta on 170 kertaa Googlen palkkio Chrome-hiekkalaatikon karkottamisesta. Hänen selityksensä: alussa hän kopioi tekoälyn siirtoja ja hävisi; hän voitti rakentamalla pelilaudan omalla tyylillään, mikä on hyödyllisin neuvo tekoälystä, jonka olen kuullut koko vuonna, ja se tuli lautapelistä. Kaksi riviä lisää diffissä.

4:22 Oxc:n Rust React Compiler on nyt natiivina Vitessa yhden lipun takana; 1 036 tiedoston koodikanta siirtyi 14,3 sekunnista 0,81 sekuntiin käännösvaiheessa, enimmäkseen poistamalla Babelin package.jsonista, mikä on myös ihonhoitorutiinini. Ja IBM julkaisi Bobin, tekoälypohjaisen koodauskumppanin, joka tervehtii sinua sanoilla "Hi, I'm Bob", luo ala-agentteja, modernisoi suurtietokoneen koodia ja julkaisee Bobalytics-nimisen analytiikkatuotteen, joten jossain joku pankki on hyvin innoissaan eikä kukaan lukenut lisenssiä.

4:51 Tässä on paljon katetta yhdelle perjantaille; jos haluat mieluummin lukea tämän kuin kuulla minun sanovan sen, diff saapuu sähköpostiisi joka aamu – ilmaiseksi osoitteessa the daily diff dot dev, linkki alla. Joten, tämänpäiväinen tuomio: SHIP IT. Kernel sanoo kyllä, Buzzard sanoo kyllä, matematiikka ei muuttunut, mutta tapa, jolla tarkistamme matematiikan, juuri muuttui. Tässä on tämänpäiväinen diff. Olen Niko Axrisista.

5:09 Yhdistä vastuullisesti.

Lähteet

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