Claude vërtetoi Fermat-in në 11 ditë. Vendimi: SHIP IT.

Çfarë mbulon kjo video

• Claude formalizon Teoremën e Fundit të Fermat-it në Lean 4
• Chromium sandbox RCE (CVE-2026-85046), i shfrytëzuar në praktikë, shpërblim prej 1,000 $
• Shin Jin-seo mund KataGo me një handikap prej dy gurësh

Transkript i përkthyer

Përkthyer nga tregimi origjinal në anglisht. Audio dhe titrat e disponueshme kontrollohen nga YouTube.

0:00 Fermat tha se prova e tij e mrekullueshme nuk do të hynte në kufirin e faqes, dhe sot Anthropic botoi kufirin: trembëdhjetë milionë rreshta Lean, pesë herë madhësia e Mathlib, duke vërtetuar një teoremë që çdo matematikan tashmë besonte. Ishte dhjetë pa njëmbëdhjetë në Tbilisi kur Anthropic postoi, kështu që natyrisht isha zgjuar. Dje Google lansoi Chrome 152 me dymbëdhjetë rregullime sigurie, një prej tyre një gabim V8 i shfrytëzuar tashmë në praktikë, dhe pagoi raportuesin një mijë dollarë, që është më pak se sedani që do ta shohim më vonë.

0:26 Gjithashtu dje, Mullvad tha se do të mbyllë DNS-në e tij të enkriptuar publike më 2 nëntor dhe do të paguajë Quad9 për ta bërë këtë në vend, dhe këtë mëngjes Rust React Compiler u bë nativ në Vite, ndërsa Hacker News zbuloi IBM Bob, një agjent kodimi AI. Pastaj Claude formalizoi Teoremën e Fundit të Fermat-it, dhe në të njëjtën faqe të parë një grandmaster koreano mundi motorin më të fortë të Go në Tokë, kështu që sot njerëzimi bëri një nga dy. Në këtë video: çfarë provoi Claude në të vërtetë, sa kushtoi,

0:52 pse matematikani që kaloi karrierën e tij në këtë thotë se nuk ndryshon asgjë dhe është megjithatë i emocionuar, dhe si një njeri mundi makinerinë në Go. Është e premte, 4 shtator, dhe ky është The Daily Diff. Teorema e Fundit e Fermat-it: asnjë numër i plotë pozitiv a, b, c nuk plotëson a në fuqi n plus b në fuqi n baraz c në fuqi n për çdo n mbi 2. Fermat e shkroi atë në një kufi rreth vitit 1637 dhe vdiq pa treguar punën e tij, duke e bërë atë zhvilluesin e parë që mbylli një biletë me "punon në makinerinë time". Një çmim prej 100,000 markash ari në vitin 1908 tërhoqi 621 prova të gabuara

1:25 në vitin e saj të parë, dhe Andrew Wiles më në fund e mori atë në 1995, në 129 faqe që u morën gjyqtarëve muaj për t'i verifikuar. Formalizimi do të thotë rishkrimi i asaj prove në mënyrë që Lean, një asistent provash, të mund të kontrollojë çdo hap mekanikisht, dhe Kevin Buzzard në Imperial ka udhëhequr një përpjekje njerëzore për ta bërë pikërisht këtë që nga viti 2024; vetëm plani i veprimit është 86 faqe. Studiuesi i Anthropic, Tianyi Peng drejtoi dhjetëra agjentë Claude drejt saj në vend të kësaj, në një platformë të quajtur Prove2Me që mban një DAG të deklaratave të teoremës në mënyrë që agjentët të dinë çfarë të provojnë më pas, sepse pa të tufat e para

2:00 humbën gjurmët e asaj se kush po provonte çfarë, që është ajo që ndodh kur shtresa juaj e orkestrimit është regex me një buxhet marketingu. Njëmbëdhjetë ditë më vonë nyja rrënjësore lexonte PROVED: trembëdhjetë milionë rreshta Lean, 29,500 teorema të ndërmjetme, rreth gjashtë miliardë "output tokens" nga një model i brendshëm i krahasueshëm me Claude Fable 5.1. Ndërtimi dështon nëse prova nuk bazohet saktësisht në tre aksiomat standarde të Lean: jo më falni, jo decide vendase, pa mashtrime. Kontrolli i tij nuk është gjithashtu i lirë: një ndërtim

