Клод 11 күндө Ферманы далилдеди. Өкүм: ЖӨНӨТ.

Бул видео эмнелерди камтыйт

• Клод Ферманын Акыркы Теоремасын Lean 4 форматында формалдаштырды
• Chromium кумкоргон RCE (CVE-2026-85046), иш жүзүндө колдонулган, 1000 доллар сыйлык
• Шин Жин-сео КатаГону эки таш фора менен жеңди

Котормо стенограмма

Англис тилиндеги баштапкы баяндамадан которулган. Жеткиликтүү аудио жана коштомо жазуулар YouTube тарабынан көзөмөлдөнөт.

0:00 Ферма өзүнүн укмуштуудай далилин четке батырбасын айткан, жана бүгүн Anthropic четти жарыялады: он үч миллион сап Lean, Mathlibдин көлөмүнөн беш эсе чоң, ар бир математик буга чейин эле ишенген теореманы далилдеди. Anthropic жарыялаганда Тбилисиде ондон он бирге чейин болчу, ошондуктан мен, албетте, ойгоо болчумун. Кечээ Google Chrome 152 версиясын он эки коопсуздук оңдоолору менен чыгарды, алардын бири V8 катасы, ал буга чейин иш жүзүндө колдонулган, жана кабарчыга миң доллар төлөдү, бул кийинчерээк токтоло турган седандан аз.

0:26 Ошондой эле кечээ, Mullvad 2-ноябрда өзүнүн коомдук шифрленген DNS'ин жаап, анын ордуна Quad9га төлөөрүн айтты, жана бул эртең менен Rust React Компилятору Viteде жергиликтүү болуп иштеп кетти, ал эми Hacker News IBM Bobду, AI коддоо агентин тапты. Андан кийин Клод Ферманын Акыркы Теоремасын формалдаштырды, жана ошол эле биринчи бетте корей гроссмейстери Жердеги эң күчтүү Го кыймылдаткычын жеңди, ошондуктан бүгүн адамзат экөөнүн бирөөсүн ишке ашырды. Бул видеодо: Клод чындыгында эмнени далилдеди, ал канчага турду,

0:52 эмне үчүн карьерасын буга арнаган математик бул эч нерсени өзгөртпөйт, бирок ошентсе да кубанычта экенин айтты, жана адам Годо машинаны кантип жеңди. Бүгүн жума, 4-сентябрь, жана бул The Daily Diff. Ферманын Акыркы Теоремасы: оң бүтүн сандар a, b, c n 2ден жогору болгон каалаган n үчүн a^n + b^n = c^n теңдемесин канааттандырбайт. Ферма муну 1637-жылдары бир четке чийип, өз ишин көрсөтпөй көз жумган, аны машинамда иштейт деп билетти жапкан биринчи иштеп чыгуучу кылган. 1908-жылдагы 100 000 алтын маркалык сыйлык биринчи жылы 621 туура эмес

1:25 далилдерди өзүнө тартты, жана Эндрю Уайлс акыры 1995-жылы реферилерге текшерүү үчүн айлар талап кылынган 129 бетте аны алды. Формалдаштыруу – бул ошол далилди кайра жазуу, ошондуктан Lean, далил жардамчысы, ар бир кадамды механикалык түрдө текшере алат, жана Imperialдеги Кевин Баззард 2024-жылдан бери дал ушуну аткаруу үчүн адам күчүн жетектеп келет; бир гана долбоордун өзү 86 бетти түзөт. Anthropic изилдөөчүсү Тянйи Пенг анын ордуна ондогон Клод агенттерин Prove2Me деп аталган платформага багыттады, ал теоремалардын DAG'ын сактайт, ошондуктан агенттер кийинки эмнени далилдей турганын билишет, анткени ансыз биринчи

2:00 топтор ким эмнени далилдеп жатканын унутуп калышкан, бул сиздин оркестр катмары маркетинг бюджети бар regex болгондо болот. Он бир күндөн кийин тамыр түйүнү PROVED деп окулду: он үч миллион сап Lean, 29 500 аралык теорема, ички моделден болжол менен алты миллиард чыгыш токени, Клод Fable 5.1ге салыштырмалуу. Куруу далил Leanдин үч стандарттык аксиомасына гана негизделбесе, ишке ашпайт: жок, кечиресиз, жергиликтүү чечим жок, алдоо жок. Аны текшерүү да арзан эмес: нөлдөн

