Клод 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 арваннэгдүгээр сарын 2-нд олон нийтийн шифрлэгдсэн DNS-ээ хааж, үүний оронд Quad9-д төлбөр төлж үүнийг хийлгэх болсноо хэлсэн. Харин өнөө өглөө Rust React Компьютер Vite дотор native болж, Hacker News IBM Bob-ыг олж нээсэн, AI кодын агент. Тэгээд Клод Фермагийн сүүлчийн теоремыг албан ёсны болгосон, мөн тэр л нүүр хуудсан дээр Солонгосын грандмастер Дэлхий дээрх хамгийн хүчирхэг Го хөдөлгүүрийг хожсон, тиймээс өнөөдөр хүн төрөлхтөн хоёроос нэгийг хийсэн. Энэ видеод: Клод үнэндээ юу баталсан, хэр их зардал гаргасан,

0:52 үүнд карьераа зориулсан математикч яагаад юу ч өөрчлөхгүй гэж хэлээд ямартай ч баяртай байгаа, мөн хүн Го тоглоомд машиныг хэрхэн хожсон тухай. Өнөөдөр есдүгээр сарын 4-ний Баасан гараг бөгөөд энэ бол The Daily Diff. Фермагийн сүүлчийн теорем: эерэг бүхэл тоо a, b, c n-ийн 2-оос дээш утганд 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-ийн гурван стандарт аксиом дээр яг таг тулгуурлаагүй бол build амжилтгүй болно: үгүй уучлаарай, native шийдвэр байхгүй, хууран мэхлэхгүй. Үүнийг шалгах нь хямд биш: нэг

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

2:56 иш татвал, математикийн хувьд энэ ажил бидэнд юу ч хэлэхгүй. Тэрээр теорем үнэн гэдэгт аль хэдийн 99.9 хувь итгэлтэй байсан, мөн нотолгоо шинэ математик нэмээгүй; харин энэ нь автомат формалчлал одоо юу хийж чадахыг харуулж байна, мөн тэр хэсэгтээ тэрээр үнэхээр догдолж байна. Түүнд таван жилийн хугацаанд нэг сая фунт стерлинг өгсөн; Anthropic арван нэгэн өдөр зарцуулсан, мөн сэтгэгдэл бичсэн хүний тооцоогоор зургаан тэрбум гаралтын токен жагсаалтын үнээр ойролцоогоор 300,000 доллар, тиймээс машин хямд байсан, хэрэв та машиныг сургахыг тооцохгүй бол, хэн ч тооцдоггүй.

3:24 Хамгийн сайн дэлгэрэнгүй: И-мэйл түүнийг Уэльст хөгжмийн наадамд байхад ирсэн. түүний хэзээ ч сонсож байгаагүй нэрээс 4G-ийн нэг зураастай байсан тул тэр үүнийг заваан гэж үзээд долоо хоногийн дараа уншсан нь ямар ч сэдвийн гарчигт өгөх зөв хариу юм. төгсгөлөөс төгсгөл хүртэлх албан ёсны болголт агуулсан. Үүний зэрэгцээ, хүмүүс нэг оноо авсан. Go-гийн дэлхийн нэг номер Шин Жин-со КаТаГо-г ялсан, хамгийн хүчирхэг нээлттэй эхийн Go хөдөлгүүрийг Сөүл хотод хоёр тоглоомонд нэгээр, хоёр чулууны алдаатай, шилдэг мэргэжлийн болон шинэхэн мэргэжлийн тоглогчийн хоорондох зайтай бараг ижил.

3:50 Шийдвэрлэх тоглолт 221 нүүдэлд 11.5 оноогоор ялалт байгуулж, дунд үеэс эхлэн 99 хувийн ялах магадлалтай байсан бөгөөд тэр 250 саяыг авчирсан. вон, ойролцоогоор 170,000 доллар, дээрээс нь Genesis G90, тиймээс хүнээс хэтрүү гарсан хиймэл оюун ухааныг ялсны шагнал нь Google-ийн Chrome sandbox-ийн зугтах шагналынхаас 170 дахин их. Түүний тайлбар: эхэндээ тэр хиймэл оюун ухааны нүүдлийг хуулж ялагдсан; тэр өөрийн хэв маягаар самбарыг байгуулж ялсан бөгөөд энэ нь хиймэл оюун ухааны талаар би энэ жил сонссон хамгийн хэрэгтэй зөвлөгөө бөгөөд энэ нь самбарын тоглоомоос гарсан. Ялгаанд хоёр мөр нэмэгдсэн.

4:22 oxc-аас гаралтай Rust React Компилятор одоо Vite-д нэг тугны ард үндсэн болсон; нэг 1,036 файл бүхий кодын суурь 14.3 секундээс 0.81 секунд болж эмхэтгэх алхам дээр, ихэнхдээ Babel-ийг package.json-аас устгаснаар, энэ нь миний арьс арчилгааны дэглэм юм. Мөн IBM Bob хэмээх хиймэл оюун ухааны кодчилох түншийг гаргасан бөгөөд энэ нь таныг Hi, Би Боб байна, дэд агентуудыг үүсгэдэг, үндсэн компьютерийн кодыг шинэчилдэг, мөн Bobalytics хэмээх аналитик бүтээгдэхүүнийг хүргэдэг, тиймээс хаа нэгтээ банк маш их баярлаж байгаа бөгөөд хэн ч лицензийг уншаагүй.

4:51 Энэ бол нэг баасан гарагийн хувьд ихээхэн маржин; хэрэв та үүнийг сонсохоос илүү уншихыг хүсвэл, ялгаа таны имэйлд өглөө бүр ирдэг — daily diff dot-д үнэгүй. dev, холбоос доор. Тэгэхээр, өнөөдрийн дүгнэлт: SHIP IT. Үндсэн систем тийм гэж хэлсэн, Баззард тийм гэж хэлсэн, математик өөрчлөгдөөгүй, харин бидний математикийг шалгах арга сая өөрчлөгдсөн. Энэ бол өнөөдрийн ялгаа. Би Аксиси-ийн Нико байна.

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