Claude 11 nap alatt bizonyította Fermat-t. Ítélet: SHIP IT.

Amit ez a videó tartalmaz

• Claude formalizálja Fermat utolsó tételét a Lean 4-ben
• Chromium sandbox RCE (CVE-2026-85046), kihasználva a valóságban, 1000 dollár jutalom
• Shin Jin-seo legyőzi KataGo-t kétköves hendikeppel

Lefordított átirat

Az eredeti angol narrációból fordítva. A rendelkezésre álló hangot és feliratokat a YouTube vezérli.

0:00 Fermat azt mondta, csodálatos bizonyítása nem férne el a margóra, és ma az Anthropic publikálta a margót: tizenhárommillió sor Lean, ötször nagyobb, mint a Mathlib, és egy olyan tételt bizonyít, amit minden matematikus már el is hitt. Tbilisziben tíz-tizenegy volt, amikor az Anthropic posztolt, szóval természetesen ébren voltam. Tegnap a Google kiadta a Chrome 152-t tizenkét biztonsági javítással, ezek közül az egyik egy V8 hiba, amit már kihasználtak a valóságban, és ezer dollárt fizettek a bejelentőnek, ami kevesebb, mint az a szedán, amiről később szót ejtünk.

0:26 Szintén tegnap a Mullvad bejelentette, hogy november 2-án leállítja nyilvános titkosított DNS-ét, és a Quad9-nek fizet, hogy ezt tegye helyette, ma reggel pedig a Rust React Compiler natívvá vált Vite-ban, miközben a Hacker News felfedezte az IBM Bobot, egy AI kódoló ügynököt. Aztán Claude formalizálta Fermat utolsó tételét, és ugyanazon az első oldalon egy koreai nagymester legyőzte a legerősebb Go motort a Földön, szóval ma az emberiség egyből kettőt teljesített. Ebben a videóban: mit is bizonyított Claude valójában, mennyibe került,

0:52 miért mondja a matematikus, aki a karrierjét erre szánta, hogy ez semmin sem változtat, és mégis izgatott, és hogyan győzte le az ember a gépet Go-ban. Péntek van, szeptember 4., és ez a The Daily Diff. Fermat utolsó tétele: nincsenek pozitív egész számok a, b, c amelyek kielégítik az a az n-edik plusz b az n-edik egyenlő c az n-edik egyenletet bármely 2-nél nagyobb n esetén. Fermat 1637 körül felírta a margóra, és úgy halt meg, hogy nem mutatta be a munkáját, így ő lett az első fejlesztő, aki egy „az én gépemen működik” megjegyzéssel zárt le egy hibajegyet. Egy 1908-as 100 000 arany márkás díj 621 hibás

1:25 bizonyítékot vonzott az első évben, és Andrew Wiles végül 1995-ben kapta meg, 129 oldalon, aminek ellenőrzése hónapokig tartott a bírálók számára. A formalizálás azt jelenti, hogy átírjuk ezt a bizonyítékot, hogy a Lean, egy bizonyítási asszisztens, mechanikusan ellenőrizhesse minden lépését, és Kevin Buzzard az Imperialnál 2024 óta egy emberi erőfeszítést vezet pontosan ennek elvégzésére; a tervrajz önmagában 86 oldal. Tianyi Peng, az Anthropic kutatója ehelyett tucatnyi Claude ügynököt irányított rá, egy Prove2Me nevű platformon, amely egy DAG-ot tart fenn a tételekről, így az ügynökök tudják, mit kell legközelebb bizonyítaniuk, mert enélkül az első

2:00 rajok elvesztették a fonalat, hogy ki mit bizonyít, ami akkor történik, ha az orchestration réteged regex marketing költségvetéssel. Tizenegy nap múlva a gyökérpont így szólt: BIZONYÍTVA: tizenhárommillió sor Lean, 29 500 közbenső tétel, körülbelül hatmilliárd kimeneti token egy belső modellből, amely nagyjából összehasonlítható a Claude Fable 5.1-gyel. A fordítás sikertelen, hacsak a bizonyítás pontosan Lean három standard axiómáján alapul: nem, bocsánat, nincs natív döntés, nincs csalás. Az ellenőrzése sem olcsó: egy

