# Claude je dokazal Ferma v 11 dneh. Sodba: SHIP IT.

Published: 2026-09-07

Claude je v 11 dneh in z okoli 6 milijardami žetonov napisal 13-milijonsko dolg dokaz Fermatovega zadnjega izreka v Lean-u — prvega, ki ga je v celoti preveril računalnik — medtem ko matematik, ki ga formalizira od leta 2024, pravi, da "nam matematično ne pove bistveno nič" in je kljub temu navdušen. Isti dan: Go svetovni št. 1 Shin Jin-seo premaga KataGo z 2–1 z dvema kamnitim hendikepom. Sodba: SHIP IT.

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

## Kaj zajema ta videoposnetek

- Claude formalizira Fermatov zadnji izrek v Lean 4
- Chromium sandbox RCE (CVE-2026-85046), izkoriščen v naravi, nagrada 1.000 $
- Shin Jin-seo premaga KataGo z dvema kamnitim hendikepom

## Preveden prepis

Prevedeno iz izvirnega angleškega pripovedovanja. Razpoložljivi zvok in podnapisi so nadzorovani s strani YouTuba.

0:00 Fermat je dejal, da njegov čudovit dokaz ne bi ustrezal v rob, in danes je Anthropic objavil rob: trinajst milijonov vrstic Lean-a, petkrat večji kot Mathlib, ki dokazuje izrek, ki ga je vsak matematik že verjel. V Tbilisiju je bilo deset do enajst, ko je Anthropic objavil, zato sem bil seveda buden. Včeraj je Google izdal Chrome 152 z dvanajstimi varnostnimi popravki, eden izmed njih je bila napaka V8, ki je bila že izkoriščena v naravi, in je poravnal poročevalcu tisoč dolarjev, kar je manj kot limuzina, ki jo bomo omenili kasneje.

0:26 Prav tako včeraj je Mullvad sporočil, da bo zaprl svoj javni šifrirani DNS dne 2. novembra in namesto tega plačal Quad9, in danes zjutraj je Rust React Compiler postal izvorni v Vitu, medtem ko je Hacker News odkril IBM Bob, agenta za kodiranje z umetno inteligenco. Potem je Claude formaliziral Fermatov zadnji izrek, in na isti prvi strani je korejski velemojster premagal najmočnejši Go motor na Zemlji, zato je danes človeštvo uspelo enega od dveh. V tem videu: kaj je Claude dejansko dokazal, koliko je to stalo,

0:52 zakaj matematik, ki je svojo kariero posvetil temu, pravi, da to nič ne spremeni in je kljub temu navdušen, in kako je človek premagal stroj v Go-ju. Petek, 4. september, in to je The Daily Diff. Fermatov zadnji izrek: ni pozitivnih celih števil a, b, c ki izpolnjujejo a na n plus b na n enako c na n za kateri koli n nad 2. Fermat je to zapisal na rob okoli leta 1637 in umrl, ne da bi pokazal svoje delo, s čimer je postal prvi razvijalec, ki je zaprl prijavo z "deluje na mojem stroju". Nagrada 100.000 zlatih mark leta 1908 je v prvem letu privabila 621 napačnih

1:25 dokazov, in Andrew Wiles ga je končno dobil leta 1995, na 129 straneh, ki so jih sodniki preverjali mesece. Formalizacija pomeni prepisovanje tega dokaza, tako da Lean, pomočnik za dokazovanje, lahko mehansko preveri vsak korak, in Kevin Buzzard z Imperiala je vodil človeška prizadevanja, da bi to storil natanko tako od leta 2024; sam načrt obsega 86 strani. Raziskovalec Anthropic Tianyi Peng je namesto tega usmeril desetine agentov Claude-a k temu na platformi Prove2Me, ki hrani DAG izrečnih izjav, da agenti vedo, kaj dokazati naslednje, ker brez tega so prvi

