Клод доказао Ферма за 11 дана. Пресуда: SHIP IT.

Шта овај видео покрива

• Клод формализује Фермаову последњу теорему у Lean 4
• Chromium sandbox RCE (CVE-2026-85046), експлоатисан у природи, награда 1.000 долара
• Шин Џин-сео побеђује КатаГо са хендикепом од два камена

Преведени транскрипт

Преведено са оригиналне енглеске нарације. Доступни аудио и титлови контролисани су од стране YouTube-а.

0:00 Ферма је рекао да његов чудесан доказ неће стати на маргину, а данас је Anthropic објавио маргину: тринаест милиона линија Lean-а, пет пута већи од Mathlib-а, доказујући теорему у коју је већ сваки математичар веровао. Било је десет до једанаест у Тбилисију када је Anthropic објавио, па сам природно био будан. Јуче је Google објавио Chrome 152 са дванаест безбедносних исправки, једна од њих је V8 грешка која је већ експлоатисана у природи, и платио је извештачу хиљаду долара, што је мање од лимузине до које ћемо доћи касније.

0:26 Такође јуче, Mullvad је рекао да искључује свој јавни шифровани DNS 2. новембра и да плаћа Quad9 да то ради уместо њих, а јутрос је Rust React компајлер постао нативни у Vite-у, док је Hacker News открио IBM Bob, AI агента за кодирање. Затим је Claude формализовао Фермаову последњу теорему, а на истој насловној страни корејски велемајстор је победио најјачи Го мотор на Земљи, тако да је данас човечанство отишло један за два. У овом видеу: шта је Claude заправо доказао, колико је коштало,

0:52 зашто математичар који је провео каријеру на овоме каже да то ништа не мења и ипак је одушевљен, и како је човек победио машину у Го-у. Петак је, 4. септембар, и ово је The Daily Diff. Фермаова последња теорема: нема позитивних целих бројева а, б, ц који задовољавају а на ен плус б на ен једнако ц на ен за било које ен изнад 2. Ферма је то нажврљао на маргини око 1637. и умро не показујући свој рад, чинећи га првим програмером који је затворио тикет са „ради на мојој машини“. Награда из 1908. од 100.000 златних марака привукла је 621 погрешан

1:25 доказ у првој години, а Ендру Вајлс ју је коначно добио 1995. године, у 129 страница које су судије месецима проверавале. Формализација значи преписивање тог доказа тако да Lean, асистент за доказе, може механички да провери сваки корак, а Кевин Базард са Империјала је предводио људски напор да уради управо то од 2024. године; само нацрт има 86 страница. Истраживач Anthropic-а Тиањи Пенг усмерио је десетине Claude агената на то уместо тога, на платформи званој Prove2Me која чува DAG изјава теорема тако да агенти знају шта да докажу следеће, јер без тога први

2:00 ројеви су изгубили траг ко шта доказује, што се дешава када ваш слој оркестрације је regex са маркетиншким буџетом. Једанаест дана касније коренски чвор је гласио ПРОКАЗАНО: тринаест милиона линија Lean-а, 29.500 међутеорија, око шест милијарди излазних токена из интерног модела приближно упоредивог са Claude Fable 5.1. Изградња не успева осим ако доказ не почива на тачно Lean-овим три стандардна аксиома: не, извините, нема нативне одлуке, без варања. Провера такође није јефтина: изградња

2:29 од нуле трајала је пет и по сати на 96 језгара и 153 гигабајта RAM-а, а имена теорема су машински генерисана, тако да се репозиторијум описује као написан да се провери, а не прочита, што је и како бих описао enterprise Java. Сада контрадикција. Објава Anthropic-а каже да Lean доказује исправност без сумње. Кевин Базард, човек који је био престигнут, компајлирао је репозиторијум на машини од 500 гигабајта коју му је Anthropic позајмио, потврдио да је проверена, а затим написао,

2:56 цитат, математички овај рад нам суштински ништа не говори. Већ је био 99,9 посто сигуран да је теорема истинита, а доказ не додаје нову математику; оно што показује је шта аутоформализација може да уради сада, и тај део га искрено узбуђује. Добио је милион фунти током пет година; Anthropic је требао једанаест дана, а прорачун на салвети коментатора ставља шест милијарди излазних токена по цени из каталога око 300.000 долара, тако да је машина била јефтинија, осим ако не рачунате обуку машине, што нико не ради.

3:24 Најбољи детаљ: имејл је стигао док је био на музичком фестивалу у Велсу са једном цртом 4Г мреже, од имена за које никада није чуо, па га је отписао као шалу и прочитао га недељу дана касније, што је исправан одговор на било који наслов који садржи „end-to-end formalization“. У међувремену, људи су узвратили. Шин Ђин-сео, светски број један у Го-у, победио је KataGo, најјачи Го енџин отвореног кода, два према један у Сеулу са хендикепом од два камена, отприлике толико је разлика између врхунског професионалца и професионалца почетника.

3:50 Одлучујућа партија је била победа од 11,5 поена у 221 потезу, држећи 99 процената вероватноће победе од средине игре, а кући је однео 250 милиона вона, око 170.000 долара, плус Genesis G90, тако да је награда за победу над суперхуманом АИ 170 пута већа од Google-ове награде за бекство из Chrome sandbox-а. Његово објашњење: на почетку је копирао потезе АИ и губио; победио је градећи таблу у свом стилу, што је најкориснији савет о АИ који сам чуо ове године, и дошао је из друштвене игре. Још две линије у The Daily Diff.

4:22 Rust React компајлер из oxc-а је сада нативни у Vite-у иза једне заставе; база кода са 1.036 датотека је прешла са 14,3 секунде на 0,81 у кораку компилације, углавном брисањем Babel-а из package.json, што је такође моја рутина неге коже. А IBM је лансирао Bob-а, АИ партнера за кодирање који вас поздравља са „Здраво, ја сам Боб“, ствара субагенте, модернизује мејнфрејм код, и испоручује аналитички производ под називом Bobalytics, тако да је негде нека банка веома узбуђена и нико није прочитао лиценцу.

4:51 То је велика маржа за један петак; ако више волите да ово прочитате него да ме чујете како то говорим, The Daily Diff вам стиже у инбокс сваког јутра — бесплатно на thedailydiff.dev, линк испод. Дакле, данашња пресуда: SHIP IT. Кернел каже да, Buzzard каже да, математика се није променила, али начин на који проверавамо математику јесте. То је данашњи The Daily Diff. Ја сам Нико из Axrisi-ја.

5:09 Спајајте одговорно.

Извори

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