2:29 баштап куруу беш жарым саатты алды 96 ядродо жана 153 гигабайт оперативдик эс тутумда, жана теорема аттары машина тарабынан түзүлгөн, ошондуктан репо өзүн окууга караганда текшерүү үчүн жазылган деп мүнөздөйт, мен дагы enterprise Javaны ушундайча мүнөздөйт элем. Эми карама-каршылык. Anthropicтин посту Lean тууралыгын эч кандай шексиз далилдейт дейт. Кевин Баззард, бул иште жеңилген адам, Anthropic ага берген 500 гигабайттык машинада репону компиляциялап, текшерилгенин ырастап, андан кийин жазган,

2:56 цитата: математикалык жактан бул иш бизге эч нерсе айтпайт. Ал теореманын чындыгына 99,9 пайыз ишенген, жана далил жаңы математиканы кошпойт; ал автоформалдаштыруунун азыр эмне кыла аларын көрсөтөт, жана бул бөлүгү аны чындап толкундантты. Ага беш жылда бир миллион фунт берилген; Anthropic он бир күн алган, жана комментатордун эсептөөсү боюнча алты миллиард чыгыш токени тизмедеги баада. болжол менен 300,000 доллар, ошентип машина арзаныраак болду, эгер машинаны үйрөтүүнү эсепке албасаңыз, аны эч ким эсепке албайт.

3:24 Эң жакшы деталь: ал электрондук кат Уэльстеги музыкалык фестивалда жүргөндө келген, 4G бир тилкеси менен, ал эч качан укпаган ысымдан, ошондуктан ал аны тамаша катары эсептеп, бир жумадан кийин окуган, бул ар кандай темадагы сапка туура жооп. аягына чейин формалдаштырууну камтыган. Ошол эле учурда, адамдар бирин кайтарып алышты. Го боюнча дүйнөнүн биринчи номери Шин Жин-сео, КатаГону утту, эң күчтүү ачык булактуу Го кыймылдаткычын, Сеулда эки таш фора менен эки оюнду бирге утту, бул жогорку профессионал менен жаңы профессионалдын ортосундагы айырмага барабар.

3:50 Чечүүчү оюн 221 кадамда 11,5 упай менен утуш болду, орто оюннан баштап 99 пайыз утуш ыктымалдыгын кармап, ал үйүнө 250 миллион вон, болжол менен 170,000 доллар, плюс Genesis G90 алып кетти, ошентип супер-адам AI'ын жеңүү үчүн сыйлык Google'дун Chrome кумдуктан чыгуу үчүн берген сыйлыгынан 170 эсе көп. Анын түшүндүрмөсү: башында ал AI кыймылдарын көчүрүп, утулуп калган; ал утуп алган өз стилинде тактаны куруу менен, бул AI жөнүндө уккан эң пайдалуу кеңеш мен жыл бою уктум, жана ал стол оюнунан келген. diff'те дагы эки сап. oxc'тен Rust React Compiler азыр Vite'де бир желектин артында жергиликтүү; бир

4:22 1,036 файлдык код базасы компиляция кадамында 14,3 секунддан 0,81 секундга чейин кыскарган, негизинен Babel'ди package.json'дон жок кылуу менен, бул менин териге кам көрүү тартибим. Жана IBM Bob'ду ишке киргизди, бул AI коддоо өнөктөшү, ал сизди "Салам, Мен Бобмун" деп тосуп алат, суб-агенттерди түзөт, мейнфрейм кодун модернизациялайт, жана Bobalytics деп аталган аналитика продуктусун жөнөтөт, ошентип бир жерде банк абдан кубанган жана эч ким лицензияны окуган эмес. Бул бир жума күнү үчүн көп маржа; эгер сиз муну менден укканды жактырбасаңыз,

4:51 diff күн сайын эртең менен почтаңызга келет — акысыз daily diff dot dev'де, шилтеме төмөндө. Ошентип, бүгүнкү өкүм: SHIP IT. Ядро "ооба" дейт, Buzzard "ооба" дейт, математика өзгөргөн жок, бирок биз математиканы текшерүү ыкмасы жаңы эле өзгөрдү. Бүгүнкү diff ушул. Мен Axrisi'ден Никомун. Жоопкерчиликтүү түрдө бириктириңиз.

5:09 Merge responsibly.

Булактар

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