क्लॉडने 11 दिवसांत फर्मट सिद्ध केले. निकाल: SHIP IT.

या व्हिडिओमध्ये काय समाविष्ट आहे

• क्लॉडने लीन 4 मध्ये फर्मटच्या शेवटच्या प्रमेयाचे औपचारिकीकरण केले
• क्रोमियम सँडबॉक्स आरसीई (CVE-2026-85046), प्रत्यक्षात वापरले गेले, $1,000 बक्षीस
• शिन जिन-सेओने दोन-दगडांच्या हँडिकॅपसह काटागोला हरवले

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

मूळ इंग्रजी निवेदनातून अनुवादित. उपलब्ध ऑडिओ आणि मथळे YouTube द्वारे नियंत्रित आहेत.

0:00 फर्मट म्हणाले की त्यांची अद्भुत सिद्धता मार्जिनमध्ये बसणार नाही, आणि आज ॲन्थ्रोपिकने मार्जिन प्रकाशित केले: तेरा दशलक्ष ओळींचे लीन, मॅथलिबच्या आकाराच्या पाच पट, असे प्रमेय सिद्ध केले जे प्रत्येक गणितज्ञांना आधीच माहित होते. ॲन्थ्रोपिकने पोस्ट केले तेव्हा तिबिलिसीमध्ये रात्री दहा ते अकरा वाजले होते, त्यामुळे साहजिकच मी जागा होतो. काल Google ने Chrome 152 बारा सुरक्षा दुरुस्त्यांसह शिप केले, त्यापैकी एक V8 बग प्रत्यक्षात वापरला गेला होता, आणि रिपोर्टरला एक हजार डॉलर्स दिले, जे आपण नंतर बोलणार असलेल्या सेडानपेक्षा कमी आहे.

0:26 कालच, मुल्व्हॅडने म्हटले की ते 2 नोव्हेंबर रोजी त्यांचे सार्वजनिक एनक्रिप्टेड डीएनएस बंद करत आहे आणि त्याऐवजी क्वाड9 ला पैसे देत आहे, आणि आज सकाळी रस्ट रिएक्ट कम्पाइलर वाइटमध्ये मूळ स्वरूपात आले, तर हॅकर न्यूजने आयबीएम बॉब, एक एआय कोडिंग एजंट शोधला. नंतर क्लॉडने फर्मटच्या शेवटच्या प्रमेयाचे औपचारिकीकरण केले, आणि त्याच पहिल्या पानावर एक कोरियन ग्रँडमास्टरने पृथ्वीवरील सर्वात शक्तिशाली गो इंजिनला हरवले, त्यामुळे आज मानवजातीने दोनपैकी एक जिंकले. या व्हिडिओमध्ये: क्लॉडने प्रत्यक्षात काय सिद्ध केले, त्यासाठी किती खर्च आला,

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 पानांची आहे. ॲन्थ्रोपिक संशोधक तियानी पेंगने त्याऐवजी डझनभर क्लॉड एजंट्सना प्रूफ2मी नावाच्या प्लॅटफॉर्मवर निर्देशित केले, जो प्रमेय विधानांचा डीएजी (DAG) ठेवतो जेणेकरून एजंट्सना पुढे काय सिद्ध करायचे ते माहित असते, कारण त्याशिवाय पहिल्या

2:00 समूहांना कोण काय सिद्ध करत आहे याचा मागोवा लागत नव्हता, जे तुमच्या ऑर्केस्ट्रेशन लेयरमध्ये मार्केटिंग बजेटसह रेगएक्स (regex) असते तेव्हा होते. अकरा दिवसांनंतर मूळ नोडवर PROVED असे होते: तेरा दशलक्ष ओळींचे लीन, 29,500 मध्यवर्ती प्रमेय, अंदाजे सहा अब्ज आउटपुट टोकन्स क्लॉड फेबल 5.1 सारख्या अंतर्गत मॉडेलमधून. जर सिद्धता केवळ लीनच्या तीन मानक स्वयंसिद्धांतांवर आधारित नसेल तर बिल्ड अयशस्वी होतो: नाही माफ करा, मूळ निर्णय नाही, फसवणूक नाही. त्याची तपासणी करणे स्वस्त नाही: एक

2:29 सुरवातीपासून बिल्ड करण्यासाठी साडेपाच तास लागले 96 कोअर आणि 153 गिगाबाइट्स रॅमवर, आणि प्रमेयांची नावे मशीन-जनरेटेड आहेत, त्यामुळे रेपो स्वतःचे वर्णन वाचण्याऐवजी तपासणीसाठी लिहिलेले असे करतो, जे मी एंटरप्राइज जावाचे वर्णन कसे करेन ते देखील आहे. आता विरोधाभास. ॲन्थ्रोपिकच्या पोस्टमध्ये म्हटले आहे की लीन अचूकता निःसंशयपणे सिद्ध करते. केविन बझार्ड, ज्याला मागे टाकण्यात आले होते, त्यांनी ॲन्थ्रोपिकने त्यांना दिलेल्या 500-गिगाबाइट मशीनवर रेपो संकलित केले, ते तपासले असल्याची खात्री केली, आणि नंतर लिहिले,

