# 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 Lean dokaz Fermaove poslednje teoreme od 13 miliona linija – prvi potpuno kompjuterski proveren – dok matematičar koji ga je formalizovao od 2024. kaže da „nam suštinski ništa ne govori“ matematički i da je svejedno oduševljen. Istog dana: Svetski broj 1 u Go-u Šin Đin-seo pobedio je KataGo sa 2-1 uz hendikep od dva kamena. Presuda: SHIP IT.

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

## Šta ovaj video pokriva

- Claude formalizuje Fermaovu poslednju teoremu u Lean 4
- Chromium sandbox RCE (CVE-2026-85046), eksploatisan u divljini, nagrada 1.000 dolara
- Šin Đin-seo pobedio je KataGo sa hendikepom od dva kamena

## Preveden transkript

Prevedeno sa originalne engleske naracije. Dostupan audio i titlovi kontrolisani su od strane YouTube-a.

0:00 Ferma je rekao da njegov čudesni dokaz ne bi stao na marginu, a danas je Anthropic objavio marginu: trinaest miliona linija Lean-a, pet puta veće od Mathlib-a, dokazujući teoremu u koju je svaki matematičar već verovao. Bilo je deset do jedanaest u Tbilisiju kada je Anthropic objavio, tako da sam prirodno bio budan. Juče je Google objavio Chrome 152 sa dvanaest bezbednosnih zakrpa, jedna od njih je V8 greška već eksploatisana u divljini, i platio je reporteru hiljadu dolara, što je manje od limuzine o kojoj ćemo kasnije govoriti.

0:26 Takođe juče, Mullvad je saopštio da gasi svoj javni šifrovani DNS 2. novembra i da plaća Quad9 da to radi umesto njega, a jutros je Rust React Compiler postao nativan u Vite-u, dok je Hacker News otkrio IBM Bob, AI agenta za kodiranje. Onda je Claude formalizovao Fermaovu poslednju teoremu, a na istoj naslovnoj strani je korejski velemajstor pobedio najjači Go engine na Zemlji, tako da je danas čovečanstvo išlo jedan za dva. U ovom videu: šta je Claude zapravo dokazao, koliko je koštalo,

0:52 zašto matematičar koji je proveo karijeru na ovome kaže da ništa ne menja i da je svejedno oduševljen, i kako je čovek pobedio mašinu u Go-u. Petak je, 4. septembar, i ovo je The Daily Diff. Fermaova poslednja teorema: nema pozitivnih celih brojeva a, b, c koji zadovoljavaju a na n plus b na n jednako je c na n za bilo koje n iznad 2. Ferma je to naškrabao na margini oko 1637. i umro ne pokazavši svoj rad, čineći ga prvim programerom koji je zatvorio tiket sa works on my machine. Nagrada od 100.000 zlatnih maraka iz 1908. privukla je 621 pogrešan

1:25 dokaz u prvoj godini, a Endru Vajls ga je konačno dobio 1995. godine, na 129 stranica koje su sudijama trebale meseci da provere. Formalizovanje znači prepisivanje tog dokaza tako da Lean, asistent za dokaze, može mehanički proveriti svaki korak, a Kevin Buzzard sa Imperial-a je vodio ljudski napor da to uradi tačno od 2024. godine; sam nacrt ima 86 stranica. Istraživač Anthropic-a Tianyi Peng usmerio je desetine Claude agenata na to umesto toga, na platformi zvanoj Prove2Me koja čuva DAG teorema izjava tako da agenti znaju šta da dokažu sledeće, jer bez toga prve

2:00 rojeve su izgubile trag ko šta dokazuje, što se dešava kada vaš orkestracioni sloj je regex sa marketinškim budžetom. Jedanaest dana kasnije, korenski čvor je glasio DOKAZANO: trinaest miliona linija Lean-a, 29.500 međuproizvodnih teorema, oko šest milijardi izlaznih tokena iz internog modela otprilike uporedivog sa Claude Fable 5.1. Izgradnja ne uspeva osim ako se dokaz ne zasniva isključivo na Lean-ovim tri standardne aksiome: nema izvini, nema native decide, nema varanja. Provera takođe nije jeftina: jedna

2:29 izgradnja od nule trajala je pet i po sati na 96 jezgara i 153 gigabajta RAM-a, a imena teorema su mašinski generisana, tako da se repozitorijum opisuje kao napisan da se proveri, a ne da se pročita, što je takođe kako bih opisao enterprise Javu. Sada kontradikcija. Anthropic-ova objava kaže da Lean demonstrira ispravnost izvan svake sumnje. Kevin Buzzard, čovek koji je preduhitren, kompajlirao je repozitorijum na 500-gigabajtnom računaru koji mu je Anthropic pozajmio, potvrdio da se proverava, a zatim je napisao,

2:56 citat, matematički ovaj rad nam suštinski ništa ne govori. Već je bio 99,9 posto siguran da je teorema tačna, a dokaz ne dodaje novu matematiku; ono što pokazuje je šta autoformalizacija može da uradi sada, i taj deo ga iskreno uzbuđuje. Dobio je milion funti tokom pet godina; Anthropic je uzeo jedanaest dana, a komentatorova brza matematika procenjuje šest milijardi izlaznih tokena po katalog ceni 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-poruka je stigla dok je bio na muzičkom festivalu u Velsu sa jednom crticom 4G mreže, od imena za koje nikada nije čuo, pa ju je otpisao kao šalu i pročitao je nedelju dana kasnije, što je ispravan odgovor na bilo koji naslov teme koji sadrži formalizaciju od kraja do kraja. U međuvremenu, ljudi su uzvratili. Shin Jin-seo, svetski broj jedan u Gou, pobedio je KataGo, najjači open-source Go engine, sa dve partije prema jednoj u Seulu sa hendikepom od dva kamena, otprilike razlika između vrhunskog profesionalca i profesionalca početnika.

3:50 Odlučujuća partija je bila pobeda od 11,5 poena u 221 potezu, držeći 99 posto verovatnoće za pobedu od sredine partije, a kući je odneo 250 miliona vona, oko 170.000 dolara, plus Genesis G90, tako da je nagrada za pobedu nad natčovečanskom AI 170 puta veća od Guglove nagrade za beg iz Chrome sandboxa. Njegovo objašnjenje: na početku je kopirao poteze AI i izgubio; pobedio je gradeći tablu u svom stilu, što je najkorisniji savet o AI koji sam čuo cele godine, i došao je iz društvene igre. Još dva reda u diff-u.

4:22 Rust React Compiler iz oxc-a je sada native u Vite-u iza jednog flag-a; kodna baza od 1.036 fajlova je prešla sa 14,3 sekunde na 0,81 u koraku kompilacije, uglavnom brisanjem Babela iz package.json, što je ujedno i moja rutina nege 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, tako da je negde neka banka vrlo uzbuđena i niko nije pročitao licencu.

4:51 To je mnogo margine za jedan petak; ako biste radije ovo pročitali nego čuli kako ja to govorim, The Daily Diff stiže u vaše sanduče svakog jutra — besplatno na thedailydiff.dev, link ispod. Dakle, današnja presuda: SHIP IT. Kernel kaže da, Buzzard kaže da, matematika se nije promenila, ali način na koji proveravamo matematiku upravo jeste. 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