क्लाउड ने 11 दिनों में फर्मेट को सिद्ध किया। फैसला: SHIP IT।

इस वीडियो में क्या शामिल है

• क्लाउड लीन 4 में फर्मेट के अंतिम प्रमेय को औपचारिक रूप देता है
• क्रोमियम सैंडबॉक्स RCE (CVE-2026-85046), जिसका वास्तविक दुनिया में फायदा उठाया गया, $1,000 का इनाम
• शिन जिन-सियो ने दो-पत्थर के हैंडीकैप के साथ KataGo को हराया

अनुवादित प्रतिलेख

मूल अंग्रेजी कथन से अनुवादित। उपलब्ध ऑडियो और कैप्शन YouTube द्वारा नियंत्रित होते हैं।

0:00 फर्मेट ने कहा था कि उनका अद्भुत प्रमाण हाशिया में फिट नहीं होगा, और आज एंथ्रोपिक ने हाशिया प्रकाशित किया: तेरह मिलियन लाइनें लीन की, मैथलिब के आकार का पांच गुना, एक प्रमेय को साबित करते हुए जिसे हर गणितज्ञ पहले से ही मानता था। जब एंथ्रोपिक ने पोस्ट किया तब त्बिलिसी में दस से ग्यारह बज रहे थे, इसलिए स्वाभाविक रूप से मैं जाग रहा था। कल Google ने क्रोम 152 को बारह सुरक्षा फिक्स के साथ शिप किया, उनमें से एक V8 बग था जिसका पहले से ही वास्तविक दुनिया में फायदा उठाया जा रहा था, और रिपोर्टर को एक हजार डॉलर का भुगतान किया, जो उस सेडान से कम है जिसके बारे में हम बाद में बात करेंगे।

0:26 कल भी, मुल्लावड ने कहा कि वह 2 नवंबर को अपनी सार्वजनिक एन्क्रिप्टेड DNS बंद कर रहा है और इसके बजाय क्वाड9 को ऐसा करने के लिए भुगतान कर रहा है, और आज सुबह रस्ट रिएक्ट कंपाइलर Vite में नेटिव हो गया, जबकि हैकर न्यूज ने IBM बॉब, एक 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 पृष्ठों में जिसे रेफरी को सत्यापित करने में महीनों लग गए। औपचारिक रूप देने का मतलब है उस प्रमाण को फिर से लिखना ताकि लीन, एक प्रूफ सहायक, हर कदम को यांत्रिक रूप से जांच सके, और इंपीरियल के केविन बज़ार्ड ने 2024 से ठीक ऐसा करने के लिए एक मानवीय प्रयास का नेतृत्व किया है; अकेले ब्लूप्रिंट 86 पृष्ठों का है। एंथ्रोपिक शोधकर्ता टियानयी पेंग ने इसके बजाय दर्जनों क्लाउड एजेंटों को Prove2Me नामक एक प्लेटफॉर्म पर लगाया, प्लेटफॉर्म पर लगाया, जो प्रमेय कथनों का एक DAG रखता है ताकि एजेंटों को पता चले कि आगे क्या साबित करना है, क्योंकि इसके बिना पहले झुंड यह भूल गए कि कौन क्या साबित कर रहा था, जो तब होता है जब आपकी

2:00 ऑर्केस्ट्रेशन लेयर मार्केटिंग बजट के साथ रेग्युलर एक्सप्रेशन होती है। ग्यारह दिन बाद रूट नोड ने PROVED पढ़ा: तेरह मिलियन लाइनें लीन की, 29,500 मध्यवर्ती प्रमेय, एक आंतरिक मॉडल से लगभग छह बिलियन आउटपुट टोकन जो मोटे तौर पर क्लाउड फेबल 5.1 के बराबर है। बिल्ड विफल हो जाता है जब तक कि प्रूफ लीन के तीन मानक स्वयंसिद्धों पर आधारित न हो: नहीं, क्षमा करें, कोई मूल निर्णय नहीं, कोई धोखा नहीं। इसे जांचना भी सस्ता नहीं है: 96 कोर और 153 गीगाबाइट रैम पर खरोंच से एक बिल्ड को साढ़े पांच घंटे लगे,

