Claude បាន​បញ្ជាក់​ទ្រឹស្តីបទ Fermat ក្នុង​រយៈពេល 11 ថ្ងៃ។ សាលក្រម៖ SHIP IT។

អ្វីដែលវីដេអូនេះគ្របដណ្ដប់

• Claude ធ្វើឱ្យទ្រឹស្តីបទចុងក្រោយរបស់ Fermat មានលក្ខណៈផ្លូវការនៅក្នុង Lean 4
• Chromium sandbox RCE (CVE-2026-85046) ត្រូវបានវាយប្រហារនៅក្នុងការអនុវត្តជាក់ស្តែង រង្វាន់ 1,000 ដុល្លារ
• Shin Jin-seo ឈ្នះ KataGo ដោយមានហាងឌីខាបពីរគ្រាប់

កំណត់ត្រាដែលបានបកប្រែ

បកប្រែចេញពីការនិទានដើមជាភាសាអង់គ្លេស។ សំឡេង និងចំណងជើងរងដែលមានគឺស្ថិតនៅក្រោមការគ្រប់គ្រងរបស់ YouTube។

0:00 Fermat បាននិយាយថាភស្តុតាងដ៏អស្ចារ្យរបស់គាត់នឹងមិនសមនៅក្នុងរឹមទេ ហើយថ្ងៃនេះ Anthropic បានបោះពុម្ពរឹម៖ ដប់បីលានបន្ទាត់នៃ Lean ប្រាំដងនៃទំហំ Mathlib ដែលបញ្ជាក់ទ្រឹស្តីបទដែលគណិតវិទូគ្រប់រូបបានដឹងរួចហើយ ជឿ។ វាគឺម៉ោងដប់ទៅដប់មួយនៅ Tbilisi នៅពេលដែល Anthropic បានបង្ហោះ ដូច្នេះជាធម្មតាខ្ញុំភ្ញាក់។ ម្សិលមិញ Google បានចេញផ្សាយ Chrome 152 ជាមួយនឹងការជួសជុលសុវត្ថិភាពចំនួនដប់ពីរ មួយក្នុងចំណោមនោះគឺជាកំហុស V8 ដែលត្រូវបានវាយប្រហារនៅក្នុងការអនុវត្តជាក់ស្តែងរួចហើយ ហើយបានបង់ប្រាក់ឱ្យអ្នករាយការណ៍ មួយពាន់ដុល្លារ ដែលតិចជាងរថយន្ត sedan ដែលយើងនឹងនិយាយនៅពេលក្រោយ។

0:26 ម្សិលមិញផងដែរ Mullvad បាននិយាយថាខ្លួនកំពុងបិទ DNS ដែលបានអ៊ិនគ្រីបជាសាធារណៈរបស់ខ្លួននៅថ្ងៃ ទី 2 ខែវិច្ឆិកា ហើយបង់ប្រាក់ឱ្យ Quad9 ដើម្បីធ្វើវាជំនួសវិញ ហើយព្រឹកនេះ Rust React Compiler បានទៅកំណែដើមនៅក្នុង Vite ខណៈដែល Hacker News បានរកឃើញ IBM Bob ភ្នាក់ងារសរសេរកូដ AI ។ បន្ទាប់មក Claude បានធ្វើឱ្យទ្រឹស្តីបទចុងក្រោយរបស់ Fermat មានលក្ខណៈផ្លូវការ ហើយនៅលើទំព័រមុខដដែលនោះ មេ Go កូរ៉េម្នាក់បានឈ្នះម៉ាស៊ីន Go ខ្លាំងបំផុតនៅលើផែនដី ដូច្នេះថ្ងៃនេះមនុស្សជាតិបានទៅមួយសម្រាប់ពីរ។ នៅក្នុងវីដេអូនេះ៖ អ្វីដែល Claude បានបញ្ជាក់ពិតប្រាកដ អ្វីដែលវាបានចំណាយ

0:52 ហេតុអ្វីបានជាគណិតវិទូដែលបានចំណាយអាជីពរបស់គាត់លើរឿងនេះនិយាយថាវាមិនផ្លាស់ប្តូរអ្វីទាំងអស់ ហើយ មានសេចក្តីរីករាយយ៉ាងណាក៏ដោយ និងរបៀបដែលមនុស្សម្នាក់បានឈ្នះម៉ាស៊ីននៅ Go ។ ថ្ងៃសុក្រ ទី 4 ខែកញ្ញា ហើយនេះគឺ The Daily Diff ។ ទ្រឹស្តីបទចុងក្រោយរបស់ Fermat៖ គ្មានចំនួនគត់វិជ្ជមាន a, b, c បំពេញ a ស្វ័យគុណ n បូក b ស្វ័យគុណ n ស្មើ c ស្វ័យគុណ n សម្រាប់ n ណាមួយលើសពី 2 ។ Fermat បានសរសេរវានៅក្នុងរឹមប្រហែលឆ្នាំ 1637 ហើយបានស្លាប់ដោយមិនបានបង្ហាញការងាររបស់គាត់ ធ្វើឱ្យគាត់ក្លាយជាអ្នកអភិវឌ្ឍន៍ដំបូងគេដែលបិទសំបុត្រជាមួយ Works on my machine ។ រង្វាន់ 100,000 ម៉ាកមាសឆ្នាំ 1908 បានទាក់ទាញភស្តុតាងខុសចំនួន 621

