# Claude dokazao Fermata za 11 dana. Presuda: SHIP IT.

Published: 2026-09-07

Claude je proveo 11 dana i oko 6 milijardi tokena pišući Lean dokaz Fermatovog posljednjeg teorema od 13 milijuna redaka — prvi cjeloviti računalno provjereni — dok matematičar koji ga formalizira od 2024. kaže da nam "matematički ne govori suštinski ništa" i svejedno je oduševljen. Isti dan: Go svjetski broj 1 Shin Jin-seo pobijedio KataGo 2–1 s hendikepom od dva kamena. Presuda: SHIP IT.

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

## Što ovaj video pokriva

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

## Prevedeni transkript

Prevedeno iz izvornog engleskog pripovijedanja. Dostupni zvuk i titlovi kontroliraju se putem YouTubea.

0:00 Fermat je rekao da njegov čudesni dokaz neće stati na marginu, a danas je Anthropic objavio marginu: trinaest milijuna redaka Leana, pet puta veću od Mathliba, dokazujući teorem u koji su već svi matematičari vjerovali. Bilo je deset do jedanaest u Tbilisiju kad je Anthropic objavio, pa sam prirodno bio budan. Jučer je Google objavio Chrome 152 s dvanaest sigurnosnih popravaka, jedan od njih je V8 bug već iskorišten u divljini, i platio je izvjestitelju tisuću dolara, što je manje od limuzine koju ćemo spomenuti kasnije.

0:26 Također jučer, Mullvad je rekao da gasi svoj javni šifrirani DNS 2. studenog i plaća Quad9 da to radi umjesto njega, a jutros je Rust React Compiler prešao na native u Viteu, dok je Hacker News otkrio IBM Boba, AI agenta za kodiranje. Zatim je Claude formalizirao Fermatov posljednji teorem, a na istoj naslovnici je korejski velemajstor pobijedio najjači Go engine na Zemlji, tako da je danas čovječanstvo bilo jedan za dva. U ovom videu: što je Claude zapravo dokazao, koliko je koštalo,

0:52 zašto matematičar koji je proveo svoju karijeru na ovome kaže da ništa ne mijenja i svejedno je oduševljen, i kako je čovjek pobijedio stroj u Gou. Petak je, 4. rujna, 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 ga je zapisao na marginu oko 1637. i umro bez da je pokazao svoj rad, što ga čini prvim developerom koji je zatvorio tiket s 'radi na mom stroju'. 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 dobio 1995. u 129 stranica koje su sucima trebale mjeseci za provjeru. Formaliziranje znači prepisivanje tog dokaza tako da Lean, asistent za dokaze, može mehanički provjeriti svaki korak, a Kevin Buzzard s Imperijala vodi ljudski napor da to učini od 2024.; sam nacrt ima 86 stranica. Istraživač iz Anthropic-a, Tianyi Peng, umjesto toga je usmjerio desetke Claude agenata na to na platformi nazvanoj Prove2Me koja održava DAG teorema izjava kako bi agenti znali što dalje dokazivati, 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 DOKAZANO: trinaest milijuna redaka Leana, 29.500 međuproizvodnih teorema, oko šest milijardi izlaznih tokena iz internog modela otprilike usporedivog s Claude Fable 5.1. Izgradnja propada ako se dokaz ne temelji isključivo na tri standardna Leanova aksioma: ne, oprostite, bez native decide, bez varanja. Provjera također nije jeftina: a

2:29 izgradnja 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 također način na koji bih opisao enterprise Javu. Sada proturječnost. Anthropicova objava kaže da Lean demonstrira ispravnost bez sumnje. Kevin Buzzard, čovjek koji je pretečen, kompajlirao je repozitorij na stroju od 500 gigabajta koji mu je posudio Anthropic, potvrdio da se provjerava, a zatim je napisao,

2:56 citiram, matematički nam ovaj rad suštinski ništa ne govori. Već je bio 99,9 posto siguran da je teorem istinit, a dokaz ne dodaje novu matematiku; ono što pokazuje je što autoformalizacija može učiniti sada, i taj dio ga je iskreno oduševio. Dobio je milijun funti tijekom pet godina; Anthropicu je trebalo jedanaest dana, a komentatorova brza procjena stavlja šest milijardi izlaznih tokena po katalog cijeni oko 300.000 dolara, pa je stroj bio jeftiniji, osim ako ne računate obuku stroja, što nitko ne radi.

3:24 Najbolji detalj: e-mail je stigao dok je bio na glazbenom festivalu u Walesu s jednom crticom 4G, od imena za koje nikad nije čuo, pa ga je otpisao kao šalu i pročitao ga tjedan dana kasnije, što je ispravan odgovor na bilo koji naslov koji sadrži end-to-end 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 s hendikepom od dva kamena, otprilike razlika između vrhunskog profesionalca i profesionalca početnika.

3:50 Odlučujuća je bila pobjeda od 11,5 poena u 221 potezu, držeći 99 posto vjerojatnosti pobjede od sredine igre nadalje, a kući je odnio 250 milijuna won, oko 170.000 dolara, plus Genesis G90, tako da je nagrada za pobjedu nad nadljudskim AI-jem 170 puta veća od Googleove nagrade za Chrome sandbox escape. Njegovo objašnjenje: rano je kopirao AI poteze i izgubio; pobijedio je gradeći ploču u vlastitom stilu, što je najkorisniji savjet o AI-ju koji sam čuo cijele godine, a došao je iz društvene igre. Još dvije linije u The Daily Diffu.

4:22 Rust React Compiler iz oxc-a sada je nativan u Viteu iza jedne zastavice; baza koda od 1.036 datoteka prešla je s 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 pokrenuo Boba, AI partnera za kodiranje koji vas pozdravlja s Bok, ja sam Bob, stvara podagente, modernizira mainframe kod i isporučuje analitički proizvod pod nazivom Bobalytics, pa je negdje neka banka vrlo uzbuđena i nitko nije pročitao licencu.

4:51 To je puno marže za jedan petak; ako ovo radije čitate nego što me slušate kako to govorim, The Daily Diff stiže u vašu pristiglu poštu svako jutro — besplatno na thedailydiff.dev, poveznica ispod. dev, poveznica 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 The Daily Diff. Ja sam Niko iz Axrisija.

5:09 Merge responsibly.

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