2:00 roji izgubili sled o tem, kdo kaj dokazuje, kar se zgodi, ko je vaša orkestracijska plast regex z marketinškim proračunom. Enajst dni pozneje je korensko vozlišče bralo DOKAZANO: trinajst milijonov vrstic Lean-a, 29.500 vmesnih izrekov, približno šest milijard izhodnih žetonov iz notranjega modela, ki je bil približno primerljiv s Claude Fable 5.1. Izgradnja ne uspe, razen če dokaz temelji na Lean-ovih treh standardnih aksiomih: ne, žal, brez izvornega odločanja, brez goljufanja. Preverjanje tudi ni poceni: izgradnja

2:29 iz nič je trajala pet ur in pol na 96 jedrih in 153 gigabajtih RAM-a, imena izrekov pa so strojno generirana, zato repozitorij sam sebe opisuje kot napisanega za preverjanje in ne za branje, kar bi opisal tudi za enterprise Javo. Zdaj protislovje. Anthropicova objava pravi, da Lean dokazuje pravilnost onkraj dvoma. Kevin Buzzard, mož, ki so ga prehiteli, je prevedel repozitorij na 500-gigabajtnem stroju, ki mu ga je posodil Anthropic, potrdil, da je preverjen, nato pa napisal,

2:56 citat, matematično nam to delo ne pove bistveno nič. Že 99,9 odstotka je bil prepričan, da je izrek resničen, in dokaz ne dodaja nobene nove matematike; kar kaže, je, kaj lahko avtoformalizacija stori zdaj, in glede tega je resnično navdušen. Dobili so mu milijon funtov v petih letih; Anthropic je potreboval enajst dni, in komentatorjeva hitra ocena postavi šest milijard izhodnih žetonov po ceniku okoli 300.000 dolarjev, tako da je bil stroj cenejši, razen če ne štejete usposabljanja stroja, česar pa nihče ne dela.

3:24 Najboljša podrobnost: e-pošta je prispela, ko je bil na glasbenem festivalu v Walesu z eno črtico 4G, od imena, za katerega še nikoli ni slišal, zato ga je odpisal kot potegavščino in ga prebral teden dni kasneje, kar je pravilen odziv na vsako zadevo e-pošte, ki vsebuje celovito formalizacijo. Medtem so ljudje dobili eno nazaj. Shin Jin-seo, svetovna številka ena v igri Go, je premagal KataGo, najmočnejši odprtokodni Go pogon, dve igri proti ena v Seulu z dvema kamnitim hendikepom, kar je približno razlika med vrhunskim profesionalcem in profesionalcem novincem.

3:50 Odločilna je bila zmaga z 11,5 točke v 221 potezah, z 99-odstotno verjetnostjo zmage od sredine igre naprej, in domov je odnesel 250 milijonov won, približno 170.000 dolarjev, plus Genesis G90, tako da je nagrada za premaganje nadčloveške umetne inteligence 170-krat večja od Googleove nagrade za Chrome sandbox pobeg. Njegova razlaga: na začetku je kopiral poteze umetne inteligence in izgubil; zmagal je z gradnjo plošče v svojem slogu, kar je najbolj uporaben nasvet o umetni inteligenci, ki sem ga slišal v vsem letu, in prišel je iz družabne igre. Še dve vrstici v The Daily Diff.

4:22 Rust React Compiler iz oxc je zdaj naraven v Vitu za eno zastavico; kodna baza z 1.036 datotekami je prešla iz 14,3 sekund na 0,81 v koraku prevajanja, večinoma z brisanjem Babel iz package.json, kar je tudi moja rutina nege kože. In IBM je lansiral Boba, AI partnerja za kodiranje, ki vas pozdravi z "Živjo, Jaz sem Bob," ustvarja podagente, posodablja kodo glavnega računalnika, in pošilja analitični izdelek, imenovan Bobalytics, tako da je nekje banka zelo navdušena in nihče ni prebral licence.

4:51 To je veliko marže za en petek; če raje to preberete, kot da me slišite to izgovoriti, The Daily Diff pristane v vašem nabiralniku vsako jutro — brezplačno na thedailydiff.dev, povezava spodaj. Torej, današnja sodba: SHIP IT. Kernel pravi da, Buzzard pravi da, matematika se ni spremenila, vendar se je pravkar spremenil način, kako preverjamo matematiko. To je današnji The Daily Diff. Sem Niko iz Axrisija.

5:09 Združujte odgovorno.

## Viri

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