1:25 នៅក្នុងឆ្នាំដំបូងរបស់វា ហើយ Andrew Wiles ទីបំផុតបានទទួលវានៅឆ្នាំ 1995 ក្នុង 129 ទំព័រដែលចំណាយពេលជាច្រើនខែសម្រាប់អាជ្ញាកណ្តាលដើម្បីផ្ទៀងផ្ទាត់។ ការធ្វើឱ្យមានលក្ខណៈផ្លូវការមានន័យថាការសរសេរភស្តុតាងនោះឡើងវិញដូច្នេះ Lean ជាជំនួយការភស្តុតាង អាចពិនិត្យរាល់ជំហានដោយមេកានិច ហើយ Kevin Buzzard នៅ Imperial បានដឹកនាំការខិតខំប្រឹងប្រែងរបស់មនុស្ស ដើម្បីធ្វើដូច្នេះពិតប្រាកដតាំងពីឆ្នាំ 2024; គំរូតែឯងមាន 86 ទំព័រ។ អ្នកស្រាវជ្រាវ Anthropic លោក Tianyi Peng បានចង្អុលភ្នាក់ងារ Claude រាប់សិបនាក់ទៅកាន់វា ជំនួសវិញ នៅលើវេទិកាមួយដែលមានឈ្មោះថា Prove2Me ដែលរក្សា DAG នៃទ្រឹស្តីបទ សេចក្តីថ្លែងការណ៍ដូច្នេះភ្នាក់ងារដឹងពីអ្វីដែលត្រូវបញ្ជាក់បន្ទាប់ ពីព្រោះបើគ្មានវា កងភ្នាក់ងារដំបូង

2:00 បានបាត់បង់ដានអ្នកណាដែលកំពុងបញ្ជាក់អ្វី ដែលជាអ្វីដែលកើតឡើងនៅពេលដែលស្រទាប់សម្របសម្រួលរបស់អ្នក គឺជា regex ជាមួយនឹងថវិកាទីផ្សារ។ ដប់មួយថ្ងៃក្រោយមក node ឫសបានអាន PROVED៖ ដប់បីលានបន្ទាត់នៃ Lean ទ្រឹស្តីបទមធ្យម 29,500 ប្រហែលប្រាំមួយពាន់លានថូខឹនចេញពីម៉ូដែល ខាងក្នុងដែលប្រហាក់ប្រហែលនឹង Claude Fable 5.1 ។ ការបង្កើតបរាជ័យលុះត្រាតែភស្តុតាងផ្អែកលើ Axiom ស្តង់ដារបីរបស់ Lean ពិតប្រាកដ៖ អត់ទេ អត់ native decide ទេ អត់បោកទេ ។ ការពិនិត្យមើលវាក៏មិនថោកដែរ៖ ការ

2:29 បង្កើតពីដំបូងចំណាយពេលប្រាំម៉ោងកន្លះ លើ 96 cores និង RAM 153 gigabytes ហើយឈ្មោះទ្រឹស្តីបទគឺ បង្កើតដោយម៉ាស៊ីន ដូច្នេះឃ្លាំងផ្ទុកពិពណ៌នាខ្លួនឯងថាត្រូវបានសរសេរដើម្បីពិនិត្យជាជាង អាន ដែលជាវិធីដែលខ្ញុំនឹងពិពណ៌នាអំពី enterprise Java ។ ឥឡូវនេះភាពផ្ទុយគ្នា។ ការបង្ហោះរបស់ Anthropic និយាយថា Lean បង្ហាញពីភាពត្រឹមត្រូវដោយគ្មានការសង្ស័យ។ Kevin Buzzard បុរសដែលត្រូវបានគេវាយឈ្នះ បានចងក្រងឃ្លាំងផ្ទុកនៅលើម៉ាស៊ីន 500 gigabyte ដែល Anthropic បានឱ្យគាត់ខ្ចី បានបញ្ជាក់ថាវាត្រឹមត្រូវ ហើយបន្ទាប់មកបានសរសេរ