2:56 कोट, गणिताच्या दृष्टीने हे काम आपल्याला काहीही सांगत नाही. त्यांना आधीच 99.9 टक्के खात्री होती की प्रमेय खरे आहे, आणि ही सिद्धता कोणतेही नवीन गणित जोडत नाही; ती काय दाखवते ते म्हणजे ऑटोफॉर्मलायझेशन आता काय करू शकते, आणि त्या भागाबद्दल ते खरोखरच उत्सुक आहेत. त्यांना पाच वर्षांसाठी एक दशलक्ष पाउंड दिले होते; ॲन्थ्रोपिकला अकरा दिवस लागले, आणि एका टिप्पणीकर्त्याच्या जलद गणनेनुसार सहा अब्ज आउटपुट टोकन्सची किंमत सूची दरावर येते सुमारे 300,000 डॉलर्स, त्यामुळे मशीन स्वस्त होते, जोपर्यंत तुम्ही मशीनला प्रशिक्षण देण्याची गणना करत नाही, जे कोणीही करत नाही.

3:24 सर्वोत्तम तपशील: तो वेल्समधील एका संगीत महोत्सवात असताना त्याला ईमेल आला, एका 4G बारसह, अशा नावाकडून जे त्याने कधीही ऐकले नव्हते, म्हणून त्याने ते एक क्रँक मानले, आणि एका आठवड्यानंतर वाचले, जो कोणत्याही विषय ओळीला योग्य प्रतिसाद आहे, ज्यात एंड-टू-एंड औपचारिकीकरण समाविष्ट आहे. दरम्यान, मानवांना एक परत मिळाले. गोमधील जगातील नंबर एक, शिन जिन-सिओने, काटागोला हरवले, सर्वात शक्तिशाली ओपन-सोर्स गो इंजिन, सोलमध्ये दोन-स्टोनच्या हँडिकॅपसह दोन गेममध्ये एकाने हरवले, जो एक अव्वल व्यावसायिक आणि एक नवशिक्या व्यावसायिक यांच्यातील अंदाजे अंतर आहे.

3:50 निर्णायक सामना 221 चालींमध्ये 11.5-पॉइंट्सच्या फरकाने जिंकला, मध्य-गेमपासून 99 टक्के जिंकण्याची शक्यता कायम ठेवली, आणि त्याने 250 मिलियन वॉन, सुमारे 170,000 डॉलर्स, तसेच एक जेनेसिस G90, घरी नेले, त्यामुळे एका अलौकिक एआयला हरवण्यासाठीचे बक्षीस गुगलच्या क्रोम सँडबॉक्स एस्केपसाठी असलेल्या बक्षीसापेक्षा 170 पट जास्त आहे. त्याचे स्पष्टीकरण: सुरुवातीला त्याने एआयच्या चालींची कॉपी केली आणि हरला; तो स्वतःच्या शैलीत बोर्ड तयार करून जिंकला, जो मला या वर्षातील एआयबद्दल ऐकलेला सर्वात उपयुक्त सल्ला आहे, आणि तो एका बोर्ड गेममधून आला. diff मध्ये आणखी दोन ओळी.

4:22 oxc मधील रस्ट रिॲक्ट कंपाइलर आता एका ध्वजामागे वाइटमध्ये नेटिव्ह आहे; एक 1,036-फाइल कोडबेस संकलन टप्प्यात 14.3 सेकंदांवरून 0.81 सेकंदांवर आला, बहुतेक करून Babel ला package.json मधून काढून टाकल्याने, जी माझी स्किनकेअर रूटीन देखील आहे. package.json मधून Babel हटवून, जे माझे स्किनकेअर रूटीन देखील आहे. आणि IBM ने बॉब नावाचा एक AI कोडिंग पार्टनर लॉन्च केला आहे जो तुम्हाला 'हाय, आय एम बॉब' असे अभिवादन करतो, उप-एजंट तयार करतो, मेनफ्रेम कोड आधुनिक करतो, आणि बॉबॅलिटिक्स नावाचे ॲनालिटिक्स उत्पादन शिप करतो, त्यामुळे कुठेतरी एक बँक खूप उत्साहित आहे आणि कोणीही परवाना वाचला नाही.

4:51 एका शुक्रवारसाठी हे खूप जास्त मार्जिन आहे; जर तुम्हाला हे ऐकण्याऐवजी वाचायला आवडत असेल, तर द डेली डिफ डॉट देववर तुम्हाला दररोज सकाळी तुमच्या इनबॉक्समध्ये विनामूल्य diff मिळते, लिंक खाली आहे. तर, आजचा निकाल: SHIP IT. कर्नेल म्हणतो हो, बझार्ड म्हणतो हो, गणित बदलले नाही, पण आपण गणित तपासण्याची पद्धत आताच बदलली. हा आजचा diff आहे. मी अ‍ॅक्स्रिसीकडून निको आहे.

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