# Claude dokázal Fermata za 11 dní. Verdikt: SCHVÁLENÉ.

Published: 2026-09-07

Claude strávil 11 dní a asi 6 miliárd tokenov písaním 13-miliónovej verzie Lean dôkazu Fermatovej poslednej vety – prvého komplexného počítačom overeného – zatiaľ čo matematik, ktorý ju formalizuje od roku 2024, hovorí, že "nám matematicky v podstate nič nehovorí" a aj tak je nadšený. V ten istý deň: Svetová jednotka Go Shin Jin-seo poráža KataGo 2:1 s dvojkameňovým hendikepom. Verdikt: SCHVÁLENÉ.

Canonical: https://thedailydiff.dev/sk/video/2026-09-04-fermat-lean/

## Čo toto video pokrýva

- Claude formalizuje Fermatovu poslednú vetu v Lean 4
- Chromium sandbox RCE (CVE-2026-85046), zneužité v praxi, odmena 1 000 USD
- Shin Jin-seo poráža KataGo s dvojkameňovým hendikepom

## Preložený prepis

Preložené z pôvodného anglického rozprávania. Dostupný zvuk a titulky sú kontrolované službou YouTube.

0:00 Fermat povedal, že jeho úžasný dôkaz by sa nezmestil na okraj, a dnes Anthropic zverejnil okraj: trinásť miliónov riadkov kódu Lean, päťnásobok veľkosti Mathlibu, dokazujúci vetu, ktorej každý matematik už veril. V Tbilisi bolo desať až jedenásť, keď Anthropic zverejnil, takže som prirodzene bdel. Včera Google vydal Chrome 152 s dvanástimi bezpečnostnými opravami, jedna z nich bola chyba V8 už zneužitá v praxi, a zaplatil reportérovi tisíc dolárov, čo je menej ako za sedan, ku ktorému sa dostaneme neskôr.

0:26 Taktiež včera Mullvad oznámil, že 2. novembra vypína svoju verejnú šifrovanú DNS a namiesto toho platí Quad9, aby to urobil, a dnes ráno Rust React Compiler prešiel natívne vo Vite, zatiaľ čo Hacker News objavil IBM Bob, agenta pre AI kódovanie. Potom Claude formalizoval Fermatovu poslednú vetu a na tej istej titulnej strane kórejský veľmajster porazil najsilnejší Go engine na Zemi, takže dnes ľudstvo uspelo v pomere jedna ku dvom. V tomto videu: čo Claude skutočne dokázal, čo to stálo,

0:52 prečo matematik, ktorý strávil svoju kariéru týmto, hovorí, že to nič nemení a aj tak je nadšený, a ako človek porazil stroj v Go. Je piatok, 4. septembra, a toto je The Daily Diff. Fermatova posledná veta: žiadne kladné celé čísla a, b, c nespĺňajú a na n-tú plus b na n-tú rovná sa c na n-tú pre žiadne n nad 2. Fermat si to načmáral na okraj okolo roku 1637 a zomrel bez toho, aby ukázal svoju prácu, čím sa stal prvým vývojárom, ktorý uzavrel tiket s "funguje to na mojom stroji". Cena 100 000 zlatých mariek z roku 1908 prilákala 621 chybných

1:25 dôkazov v prvom roku a Andrew Wiles to nakoniec dokázal v roku 1995, na 129 stranách, ktorých overenie trvalo posudzovateľom mesiace. Formalizovanie znamená prepísanie tohto dôkazu tak, aby Lean, asistent dôkazov, mohol mechanicky skontrolovať každý krok, a Kevin Buzzard z Imperialu viedol ľudské úsilie presne to urobiť od roku 2024; samotný plán má 86 strán. Výskumník Anthropic Tianyi Peng namieril desiatky Claude agentov na to namiesto toho, na platforme nazvanej Prove2Me, ktorá udržuje DAG výrokov teorémov, aby agenti vedeli, čo majú dokázať ďalej, pretože bez nej prvé

2:00 roje stratili prehľad o tom, kto čo dokazoval, čo sa stane, keď vaša orchestračná vrstva je regex s marketingovým rozpočtom. Jedenásť dní neskôr koreňový uzol hlásil DOKÁZANÉ: trinásť miliónov riadkov Lean kódu, 29 500 medzivýsledných teorémov, asi šesť miliárd výstupných tokenov z interného modelu približne porovnateľného s Claude Fable 5.1. Zostavenie zlyhá, pokiaľ sa dôkaz neopiera presne o tri štandardné axiómy Lean: žiadne prepáčte, žiadne natívne rozhodovanie, žiadne podvádzanie. Kontrola nie je tiež lacná:

2:29 zostavenie od nuly trvalo päť a pol hodiny na 96 jadrách a 153 gigabajtoch RAM, a názvy teorémov sú strojovo generované, takže repozitár sa sám opisuje ako napísaný na kontrolu a nie na čítanie, čo je tiež spôsob, akým by som opísal podnikový Java kód. Teraz rozpor. Príspevok Anthropic hovorí, že Lean dokazuje správnosť bez pochybností. Kevin Buzzard, muž, ktorého prekonali, skompiloval repozitár na 500-gigabajtovom stroji, ktorý mu Anthropic požičal, potvrdil, že sa overil, a potom napísal,

2:56 citujem, matematicky nám táto práca v podstate nič nehovorí. Už bol na 99,9 percenta istý, že teorém je pravdivý, a dôkaz nepridáva žiadnu novú matematiku; ukazuje, čo dokáže autoformalizácia teraz, a z tejto časti je skutočne nadšený. Dostal milión libier za päť rokov; Anthropicu to trvalo jedenásť dní, a "servítkové" výpočty komentátora uvádzajú šesť miliárd výstupných tokenov za cenníkovú cenu. okolo 300 000 dolárov, takže stroj bol lacnejší, pokiaľ nepočítate školenie stroja, čo nikto nerobí.

3:24 Najlepší detail: e-mail prišiel, keď bol na hudobnom festivale vo Walese s jednou čiarkou 4G, od mena, o ktorom nikdy nepočul, takže to odpísal ako vtip a prečítal si ho o týždeň neskôr, čo je správna reakcia na akýkoľvek predmet obsahujúci komplexnú formalizáciu. Medzitým ľudia získali jeden bod späť. Shin Jin-seo, svetová jednotka v Go, porazil KataGo, najsilnejší open-source Go engine, dva zápasy k jednému v Soule s hendikepom dvoch kameňov, čo je zhruba rozdiel medzi špičkovým profesionálom a nováčikom profesionálom.

3:50 Rozhodujúci zápas bol víťazstvo o 11,5 bodu v 221 ťahoch, držiac 99-percentnú pravdepodobnosť víťazstva od polovice hry, a domov si odniesol 250 miliónov wonov, asi 170 000 dolárov, plus Genesis G90, takže odmena za porazenie nadľudskej AI je 170-krát vyššia ako odmena Googlu za únik z Chrome sandboxu. Jeho vysvetlenie: na začiatku kopíroval ťahy AI a prehral; vyhral tým, že si postavil hraciu plochu vo svojom vlastnom štýle, čo je najužitočnejšia rada o AI, akú som počul tento rok, a prišla z doskovej hry. Ďalšie dva riadky v The Daily Diff.

4:22 Rust React Compiler z oxc je teraz natívny vo Vite za jedným príznakom; kódová báza s 1 036 súbormi prešla z 14,3 sekúnd na 0,81 v kompilačnom kroku, väčšinou odstránením Babelu z package.json, čo je tiež moja rutina starostlivosti o pleť. A IBM spustilo Boba, partnera pre kódovanie AI, ktorý vás pozdraví s Ahoj, som Bob, vytvára subagenty, modernizuje kód mainframe, a dodáva analytický produkt s názvom Bobalytics, takže niekde je banka veľmi nadšená a nikto si neprečítal licenciu.

4:51 To je na jeden piatok veľa marže; ak si to radšej prečítate, než by ste ma chceli počuť hovoriť, The Daily Diff pristane vo vašej schránke každé ráno – zadarmo na thedailydiff.dev, odkaz nižšie. Takže dnešný verdikt: SHIP IT. Jadro hovorí áno, Buzzard hovorí áno, matematika sa nezmenila, ale spôsob, akým kontrolujeme matematiku, sa práve zmenil. To je dnešný The Daily Diff. Som Niko z Axrisi.

5:09 Zlučujte zodpovedne.

## Zdroje

- [Anthropic — Formalizing Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem) — www.anthropic.com
- [The proof (Lean 4, Apache-2.0)](https://github.com/anthropics/fermats-last-theorem) — github.com
- [Kevin Buzzard — FLT: Anthropic has beaten me to it](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/) — xenaproject.wordpress.com
- [HN thread](https://news.ycombinator.com/item?id=49568506) — news.ycombinator.com
- [KED Global — Shin defeats KataGo](https://www.kedglobal.com/artificial-intelligence/newsView/ked202607210007) — www.kedglobal.com
- [HN](https://news.ycombinator.com/item?id=49544762) — news.ycombinator.com
- [Chrome 152 release notes (CVE-2026-85046)](https://chromereleases.googleblog.com/2026/09/stable-channel-update-for-desktop_01882797386.html) — chromereleases.googleblog.com
- [NVD](https://nvd.nist.gov/vuln/detail/cve-2026-85046) — nvd.nist.gov
- [Mullvad — shutting down public encrypted DNS](https://mullvad.net/en/blog/shutting-down-our-public-encrypted-dns-servers-and-sponsoring-quad9-instead) — mullvad.net
- [Rust React Compiler native in Vite](https://blog.master.dev/react-now-rusted-all-the-way-out/) — blog.master.dev
- [IBM Bob](https://bob.ibm.com/) — bob.ibm.com