# Claude je dokazao Ferma za 11 dana. Presuda: SHIP IT.

Published: 2026-09-07

Claude je proveo 11 dana i oko 6 milijardi tokena pišući 13 miliona linija Lean dokaza Fermatovog posljednjeg teorema — prvi put end-to-end računalno provjeren — dok matematičar koji ga formalizira od 2024. kaže da nam "suštinski ništa ne govori" matematički i ipak je oduševljen. Istog dana: Go svjetski broj 1 Shin Jin-seo pobjeđuje KataGo 2–1 sa hendikepom od dva kamena. Presuda: SHIP IT.

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

## Šta ovaj video pokriva

- Claude formalizira Fermatov posljednji teorem u Lean 4
- Chromium sandbox RCE (CVE-2026-85046), iskorišten u divljini, 1.000 USD nagrade
- Shin Jin-seo pobjeđuje KataGo sa hendikepom od dva kamena

## Prevedeni transkript

Prevedeno iz originalne engleske naracije. Dostupan zvuk i titlovi kontroliše YouTube.

0:00 Fermat je rekao da njegov čudesni dokaz neće stati na marginu, a danas je Anthropic objavio marginu: trinaest miliona linija Leana, pet puta veću od Mathliba, dokazujući teorem u koji je svaki matematičar već vjerovao. Bilo je deset do jedanaest u Tbilisiju kada je Anthropic objavio, pa sam prirodno bio budan. Jučer je Google objavio Chrome 152 sa dvanaest sigurnosnih popravaka, jedan od njih je V8 bug već iskorišten u divljini, i platio reporteru hiljadu dolara, što je manje od limuzine o kojoj ćemo kasnije.

0:26 Također jučer, Mullvad je objavio da zatvara svoj javni šifrirani DNS 2. novembra i plaća Quad9 da to radi umjesto njih, a jutros je Rust React Compiler postao nativan u Viteu, dok je Hacker News otkrio IBM Boba, AI agenta za kodiranje. Zatim je Claude formalizirao Fermatov posljednji teorem, a na istoj naslovnoj stranici korejski velemajstor je pobijedio najjači Go motor na Zemlji, pa je danas čovječanstvo imalo jedan od dva uspjeha. U ovom videu: što je Claude zapravo dokazao, koliko je to koštalo,

0:52 zašto matematičar koji je proveo svoju karijeru na ovome kaže da to ništa ne mijenja i ipak je oduševljen, i kako je čovjek pobijedio mašinu u Gou. Petak je, 4. septembar, i ovo je The Daily Diff. Fermatov posljednji teorem: nema pozitivnih cijelih brojeva a, b, c koji zadovoljavaju a na n plus b na n jednako c na n za bilo koji n iznad 2. Fermat je to zabilježio na margini oko 1637. i umro ne pokazavši svoj rad, što ga čini prvim programerom koji je zatvorio tiket sa "radi na mojoj mašini". Nagrada od 100.000 zlatnih maraka iz 1908. privukla je 621 pogrešan

1:25 dokaz u prvoj godini, a Andrew Wiles ga je konačno dokazao 1995. na 129 stranica koje su sucima trebale mjeseci da provjere. Formalizacija znači prepisivanje tog dokaza tako da Lean, asistent za dokazivanje, može mehanički provjeriti svaki korak, a Kevin Buzzard s Imperiala je vodio ljudski napor da to učini od 2024.; sam nacrt ima 86 stranica. Istraživač iz Anthropic-a, Tianyi Peng, usmjerio je desetine Claude agenata na to umjesto toga, na platformi nazvanoj Prove2Me koja održava DAG teorema izjava tako da agenti znaju što sljedeće dokazati, jer bez toga prvi

2:00 rojevi su izgubili trag tko što dokazuje, što se događa kada vam je orkestracijski sloj regex s marketinškim budžetom. Jedanaest dana kasnije korijenski čvor je glasio PROVEDENO: trinaest miliona linija Leana, 29.500 međuproizvodnih teorema, oko šest milijardi izlaznih tokena iz internog modela otprilike usporedivog s Claude Fable 5.1. Izgradnja ne uspijeva osim ako dokaz počiva na točno Lean-ovim tri standardne aksiome: nema isprike, nema nativnog odlučivanja, nema varanja. Provjera također nije jeftina: izrada