2:29 nga zeroja zgjati pesë orë e gjysmë në 96 bërthama dhe 153 gigabajt RAM, dhe emrat e teoremës janë të gjeneruar nga makina, kështu që depoja e përshkruan veten si të shkruar për t'u kontrolluar në vend që të lexohet, që është gjithashtu si do të përshkruaja Java-n e ndërmarrjes. Tani kontradikta. Postimi i Anthropic thotë se Lean demonstron saktësinë pa dyshim. Kevin Buzzard, njeriu që u mund, përpiloi depozitorin në një makinë 500-gigabajtëshe që Anthropic ia huazoi, konfirmoi se ishte në rregull, dhe pastaj shkroi,

2:56 citat, matematikisht kjo punë nuk na tregon thelbësisht asgjë. Ai ishte tashmë 99.9 për qind i sigurt se teorema ishte e vërtetë, dhe prova nuk shton matematikë të re; ajo që tregon është çfarë mund të bëjë autoformalizimi tani, dhe për këtë pjesë ai është vërtet i emocionuar. Atij iu dhanë një milion paund për pesë vjet; Anthropicit i mori njëmbëdhjetë ditë, dhe matematika e thjeshtë e një komentuesi vlerëson gjashtë miliardë "output tokens" me çmim liste rreth 300,000 dollarë, kështu që makina ishte më e lirë, përveç nëse llogaritni trajnimin e makinës, të cilën askush nuk e bën.

3:24 Detaji më i mirë: emaili mbërriti ndërsa ai ishte në një festival muzike në Uells me një shirit 4G, nga një emër që nuk e kishte dëgjuar kurrë, kështu që ai e hodhi poshtë si një mashtrim dhe e lexoi një javë më vonë, e cila është përgjigja e saktë për çdo titull lënde që përmban formalizim fund-për-fund. Ndërkohë, njerëzit fituan një pikë. Shin Jin-seo, numri një i botës në Go, mposhti KataGo, motori më i fuqishëm i Go-së me burim të hapur, dy ndeshje me një në Seul me një handicap prej dy gurësh, afërsisht hendeku midis një profesionisti të lartë dhe një profesionisti fillestar.

3:50 Vendimtaria ishte një fitore 11.5 pikëshe në 221 lëvizje, duke mbajtur një 99 për qind probabilitet fitoreje nga mesi i lojës, dhe ai mori në shtëpi 250 milionë won, rreth 170,000 dollarë, plus një Genesis G90, kështu që shpërblimi për mposhtjen e një AI supernjerëzore është 170 herë shpërblimi i Google për një ikje nga kutia e rërës së Chrome. Shpjegimi i tij: në fillim ai kopjoi lëvizjet e AI dhe humbi; ai fitoi duke ndërtuar bordin në stilin e tij, që është këshilla më e dobishme për AI që kam dëgjuar gjatë gjithë vitit, dhe ajo erdhi nga një lojë tavoline. Dy rreshta më shumë në the Daily Diff.

4:22 Përpiluesi Rust React nga oxc tani është vendas në Vite pas një flamuri; një kod bazë prej 1,036 dosjesh kaloi nga 14.3 sekonda në 0.81 në hapin e përpilimit, kryesisht duke fshirë Babel nga package.json, e cila është gjithashtu rutina ime e kujdesit të lëkurës. Dhe IBM lançoi Bob, një partner kodimi me AI që të përshëndet me Përshëndetje, Unë jam Bob, krijon nën-agjentë, modernizon kodin kryesor, dhe shpërndan një produkt analitik të quajtur Bobalytics, kështu që diku një bankë është shumë e emocionuar dhe askush nuk lexoi licencën.

4:51 Kjo është shumë diferencë për një të premte; nëse preferoni ta lexoni këtë sesa të më dëgjoni ta them, diff-i arrin në kutinë tuaj çdo mëngjes – falas në the daily diff dot dev, lidhja më poshtë. Pra, vendimi i sotëm: SHIP IT. Bërthama thotë po, Buzzard thotë po, matematika nuk ndryshoi, por mënyra si e kontrollojmë matematikën sapo ndryshoi. Ky është the daily diff i sotëm. Unë jam Niko nga Axrisi.

5:09 Bashkojeni me përgjegjësi.

Burimet

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com