Claudek Fermaten teorema frogatu zuen 11 egunetan. Epaia: SHIP IT.

Bideo honek zer jorratzen duen

• Claudek Fermaten Azken Teorema formalizatzen du Lean 4-n
• Chromium sandbox RCE (CVE-2026-85046), jadanik ustiatua, 1.000 $ sari gisa
• Shin Jin-seok KataGo garaitu du bi harriko desabantailarekin

Itzulitako transkripzioa

Jatorrizko ingelesezko narraziotik itzulia. Eskuragarri dauden audioa eta azpitituluak YouTube-k kontrolatzen ditu.

0:00 Fermatek esan zuen bere froga bikaina ez zela marjinan sartuko, eta gaur Anthropic-ek marjina argitaratu du: hamahiru milioi lerro Lean, Mathlib-en tamainaren bost bider, matematikari guztiek dagoeneko uste zuten teorema bat frogatuz. Hamarrak laurden gutxi edo hamaikak laurden gutxi ziren Tbilisin Anthropic-ek argitaratu zuenean, beraz, modu naturalean esna nengoen. Atzo Google-k Chrome 152 kaleratu zuen hamabi segurtasun konponketarekin, horietako bat V8-ren akats bat, jadanik ustiatua, eta berriemaileari mila dolar ordaindu zizkion, geroago ikusiko dugun berlina baino gutxiago dena.

0:26 Atzo ere, Mullvad-ek esan zuen bere DNS enkriptatu publikoa itxiko zuela azaroaren 2an eta Quad9-ri ordainduko ziola hura egiteko, eta gaur goizean Rust React Compiler-ek natibo bihurtu zen Vite-n, bitartean Hacker News-ek IBM Bob aurkitu zuen, AI kodetze agente bat. AI kodetze agente bat. Orduan Claudek Fermaten Azken Teorema formalizatu zuen, eta orrialde nagusi berean Koreako maisu handi batek Go motor indartsuena garaitu zuen Lurrean, beraz, gaur gizateriak batetik bi lortu ditu. Bideo honetan: zer frogatu zuen Claudek, zenbat kostatu zen,

0:52 zergatik dio bere karrera honetan eman zuen matematikariak ezer ez duela aldatzen eta hala ere pozik dagoela, eta nola gizaki batek makina garaitu zuen Go-n. Ostirala da, irailak 4, eta hau The Daily Diff da. Fermaten Azken Teorema: ez dago a, b, c zenbaki oso positiborik a^n + b^n = c^n ekuazioa betetzen dutenik n > 2 denean. Fermatek marjina batean idatzi zuen 1637 inguruan eta bere lana erakutsi gabe hil zen, horrela, nire makinan funtzionatzen duela esanez txartel bat itxi zuen lehen garatzailea izan zen. 1908ko 100.000 urrezko markako sari batek 621 froga oker erakarri zituen lehen urtean,

1:25 eta Andrew Wilesek azkenean lortu zuen 1995ean, 129 orrialdetan, epaileei hilabeteak kostatu zitzaizkienak egiaztatzea. Formalizatzeak esan nahi du froga hori berriro idaztea, Lean-ek, froga laguntzaile batek, urrats bakoitza mekanikoki egiaztatu ahal izateko, eta Kevin Buzzardek Imperial-en giza ahalegin bat zuzendu du hori egiteko 2024tik; planoak bakarrik 86 orrialde ditu. Anthropic-eko ikertzaile Tianyi Pengek Claude agente dozenaka jarri zituen horretan, Prove2Me izeneko plataforma batean, teorema adierazpenen DAG bat gordetzen duena, agenteek zer frogatu behar duten jakin dezaten, bestela lehenbiziko taldeek

2:00 nork zer frogatzen ari zenaren arrastoa galdu baitzuten, hori gertatzen baita zure orkestrazio geruza marketin aurrekontua duen regex bat denean. nork zer frogatzen ari zenaren arrastoa galdu baitzuten, hori gertatzen baita zure orkestrazio geruza marketin aurrekontua duen regex bat denean. Hamaika egun geroago, erro nodoan PROVED irakurtzen zen: hamahiru milioi lerro Lean, 29.500 bitarteko teorema, 6 mila milioi irteera token inguru Claude Fable 5.1-ren antzeko barne eredu batetik. 29.500 bitarteko teorema, 6 mila milioi irteera token inguru Claude Fable 5.1-ren antzeko barne eredu batetik. Eraikuntza huts egiten du frogak Leanen hiru axioma estandarretan bakarrik oinarritzen ez bada: ez, barkatu, ez dago erabaki natiborik, ez dago iruzurrik. Egiaztatzea ere ez da merkea: hutsetik