2:29 और प्रमेय के नाम मशीन-जनरेटेड हैं, इसलिए रेपो खुद को पढ़ने के बजाय जांचने के लिए लिखे गए के रूप में वर्णित करता है, जो कि मैं एंटरप्राइज जावा का वर्णन भी कैसे करूंगा। अब विरोधाभास। एंथ्रोपिक की पोस्ट कहती है कि लीन संदेह से परे शुद्धता प्रदर्शित करता है। केविन बज़ार्ड, वह व्यक्ति जिसे इसमें हराया गया था, ने एंथ्रोपिक द्वारा उन्हें उधार दी गई 500-गीगाबाइट मशीन पर रेपो को संकलित किया, पुष्टि की कि यह ठीक है, और फिर लिखा, उद्धरण, गणितीय रूप से यह काम हमें अनिवार्य रूप से कुछ नहीं बताता। वह पहले से ही 99.9 प्रतिशत सुनिश्चित थे कि प्रमेय सत्य था,

2:56 और प्रूफ कोई नया गणित नहीं जोड़ता; यह जो दिखाता है वह यह है कि ऑटोफॉर्मलाइजेशन अब क्या कर सकता है, और उस हिस्से के बारे में वह वास्तव में उत्साहित हैं। उन्हें पांच साल में एक मिलियन पाउंड दिए गए थे; एंथ्रोपिक को ग्यारह दिन लगे, और एक टिप्पणीकार के नैपकिन गणित के अनुसार छह बिलियन आउटपुट टोकन सूची मूल्य पर हैं। और एक टिप्पणीकार के नैपकिन गणित के अनुसार छह बिलियन आउटपुट टोकन सूची मूल्य पर हैं। और एक टिप्पणीकार के नैपकिन गणित के अनुसार छह बिलियन आउटपुट टोकन सूची मूल्य पर हैं। लगभग 300,000 डॉलर, तो मशीन सस्ती थी, जब तक आप मशीन को प्रशिक्षित करने की गणना नहीं करते हैं, जो कोई नहीं करता।

3:24 सबसे अच्छा विवरण: जब वह वेल्स में एक संगीत समारोह में था, तब ईमेल आया था, एक 4G बार के साथ, एक ऐसे नाम से जिसे उसने कभी नहीं सुना था, इसलिए उसने इसे एक सनक मान लिया और एक सप्ताह बाद इसे पढ़ा, जो किसी भी विषय पंक्ति के लिए सही प्रतिक्रिया है जिसमें एंड-टू-एंड औपचारिकता शामिल हो। इस बीच, मनुष्यों को एक वापस मिल गया। शि जिन-सेओ, गो में दुनिया के नंबर एक, ने कटागो को हराया, सबसे शक्तिशाली ओपन-सोर्स गो इंजन, सियोल में दो गेम से एक, दो-पत्थर के साथ हैंडीकैप, मोटे तौर पर एक शीर्ष पेशेवर और एक नौसिखिया पेशेवर के बीच का अंतर।

3:50 निर्णायक 221 चालों में 11.5 अंकों की जीत थी, जिसमें मध्य-खेल से 99 प्रतिशत जीत की संभावना थी, और उसने 250 मिलियन घर ले लिए वॉन, लगभग 170,000 डॉलर, साथ ही एक जेनेसिस G90, तो एक अलौकिक AI को हराने का इनाम Google के क्रोम सैंडबॉक्स से 170 गुना है पलायन। उनकी व्याख्या: शुरुआत में उन्होंने AI चालों की नकल की और हार गए; उन्होंने अपने स्वयं की शैली में बोर्ड का निर्माण करके जीता, जो AI के बारे में सबसे उपयोगी सलाह है जो मैंने पूरे साल सुनी है, और यह एक बोर्ड गेम से आई थी। अंतर में दो और पंक्तियाँ।

4:22 oxc से रस्ट रिएक्ट कंपाइलर अब एक फ्लैग के पीछे वाइट में मूल निवासी है; एक 1,036-फ़ाइल कोडबेस संकलन चरण में 14.3 सेकंड से 0.81 हो गया, ज्यादातर package.json से बैबेल को हटाकर, जो मेरी स्किनकेयर दिनचर्या भी है। पैकेज.जेएसएन से बैबेल को हटाकर, जो मेरी त्वचा देखभाल की दिनचर्या भी है। और IBM ने बॉब लॉन्च किया, एक AI कोडिंग पार्टनर जो आपको Hi, से अभिवादन करता है, मैं बॉब हूँ, उप-एजेंट बनाता है, मेनफ्रेम कोड का आधुनिकीकरण करता है, और Bobalytics नामक एक एनालिटिक्स उत्पाद भेजता है, इसलिए कहीं एक बैंक बहुत उत्साहित है और किसी ने लाइसेंस नहीं पढ़ा।

4:51 एक शुक्रवार के लिए यह बहुत अधिक मार्जिन है; यदि आप इसे पढ़ने के बजाय मुझे इसे कहते हुए सुनना चाहते हैं, तो द डेली डिफ हर सुबह आपके इनबॉक्स में आता है — the 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