Claude dokázal Fermata za 11 dní. Verdikt: SHIP IT.

Co toto video pokrývá

• Claude formalizuje Fermatovu poslední větu v Lean 4
• Chromium sandbox RCE (CVE-2026-85046), zneužito v praxi, odměna 1 000 $
• Shin Jin-seo porazil KataGo s handicapem dvou kamenů

Přeložený přepis

Přeloženo z původního anglického vyprávění. Dostupné audio a titulky jsou řízeny YouTube.

0:00 Fermat řekl, že jeho úžasný důkaz by se nevešel do okraje, a dnes Anthropic zveřejnil okraj: třináct milionů řádků Lean, pětkrát větší než Mathlib, dokazující větu, které už každý matematik věřil. V Tbilisi bylo deset až jedenáct, když Anthropic zveřejnil, takže jsem přirozeně byl vzhůru. Včera Google vydal Chrome 152 s dvanácti bezpečnostními opravami, jedna z nich byla chyba V8 již zneužita v praxi, a zaplatil reportérovi tisíc dolarů, což je méně než sedan, ke kterému se dostaneme později.

0:26 Také včera Mullvad oznámil, že 2. listopadu vypíná svůj veřejný šifrovaný DNS a místo toho platí Quad9, a dnes ráno Rust React Compiler přešel do nativní podoby ve Vite, zatímco Hacker News objevil IBM Bob, agent AI kódování. Pak Claude formalizoval Fermatovu poslední větu a na téže titulní straně korejský velmistr porazil nejsilnější Go engine na Zemi, takže dnes lidstvo bylo jedna ku dvěma. V tomto videu: co Claude skutečně dokázal, co to stálo,

0:52 proč matematik, který na tom strávil kariéru, říká, že to nic nemění a přesto je nadšený, a jak člověk porazil stroj v Go. Je pátek, 4. září, a toto je The Daily Diff. Fermatova poslední věta: žádná kladná celá čísla a, b, c nesplňují a na n plus b na n se rovná c na n pro jakékoli n nad 2. Fermat si to naškrábal do okraje kolem roku 1637 a zemřel, aniž by ukázal svou práci, čímž se stal prvním vývojářem, který uzavřel tiket s „funguje to na mém stroji“. Cena 100 000 zlatých marek z roku 1908 přilákala 621 chybných

1:25 důkazů v prvním roce, a Andrew Wiles ji konečně získal v roce 1995, na 129 stranách, jejichž ověření trvalo rozhodčím měsíce. Formalizace znamená přepsání tohoto důkazu tak, aby Lean, asistent důkazů, mohl mechanicky zkontrolovat každý krok, a Kevin Buzzard z Imperialu vedl lidské úsilí přesně to dělat od roku 2024; samotný plán má 86 stran. Výzkumník Anthropic Tianyi Peng na to místo toho nasadil desítky agentů Claude na platformě nazvané Prove2Me, která udržuje DAG příkazů vět, aby agenti věděli, co dokázat dál, protože bez toho se první

2:00 roje ztratily v tom, kdo co dokazoval, což se stane, když je vaše orchestrační vrstva regex s marketingovým rozpočtem. Jedenáct dní poté kořenový uzel hlásil PROVEDENO: třináct milionů řádků Lean, 29 500 mezilehlých vět, asi šest miliard výstupních tokenů z interního modelu zhruba srovnatelného s Claude Fable 5.1. Sestavení selže, pokud důkaz nespočívá přesně na třech standardních axiomech Lean: omlouvám se, žádné nativní rozhodování, žádné podvádění. Jeho kontrola také není levná: sestavení

2:29 od začátku trvalo pět a půl hodiny na 96 jádrech a 153 gigabajtech RAM, a názvy vět jsou strojově generované, takže repozitář se popisuje jako napsaný k ověření spíše než ke čtení, což bych také popsal jako podnikový Java. Nyní rozpor. Příspěvek Anthropic říká, že Lean demonstruje správnost nade vší pochybnost. Kevin Buzzard, muž, který byl předstižen, zkompiloval repozitář na 500gigabajtovém stroji, který mu Anthropic zapůjčil, potvrdil, že se kontroluje, a pak napsal,

2:56 cituji, matematicky nám tato práce v podstatě nic neříká. Už byl na 99,9 procenta přesvědčen, že věta je pravdivá, a důkaz nepřidává žádnou novou matematiku; ukazuje, co autoformalizace dokáže nyní, a z této části je skutečně nadšený. Bylo mu dáno milion liber za pět let; Anthropicovi to trvalo jedenáct dní, a podle komentátorova rychlého výpočtu stojí šest miliard výstupních tokenů podle ceníku kolem 300 000 dolarů, takže stroj byl levnější, pokud nepočítáte trénování stroje, což nikdo nedělá.

3:24 Nejlepší detail: e-mail dorazil, když byl na hudebním festivalu ve Walesu s jednou čárkou 4G, od jména, o kterém nikdy neslyšel, takže to odepsal jako podvrh a přečetl si ho o týden později, což je správná reakce na jakýkoli předmět obsahující end-to-end formalizaci. Mezitím se lidem jeden vrátil. Shin Jin-seo, světová jednička v Go, porazil KataGo, nejsilnější open-source Go engine, dvě hry ku jedné v Soulu s handicapem dvou kamenů, zhruba rozdíl mezi špičkovým profesionálem a začínajícím profesionálem.

3:50 Rozhodující byla výhra o 11,5 bodu ve 221 tazích, udržující 99procentní pravděpodobnost výhry od poloviny hry, a odnesl si domů 250 milionů wonů, asi 170 000 dolarů, plus Genesis G90, takže odměna za porážku nadlidské AI je 170krát vyšší než odměna Googlu za únik z Chrome sandboxu. Jeho vysvětlení: zpočátku kopíroval tahy AI a prohrál; vyhrál tím, že postavil desku ve svém vlastním stylu, což je nejužitečnější rada o AI, kterou jsem za celý rok slyšel, a přišla z deskové hry. Další dva řádky v diffu.

4:22 Rust React Compiler z oxc je nyní nativní ve Vite za jedním přepínačem; kódová základna s 1 036 soubory přešla z 14,3 sekund na 0,81 v kroku kompilace, většinou odstraněním Babelu z package.json, což je mimochodem také moje rutina péče o pleť. A IBM spustila Boba, AI kódovacího partnera, který vás pozdraví s Ahoj, jsem Bob, spouští subagenty, modernizuje mainframe kód, a dodává analytický produkt nazvaný Bobalytics, takže někde je banka velmi nadšená a nikdo si nepřečetl licenci.

4:51 To je hodně marže na jeden pátek; pokud si to raději přečtete, než abyste mě slyšeli říkat, diff vám přistane ve schránce každé ráno — zdarma na the daily diff dot dev, odkaz níže. Takže, dnešní verdikt: SHIP IT. Jádro říká ano, Buzzard říká ano, matematika se nezměnila, ale způsob, jakým matematiku kontrolujeme, se právě změnil. To je dnešní diff. Jsem Niko z Axrisi.

5:09 SLUČUJTE ZODPOVĚDNĚ.

Zdroje

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