2:29 eraikitzeak bost ordu eta erdi behar izan zituen 96 nukleo eta 153 gigabyte RAM erabiliz, eta teorema izenak makinak sortutakoak dira, beraz, biltegiak bere burua irakurri baino egiaztatzeko idatzita dagoela deskribatzen du, eta horrela deskribatuko nuke enpresako Java ere. Orain kontraesana. Anthropic-en argitalpenak dio Lean-ek zuzentasuna zalantzarik gabe frogatzen duela. Kevin Buzzardek, garaitua izan zen gizonak, biltegia konpilatu zuen Anthropic-ek maileguan utzitako 500 gigabyteko makina batean, egiaztatu zuela baieztatu zuen, eta gero idatzi zuen, aipuak dioenez,

2:56 matematikoki lan honek funtsean ezer ez digu esaten. Dagoeneko %99,9 ziur zegoen teorema egia zela, eta frogak ez du matematika berririk gehitzen; erakusten duena autoformalizazioak zer egin dezakeen da gaur egun, eta horrek ilusio handia egiten dio. Milioi bat libera eman zizkioten bost urterako; Anthropic-ek hamaika egun behar izan zituen, eta iruzkingile baten kalkuluen arabera, sei mila milioi irteera token prezio estandarrean jartzen ditu 300.000 dolar inguru, beraz, makina merkeagoa zen, makina entrenatzea kontuan hartzen ez bada, inork ez duena egiten.

3:24 Xehetasunik onena: posta elektronikoa Galeseko musika jaialdi batean zegoela iritsi zitzaion, 4G-ko barra batekin, inoiz entzun gabeko izen batetik, beraz, zoro batena zela pentsatu zuen eta astebete geroago irakurri zuen, eta hori da edozein gai-lerrorentzako erantzun zuzena, end-to-end formalizazioa dakarrena. Bitartean, gizakiek bat irabazi zuten. Shin Jin-seo, Go-ko munduko lehen postua, KataGo garaitu zuen, Go-ko kode irekiko motor indartsuena, bi partida bat Seulen, bi harriko desabantailarekin, ia goi mailako profesional baten eta hasiberri baten arteko aldea.

3:50 Erabakigarria 11,5 puntuko garaipena izan zen 221 mugimendutan, partida erdian ehuneko 99ko garaipen probabilitatea mantenduz, eta 250 milioi won irabazi zituen, 170.000 dolar inguru, gehi Genesis G90 bat, beraz, supergizaki AI bat garaitzearen saria Google-k Chrome sandbox batetik ihes egiteagatik eskaintzen duen saria baino 170 aldiz handiagoa da. Bere azalpena: hasieran AIren mugimenduak kopiatu zituen eta galdu egin zuen; irabazi egin zuen bere estiloan taula eraikiz, eta hori da AIri buruz urte honetan entzun dudan aholkurik erabilgarriena, eta taula-joko batetik etorri zen. Bi lerro gehiago diff-ean.

4:22 oxc-en Rust React Compiler-a Vite-n jatorrizkoa da orain bandera baten atzean; 1.036 fitxategiko kode-base bat 14,3 segundotik 0,81 segundora pasa zen konpilazio-urratsean, batez ere Babel ezabatuz package.json-etik, eta hori ere nire azala zaintzeko errutina da. Eta IBMk Bob merkaturatu zuen, AI kodeketa-kide bat, 'Kaixo, Bob naiz' esanez agurtzen zaituena, azpiagenteak sortzen dituena, mainframe kodea modernizatzen duena, eta Bobalytics izeneko analitika produktu bat merkaturatzen duena, beraz, nonbait banku bat oso pozik dago, eta inork ez zuen lizentzia irakurri.

4:51 Ostiral baterako marjina asko da; hau irakurri nahiago baduzu niri esaten entzun baino, diff-a zure sarrera-ontzira iristen da goizero — doan the daily diff dot dev-en, behean esteka. Beraz, gaurko epaia: SHIP IT. Kernelak baietz dio, Buzzardek baietz dio, matematikak ez du aldaketarik izan, baina matematikak egiaztatzeko moduak bai. Hori da gaurko diff-a. Niko naiz, Axrisi-koa.

5:09 Fusionatu arduraz.

Iturriak

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