Клод 11 күнде Ферманы дәлелдеді. Үкім: SHIP IT.

Бұл бейне не туралы

• Клод Ферманың соңғы теоремасын Lean 4 тілінде формализациялайды
• Chromium sandbox RCE (CVE-2026-85046), өмірде пайдаланылған, 1,000 доллар сыйақы
• Шин Джин-сео екі тас гандикаппен KataGo-ны жеңді

Аударылған транскрипция

Бастапқы ағылшын тіліндегі баяндамадан аударылған. Қолжетімді аудио және субтитрлерді YouTube басқарады.

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

0:26 Сондай-ақ кеше Mullvad 2 қарашада өзінің ашық шифрланған DNS-ін жабатынын және оның орнына Quad9-ға ақы төлейтінін айтты, ал бүгін таңертең Rust React Компилятор Vite-те native болды, ал 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, дәлелдеуші көмекші, әр қадамды механикалық түрде тексере алатындай етіп қайта жазу, және Империалдағы Кевин Баззард 2024 жылдан бастап осыны істеуге адам күшін басқарды; тек жобасының өзі 86 беттен тұрады. Anthropic зерттеушісі Тиани Пенг оның орнына ондаған Клод агенттерін Prove2Me деп аталатын платформада қолданды, ол теореманың DAG-ін сақтайды мәлімдемелерін, сондықтан агенттер келесі нені дәлелдейтінін біледі, өйткені онсыз алғашқы

2:00 топтар кім нені дәлелдеп жатқанын жоғалтып алды, бұл сіздің оркестрлеу қабаты маркетингтік бюджеті бар regex болғанда болады. Он бір күннен кейін түбірлік түйін ДӘЛЕЛДЕНДІ: Lean тілінде он үш миллион жол, 29,500 аралық теорема, ішкі модельден шамамен алты миллиард шығыс токен, Клод Fable 5.1-ге шамамен тең. Егер дәлел Lean-ның үш стандартты аксиомасына ғана сүйенбесе, құрастыру сәтсіз аяқталады: жоқ, кешіріңіз, native decide жоқ, алдау жоқ. Оны тексеру де арзан емес: нөлден бастап құрастыру

2:29 тоқсан алты ядро мен 153 гигабайт жедел жадыда бес жарым сағатқа созылды, ал теорема атаулары машинамен жасалған, сондықтан репозиторий өзін оқуға емес, тексеруге арналған деп сипаттайды, бұл менің кәсіпорын Java-сын қалай сипаттайтыным сияқты. Енді қарама-қайшылық. Anthropic-тің хабарламасында Lean дұрыстығын күмәнсіз дәлелдейді делінген. Кевин Баззард, оны жеңген адам, репозиторийді Anthropic берген 500 гигабайттық машинада құрастырып, оның дұрыстығын растады, содан кейін жазды,

2:56 дәйексөз, математикалық тұрғыдан бұл жұмыс бізге еш нәрсе айтпайды. Ол теореманың дұрыстығына 99.9 пайыз сенімді болған, және дәлел жаңа математиканы қоспайды; ол тек автоформализацияның қазіргі мүмкіндігін көрсетеді, және осы бөлігі оны шынымен де қуантады. Оған бес жылға бір миллион фунт берілді; Anthropic он бір күн жұмсады, және комментатордың жуық есебі бойынша алты миллиард шығыс токен тізімдік бағамен шамамен 300 000 доллар, сондықтан машина арзан болды, егер сіз машинаны үйретуді есептемесеңіз, оны ешкім есептемейді.

3:24 Ең жақсы мәлімет: электронды хат оған Уэльстегі музыкалық фестивальде болған кезде келді, 4G бір жолағы бар, ол ешқашан естімеген есімнен, сондықтан ол оны бұрмалау деп есептеп, бір аптадан кейін оқыды, бұл кез келген тақырып жолына дұрыс жауап болып табылады, онда "end-to-end formalization" сөзі бар. Осы арада адамдар бір ұпай алды. Go ойынында әлемнің бірінші нөмірлі ойыншысы Шин Джин-сео KataGo-ны жеңді, Сеулдегі ең күшті ашық бастапқы Go қозғалтқышын екі ойында бірге екі таспен гандикаппен, бұл жоғары деңгейлі кәсіби мен жаңа кәсіби арасындағы айырмашылыққа жуық.

3:50 Шешуші ойын 221 жүрісте 11.5 ұпаймен жеңіс болды, орта ойыннан бастап 99 пайыз жеңіс ықтималдығын ұстап тұрды, және ол үйіне 250 миллион вон, шамамен 170 000 доллар, плюс Genesis G90 алып кетті, сондықтан адамнан тыс жасанды интеллектті жеңу үшін сыйақы Google-дың Chrome құмсалғышынан шығу үшін берген сыйақысынан 170 есе көп. Оның түсіндірмесі: бастапқыда ол AI қозғалыстарын көшіріп, жеңілді; ол тақтаны өз стилінде құру арқылы жеңді, бұл мен биыл AI туралы естіген ең пайдалы кеңес, және ол үстел ойынынан келді. Диф-те тағы екі жол.

4:22 oxc-тен Rust React компиляторы қазір Vite-де бір жалаушаның артында жергілікті; 1,036 файлдық код базасы компиляция қадамында 14.3 секундтан 0.81 секундқа дейін қысқарды, көбінесе Babel-ді package.json-дан жою арқылы, бұл менің тері күтімімнің тәртібі. package.json-нан Babel-ді жою арқылы, бұл менің тері күтімімнің тәртібі. Және IBM Бобты іске қосты, сізді "Сәлем, мен Бобпын" деп қарсы алатын AI кодтау серіктесі, кіші агенттерді жасайды, мейнфрейм кодын жаңартады, және Bobalytics деп аталатын аналитикалық өнімді шығарады, сондықтан бір жерде банк өте қуанышты және лицензияны ешкім оқымады.

4:51 Бір жұма үшін көп маржа; егер менің айтқанымды естігеннен гөрі мұны оқығыңыз келсе, diff әр таң сайын сіздің пошта жәшігіңізге келеді — daily diff dot dev сайтында тегін, төмендегі сілтеме. Сонымен, бүгінгі үкім: SHIP IT. Ядро "иә" дейді, Buzzard "иә" дейді, математика өзгерген жоқ, бірақ біз математиканы тексеретін әдіс өзгерді. Бұл бүгінгі 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