2:29 od nule trajala je pet i pol sati na 96 jezgri i 153 gigabajta RAM-a, a imena teorema su strojno generirana, tako da se repozitorij opisuje kao napisan za provjeru, a ne za čitanje, što je i kako bih opisao enterprise Javu. Sada proturječje. Anthropic-ov post kaže da Lean nedvojbeno dokazuje ispravnost. Kevin Buzzard, čovjek kojeg su pretekli, kompajlirao je repozitorij na stroju od 500 gigabajta koji mu je Anthropic posudio, potvrdio da se provjerava, a zatim napisao,

2:56 citiram, matematički ovaj rad nam suštinski ništa ne govori. Već je bio 99,9 posto siguran da je teorem istinit, i dokaz ne dodaje novu matematiku; ono što pokazuje je što autoformalizacija može učiniti sada, i taj dio ga istinski uzbuđuje. Dobio je milijun funti tijekom pet godina; Anthropicu je trebalo jedanaest dana, a komentatorova brza kalkulacija stavlja šest milijardi izlaznih tokena po redovnoj cijeni oko 300.000 dolara, pa je mašina bila jeftinija, osim ako ne računate obuku mašine, što niko ne radi.

3:24 Najbolji detalj: e-mail je stigao dok je bio na muzičkom festivalu u Velsu sa jednom crticom 4G signala, od imena za koje nikada nije čuo, pa je to otpisao kao šalu i pročitao ga sedam dana kasnije, što je tačan odgovor na bilo koji naslov koji sadrži potpunu formalizaciju. U međuvremenu, ljudi su uzvratili. Shin Jin-seo, svjetski broj jedan u Gou, pobijedio je KataGo, najjači open-source Go engine, dvije igre prema jednoj u Seulu sa hendikepom od dva kamena, otprilike jaz između vrhunskog profesionalca i profesionalca početnika.

3:50 Odluka je bila pobjeda od 11,5 poena u 221 potezu, držeći 99 posto vjerovatnoće pobjede od sredine igre pa nadalje, i kući je odnio 250 miliona wona, oko 170.000 dolara, plus Genesis G90, tako da je nagrada za pobjedu nad nadljudskom umjetnom inteligencijom 170 puta veća od Googleove nagrade za izlazak iz Chrome sandboxa. Njegovo objašnjenje: na početku je kopirao poteze umjetne inteligencije i gubio; pobijedio je gradeći ploču u svom stilu, što je najkorisniji savjet o umjetnoj inteligenciji koji sam čuo cijele godine, a došao je iz društvene igre. Još dvije linije u diff-u.

4:22 Rust React Compiler iz oxc-a je sada nativan u Viteu iza jedne zastavice; baza kodova od 1.036 datoteka prešla je sa 14,3 sekunde na 0,81 u koraku kompilacije, uglavnom brisanjem Babela iz package.json, što je također moja rutina njege kože. A IBM je lansirao Boba, AI partnera za kodiranje koji vas pozdravlja sa „Zdravo, ja sam Bob“, stvara podagente, modernizuje mainframe kod i isporučuje analitički proizvod pod nazivom Bobalytics, pa je negdje neka banka vrlo uzbuđena i niko nije pročitao licencu.

4:51 To je mnogo marže za jedan petak; ako ovo radije čitate nego da me slušate kako to govorim, diff stiže u vaše sanduče svako jutro — besplatno na daily diff dot dev, link ispod. Dakle, današnja presuda: SHIP IT. Kernel kaže da, Buzzard kaže da, matematika se nije promijenila, ali način na koji provjeravamo matematiku se upravo promijenio. To je današnji diff. Ja sam Niko iz Axrisija.

5:09 Spajajte odgovorno.

## Izvori

- [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