2:29 a nulláról épített verzió öt és fél órát vett igénybe 96 magon és 153 gigabyte RAM-on, és a tételnevek géppel generáltak, így a repo azt állítja magáról, hogy ellenőrzésre íródott, nem pedig olvasásra, ami egyébként az enterprise Java-t is jellemezném. Most az ellentmondás. Az Anthropic bejegyzése szerint a Lean minden kétséget kizáróan igazolja a helyességet. Kevin Buzzard, az az ember, akit megelőztek, lefordította a repót egy 500 gigabyte-os gépen, amit az Anthropic kölcsönzött neki, megerősítette, hogy ellenőrizhető, majd azt írta,

2:56 idézem, matematikailag ez a munka lényegében semmit sem mond nekünk. Már 99,9 százalékig biztos volt abban, hogy a tétel igaz, és a bizonyítás nem ad hozzá új matematikát; azt mutatja meg, mire képes ma az autoformalizálás, és ez a része igazán izgatja. Öt évre egymillió fontot kapott; az Anthropic tizenegy napot vett igénybe, és egy kommentelő becslése szerint hatmilliárd kimeneti token listás áron körülbelül 300 000 dollár, szóval a gép olcsóbb volt, hacsak nem számoljuk a gép betanítását, amit senki sem tesz.

3:24 Legjobb részlet: az email akkor érkezett, amikor egy walesi zenei fesztiválon volt, egy vonal 4G-vel, egy névtől, amiről még sosem hallott, szóval bolondnak hitte, és egy héttel később olvasta el, ami a helyes válasz minden tárgysorra, amely végpontok közötti formalizálást tartalmaz. Közben az emberek visszavágtak. Shin Jin-seo, a világ első számú Go játékosa, legyőzte a KataGo-t, a legerősebb nyílt forráskódú Go motort, két játszmát egy ellen Szöulban, két kő handicappel, ami nagyjából a különbség egy top profi és egy újonc profi között.

3:50 A döntő egy 11,5 pontos győzelem volt 221 lépésben, megtartva a 99 százalékos nyerési valószínűséget a játék közepétől, és hazavitt 250 millió wont, körülbelül 170 000 dollárt, plusz egy Genesis G90-et, szóval a szuperhumán AI legyőzéséért járó jutalom 170-szerese a Google Chrome sandbox kikerüléséért járó jutalmának. Az ő magyarázata: eleinte AI lépéseket másolt és vesztett; úgy nyert, hogy a saját stílusában építette fel a táblát, ami a leghasznosabb tanács az AI-ról, amit idén hallottam, és egy társasjátéktól származott. Még két sor a diffben.

4:22 Az oxc Rust React fordítóprogramja most már natív a Vite-ben egy jelző mögött; egy 1036 fájlból álló kódbázis 14,3 másodpercről 0,81-re csökkent a fordítási lépésben, főleg a Babel törlésével a package.json-ból, ami egyben az én bőrápolási rutin is. És az IBM elindította Bobot, egy AI kódoló partnert, aki „Szia, Bob vagyok” üdvözlettel fogad, alügynököket hoz létre, modernizálja a nagyszámítógépek kódját, és kiad egy Bobalytics nevű analitikai terméket, szóval valahol egy bank nagyon izgatott, és senki sem olvasta el a licencet.

4:51 Ez sok margó egy péntekre; ha inkább elolvasnád, mint meghallgatnád tőlem, a diff minden reggel megérkezik a postaládádba – ingyenesen a the daily diff dot dev oldalon, link lent. Szóval, a mai ítélet: SHIP IT. A kernel igent mond, a Buzzard igent mond, a matek nem változott, de az, ahogyan a matekot ellenőrizzük, most igen. Ez a mai diff. Niko vagyok az Axrisi-től.

5:09 Összefonódás felelősségteljesen.

Források

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