Claude-ը ապացուցեց Ֆերմային 11 օրում։ Դատավճիռը՝ SHIP IT։

Ինչ է ընդգրկում այս տեսանյութը

• Claude-ը ձևակերպում է Ֆերմայի վերջին թեորեմը Lean 4-ում
• Chromium sandbox RCE (CVE-2026-85046), շահագործված է իրականում, 1000 դոլար պարգև
• Շին Ջին-սեոն հաղթում է KataGo-ին երկքարանի հաշմանդամությամբ

Թարգմանված արձանագրություն

Թարգմանվել է բնօրինակ անգլերեն պատմությունից։ Հասանելի աուդիո և ենթագրերը վերահսկվում են 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 կոդավորող գործակալ։ Այնուհետև Claude-ը ձևակերպեց Ֆերմայի վերջին թեորեմը, և նույն առաջին էջում մի կորեական գրոսմայստեր հաղթեց Երկրի ամենաուժեղ Go շարժիչին, այնպես որ այսօր մարդկությունը մեկը երկուսից արեց։ Այս տեսանյութում. ինչ իրականում ապացուցեց Claude-ը, ինչ արժեցավ,

0:52 ինչու է մաթեմատիկոսը, ով իր կարիերան ծախսել է դրա վրա, ասում, որ դա ոչինչ չի փոխում և միևնույն է ուրախ է, և թե ինչպես մարդը հաղթեց մեքենային Go-ում։ Ուրբաթ է, սեպտեմբերի 4-ը, և սա The Daily Diff-ն է։ Ֆերմայի վերջին թեորեմը. ոչ մի դրական ամբողջ թիվ a, b, c չի բավարարում a-ի n աստիճանին գումարած b-ի n աստիճանը հավասար է c-ի n աստիճանին ցանկացած n-ի համար, որը մեծ է 2-ից։ Ֆերման այն գրեց լուսանցքում մոտ 1637 թվականին և մահացավ առանց իր աշխատանքը ցույց տալու, դարձնելով նրան առաջին մշակողը, ով փակեց տոմսը «աշխատում է իմ մեքենայում» արտահայտությամբ։ 1908 թվականի 100,000 ոսկե մարկի մրցանակն առաջին տարում գրավեց 621 սխալ

1:25 ապացույց, և Էնդրյու Ուայլսը վերջապես ստացավ այն 1995 թվականին, 129 էջում, որոնք մրցավարներից ամիսներ պահանջեցին ստուգելու համար։ Ձևակերպել նշանակում է վերագրել այդ ապացույցը այնպես, որ Lean-ը՝ ապացույցի օգնականը, կարողանա մեխանիկորեն ստուգել յուրաքանչյուր քայլ, և Կևին Բազզարդը Imperial-ից ղեկավարել է մարդկային ջանքերը՝ հենց դա անելու համար 2024 թվականից ի վեր. միայն նախագիծը կազմում է 86 էջ։ Anthropic-ի հետազոտող Տիանյի Պենգը տասնյակ Claude գործակալներ ուղղեց դրան փոխարենը, Prove2Me կոչվող հարթակում, որը պահպանում է թեորեմի DAG հայտարարություններ, որպեսզի գործակալները իմանան, թե ինչ պետք է ապացուցեն հաջորդը, քանի որ առանց դրա առաջին

2:00 երամակները կորցնում էին, թե ով ինչ է ապացուցում, ինչը տեղի է ունենում, երբ ձեր նվագախմբային շերտը regex է մարքեթինգային բյուջեով։ Տասնմեկ օր անց արմատային հանգույցում գրված էր ԱՊԱՑՈՒՑՎԱԾ. տասներեք միլիոն տող Lean, 29,500 միջանկյալ թեորեմ, մոտ վեց միլիարդ ելքային թոքեն ներքին մոդելից, մոտավորապես համեմատելի Claude Fable 5.1-ի հետ։ Կառուցումը ձախողվում է, եթե ապացույցը հիմնված չէ հենց Lean-ի երեք ստանդարտ ակսիոմների վրա. ոչ ներողություն, ոչ բնիկ որոշում, ոչ խաբեություն։ Ստուգելը նույնպես էժան չէ. մի

2:29 զրոյից կառուցումը տևեց հինգուկես ժամ 96 միջուկի և 153 գիգաբայթ օպերատիվ հիշողության վրա, իսկ թեորեմի անունները մեքենայականորեն ստեղծված են, ուստի ռեպոն իրեն նկարագրում է որպես ստուգվելու համար գրված, այլ ոչ թե կարդալու, ինչը նաև ես կնկարագրեի ձեռնարկատիրական Java-ն։ Հիմա հակասությունը։ Anthropic-ի գրառումն ասում է, որ Lean-ը կասկածից դուրս ցույց է տալիս ճշգրտությունը։ Կևին Բազզարդը՝ մարդը, ում հաղթել էին, կազմեց ռեպոն 500 գիգաբայթանոց մեքենայի վրա, որը նրան տրամադրել էր Anthropic-ը, հաստատեց, որ այն ստուգվում է, և այնուհետև գրեց,