2:56 ដកស្រង់៖ តាមគណិតវិទ្យា ការងារនេះមិនបានប្រាប់យើងអ្វីជាសំខាន់ទេ។ គាត់ប្រាកដរួចទៅហើយ 99.9 ភាគរយថាទ្រឹស្តីបទនោះជាការពិត ហើយភស្តុតាងមិនបន្ថែមគណិតវិទ្យាថ្មីទេ អ្វីដែលវាបង្ហាញគឺអ្វីដែល autoformalization អាចធ្វើបាន ឥឡូវនេះ ហើយផ្នែកនោះគាត់ពិតជារំភើបណាស់។ គាត់ត្រូវបានគេឱ្យមួយលានផោនក្នុងរយៈពេលប្រាំឆ្នាំ; Anthropic ចំណាយពេលដប់មួយថ្ងៃ ហើយការគណនាដោយដៃរបស់អ្នកអត្ថាធិប្បាយបានដាក់ថូខឹនចេញចំនួនប្រាំមួយពាន់លានក្នុងតម្លៃបញ្ជី ប្រហែល 300,000 ដុល្លារ ដូច្នេះម៉ាស៊ីនមានតម្លៃថោកជាង លើកលែងតែអ្នករាប់ការបណ្តុះបណ្តាលម៉ាស៊ីន ដែលគ្មាននរណាម្នាក់ធ្វើនោះទេ។

3:24 ព័ត៌មានលម្អិតល្អបំផុត៖ អ៊ីមែលបានមកដល់ខណៈពេលដែលគាត់កំពុងស្ថិតនៅមហោស្រពតន្ត្រីមួយក្នុងប្រទេស Wales ជាមួយ 4G មួយ​ដុំ​ពី​ឈ្មោះ​ដែល​គាត់​មិន​ធ្លាប់​ឮ ដូច្នេះ​គាត់​បាន​បដិសេធ​វា​ថា​ជា​ការ​បោកប្រាស់ ហើយបានអានវាមួយសប្តាហ៍ក្រោយមក ដែលជាការឆ្លើយតបត្រឹមត្រូវចំពោះប្រធានបទណាមួយ ដែលមានការរៀបចំជាផ្លូវការពីចុងដល់ចប់។ ទន្ទឹមនឹងនេះ មនុស្សបានទទួលបានមួយទៀត។ Shin Jin-seo ដែលជាកីឡាករលេខមួយរបស់ពិភពលោកក្នុងកីឡា 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 នៅពីក្រោយទង់មួយ; កូដបាស ដែលមាន 1,036 ឯកសារបានប្តូរពី 14.3 វិនាទីទៅ 0.81 វិនាទីនៅក្នុង ជំហាន compile ភាគច្រើនដោយការលុប Babel ចេញពី package.json ដែលជាទម្លាប់ថែរក្សាស្បែករបស់ខ្ញុំផងដែរ។ ហើយ IBM បានដាក់ឱ្យដំណើរការ Bob ដែលជាដៃគូសរសេរកូដ AI ដែលស្វាគមន៍អ្នកដោយពាក្យ Hi, ខ្ញុំគឺ Bob បង្កើត subagents ធ្វើទំនើបកម្មកូដ mainframe និងដឹកជញ្ជូនផលិតផលវិភាគមួយដែលមានឈ្មោះថា Bobalytics ដូច្នេះនៅកន្លែងណាមួយធនាគារមួយមានការ រំភើបខ្លាំងណាស់ ហើយគ្មាននរណាម្នាក់បានអានអាជ្ញាប័ណ្ណនោះទេ។

4:51 នោះ​ជា​ប្រាក់​ចំណេញ​ច្រើន​សម្រាប់​ថ្ងៃ​សុក្រ​មួយ; ប្រសិនបើអ្នកចង់អាននេះជាជាងស្តាប់ខ្ញុំ និយាយ Diff នឹងមកដល់ក្នុងប្រអប់សំបុត្ររបស់អ្នករៀងរាល់ព្រឹក – ឥតគិតថ្លៃនៅ the daily diff dot dev, តំណភ្ជាប់ខាងក្រោម។ ដូច្នេះ សាលក្រមថ្ងៃនេះ៖ SHIP IT។ Kernel និយាយថាបាទ Buzzard និយាយថាបាទ គណិតវិទ្យាមិនបានផ្លាស់ប្តូរទេ ប៉ុន្តែរបៀបដែលយើងពិនិត្យមើលគណិតវិទ្យាទើបតែបានផ្លាស់ប្តូរ។ នោះជា Diff ថ្ងៃនេះ។ ខ្ញុំ Niko មកពី 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