Клод го докажа Ферма за 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, агент за кодирање со вештачка интелигенција. Потоа Клод ја формализира Последната теорема на Ферма, а на истата насловна страница корејски велемајстор го победи најсилниот Go мотор на Земјата, па денес човештвото освои еден од два. Во ова видео: што всушност докажа Клод, колку чинеше,

0:52 зошто математичарот кој ја помина својата кариера на ова вели дека тоа ништо не менува и е сепак воодушевен, и како човек ја победи машината во Go. Петок е, 4 септември, и ова е The Daily Diff. Последната теорема на Ферма: нема позитивни цели броеви a, b, c кои го задоволуваат a на n плус b на n еднакво на c на n за било кој n над 2. Ферма го напиша тоа на маргина околу 1637 година и умре без да ја покаже својата работа, правејќи го првиот програмер што затворил тикет со работи на мојата машина. Награда од 100.000 златни марки во 1908 година привлече 621 погрешен

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

2:00 ројви изгубија трага кој што докажува, што се случува кога вашиот слој за оркестрација е регуларен израз со маркетинг буџет. Единаесет дена подоцна, кореновиот јазол прочита ДОКАЖАНО: тринаесет милиони линии Lean, 29.500 меѓусредни теореми, околу шест милијарди излезни токени од внатрешен модел приближно споредлив со Claude Fable 5.1. Изградбата пропаѓа освен ако доказот не се заснова на точно трите стандардни аксиоми на Lean: не, извинете, нема нативна одлука, нема мамење. Проверката исто така не е евтина: изградба од нула

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

2:56 цитат, математички оваа работа ни кажува во суштина ништо. Тој веќе беше 99,9 проценти сигурен дека теоремата е вистинита, и доказот не додава нова математика; она што го покажува е што може да направи автоматското формализирање сега, и тој дел е навистина возбуден поради тоа. Му беа дадени еден милион фунти за пет години; на Anthropic и требаа единаесет дена, и пресметките на коментаторот ставаат шест милијарди излезни токени по основна цена. околу 300.000 долари, па машината беше поевтина, освен ако не ја сметате обуката на машината, што никој не го прави.

3:24 Најдобар детал: е-поштата пристигнала додека тој бил на музички фестивал во Велс со една цртичка 4G, од име за кое никогаш не слушнал, па ја отпишал како шега и ја прочитал една недела подоцна, што е точен одговор на која било насловна линија што содржи целосна формализација. Во меѓувреме, луѓето си вратија. Шин Џин-сео, светскиот број еден во Го, го победи КатаГо, најсилниот open-source Go мотор, два натпревари против еден во Сеул со хендикеп од два камена, приближно јазот помеѓу врвен професионалец и професионалец почетник.

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 го лансираше Боб, партнер за кодирање со вештачка интелигенција кој ве поздравува со Здраво, Јас сум Боб, создава под-агенти, го модернизира кодот на главниот компјутер, и испорачува аналитички производ наречен Bobalytics, така што некаде некоја банка е многу возбудена и никој не ја прочитал лиценцата.

4:51 Тоа е многу маржа за еден петок; ако повеќе сакате да го прочитате ова отколку да ме слушнете како го кажувам, The Daily Diff пристигнува во вашето сандаче секое утро — бесплатно на daily diff dot 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