2:56 մեջբերում, մաթեմատիկորեն այս աշխատանքն էապես ոչինչ չի ասում մեզ։ Նա արդեն 99.9 տոկոսով վստահ էր, որ թեորեմը ճիշտ է, և ապացույցը նոր մաթեմատիկա չի ավելացնում. այն, ինչ ցույց է տալիս, այն է, թե ինչ կարող է անել ավտոֆորմալիզացիան այժմ, և այդ մասից նա իսկապես ոգևորված է։ Նրան տվել էին մեկ միլիոն ֆունտ հինգ տարվա համար. Anthropic-ը պահանջեց տասնմեկ օր, և մեկնաբանի մոտավոր հաշվարկները վեց միլիարդ ելքային թոքենը գնահատում են ըստ ցուցակային գնի։ մոտ 300,000 դոլար, այնպես որ մեքենան ավելի էժան էր, եթե չհաշվեք մեքենայի մարզումը, ինչը ոչ ոք չի անում։

3:24 Լավագույն մանրամասնը. նամակը եկավ, երբ նա Ուելսի երաժշտական փառատոնում էր մեկ 4G ցանցով, մի անունից, որի մասին նա երբեք չէր լսել, ուստի նա դա համարեց կեղծիք և կարդաց մեկ շաբաթ անց, ինչը ճիշտ արձագանքն է ցանկացած թեմայի վերնագրին, որը պարունակում է «ծայրից ծայր պաշտոնականացում»։ Միևնույն ժամանակ, մարդիկ մեկ միավոր հետ բերեցին։ Շին Ջին-սեոն՝ աշխարհի թիվ մեկը Go-ում, հաղթեց KataGo-ին, ամենաուժեղ բաց կոդով Go շարժիչին, երկու խաղ մեկին Սեուլում՝ երկու քարի հաշմանդամությամբ, մոտավորապես լավագույն պրոֆեսիոնալի և նորեկ պրոֆեսիոնալի միջև եղած բացը։

3:50 Որոշիչը 11.5 միավորի հաղթանակ էր 221 քայլով՝ պահպանելով 99 տոկոս հաղթելու հավանականություն խաղի կեսից սկսած, և նա տուն տարավ 250 միլիոն վոն, մոտ 170,000 դոլար, գումարած Genesis G90, այնպես որ պարգևը գերմարդկային AI-ին հաղթելու համար 170 անգամ գերազանցում է Google-ի պարգևը Chrome sandbox-ից փախուստի համար։ Նրա բացատրությունը. սկզբում նա կրկնօրինակել է AI-ի քայլերը և պարտվել. նա հաղթել է՝ խաղատախտակը ստեղծելով իր ուրույն ոճով, ինչն AI-ի մասին ամենաօգտակար խորհուրդն է, որը ես լսել եմ այս ամբողջ տարի, և այն եկել է սեղանի խաղից։ Եվս երկու տող DIFF-ում։

4:22 Rust React Compiler-ը oxc-ից այժմ նաթիվ է Vite-ում մեկ դրոշակի հետևում. 1036 ֆայլանոց կոդային բազան 14.3 վայրկյանից դարձավ 0.81 վայրկյան կոմպիլյացիայի քայլում՝ հիմնականում Babel-ը package.json-ից ջնջելով, ինչը նաև իմ մաշկի խնամքի ռեժիմն է։ Babel-ը package.json-ից ջնջելով, ինչը նաև իմ մաշկի խնամքի ռեժիմն է։ Իսկ IBM-ը գործարկել է Bob-ը՝ AI կոդավորման գործընկեր, որը ձեզ ողջունում է «Բարև, ես Բոբն եմ» արտահայտությամբ, ստեղծում է ենթագործակալներ, արդիականացնում է մեյնֆրեյմի կոդը, և թողարկում է «Bobalytics» անունով վերլուծական արտադրանք, ուստի ինչ-որ տեղ մի բանկ շատ ոգևորված է, և ոչ ոք չի կարդացել լիցենզիան։

4:51 Դա շատ լայն շեղում է մեկ ուրբաթի համար. եթե դուք նախընտրում եք սա կարդալ, քան լսել ինձնից, ապա DIFF-ը ձեր մուտքի արկղում է ամեն առավոտ — անվճար the daily diff dot dev կայքում, հղումը՝ ներքևում։ 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