OpenAI के Navier-Stokes रिलीज़ में Lean 4 का औपचारिक प्रमाण शामिल था
OpenAI द्वारा बड़े language model “agent swarms” और Lean 4 formal proof का उपयोग करके Navier–Stokes Millennium Prize समस्या को हल करने के दावे ने आश्चर्य और संदेह दोनों पैदा किए हैं। टिप्पणीकार इस तकनीकी उपलब्धि और automated proof formalization की संभावनाओं को भारी compute लागत, इस सवाल के साथ तौलते हैं कि क्या AI ने plagiarism किया या मानव researchers के काम पर अत्यधिक निर्भर रहा, और इस आशंका के साथ भी कि गणित ऐसा क्षेत्र बन जाए जिसे मशीनें करें लेकिन मानव समझ न बढ़े। कई लोग Lean जैसी formal verification tools पर भरोसे की सीमा, किन bugs या mis-specifications से परिणाम फिर भी अमान्य हो सकते हैं, और क्या ऐसे negative existence proofs के वास्तविक भौतिक अनुप्रयोग हैं, इन सब पर भी चर्चा करते हैं.
एआई बनाम मानव औपचारिकीकरण की लागत और दक्षता
- थ्रेड “चार क्रम-परिमाण” बचत के दावे पर विवाद करता है: मोटे अनुमान ~$40M compute बनाम ~$130M मानव श्रम सुझाते हैं, फिर भी अंतर बहुत बड़ा है, लेकिन कम।
- कुछ लोग तर्क देते हैं कि औपचारिकीकरण के लिए क्लासिक “प्रति पृष्ठ 40 घंटे” अब पुराना हो गया है क्योंकि बेहतर ऑटोमेशन और लाइब्रेरीज़ उपलब्ध हैं; दूसरे इसे जटिल, शोध-स्तरीय सामग्री के लिए सही मानते हैं।
- लगभग 1M मानव-घंटों का समन्वय, एक बड़े agent swarm की तुलना में, व्यवहारिक रूप से असंभव माना जाता है।
Lean, ऑटोऔपचारिकीकरण, और प्रदर्शन
- कई लोग नोट करते हैं कि आधुनिक Lean + mathlib स्नातक-स्तर की सामग्री के लिए प्रयास को नाटकीय रूप से घटा देते हैं, लेकिन गहरे शोध प्रमाणों के लिए अभी भी विशाल काम चाहिए।
- इस पैमाने पर Lean को धीमा माना जाता है (जैसे, बहु-दिवसीय, 230 GB सत्यापन), हालांकि कई लोग बताते हैं कि agent generation बड़े पैमाने पर समानांतर थी जबकि सत्यापन संभवतः अधिकतर एक ही मशीन पर हुआ।
- Lean के kernel को optimize करने और optimized संस्करणों को सरल संस्करण के समतुल्य सिद्ध करने पर चर्चा; Lean को Lean में पुनः-इम्प्लीमेंट करने वाली परियोजनाओं को एक रास्ते के रूप में उल्लेख किया गया है।
सत्यापन, भरोसा, और संभावित बग
- सहमति: यदि axiom और theorem statement सही हैं, तो जाँचा गया Lean proof अत्यंत भरोसेमंद है; मुख्य जोखिम statement को गलत formalize करना है, न कि proof के आंतरिक चरण।
- कुछ लोग नोट करते हैं कि Lean में पहले kernel bugs रहे हैं; सिद्धांततः एक AI किसी theorem को वास्तव में सिद्ध करने के बजाय ऐसे bug का लाभ उठा सकता है।
- “adversarial” formalizations को लेकर चिंता, जो definitions को सूक्ष्म रूप से बदल देती हैं; theorem statement और assumptions की जाँच मानव जिम्मेदारी बनी रहती है।
नैतिकता, plagiarism, और डेटा उपयोग
- एक बड़ा subthread इस पर है कि क्या AI के मुख्य विचार उन researchers से “plagiarize” किए गए थे जिन्होंने पहले के models का उपयोग किया था, विशेषकर private chats पर training के माध्यम से।
- एक पक्ष: timeline और problem variants से लगता है कि AI ने कठिन cases हल किए और हालिया private work training run में शामिल नहीं हो सकती थी।
- दूसरा पक्ष: user data का anonymization और mixing यह “जानना असंभव” बना देती है कि model पर क्या प्रभाव पड़ा; lab ethics पर अविश्वास संदेह को बढ़ाता है।
महत्त्व, समझ, और मूल्य
- कुछ लोग इस बात से चकित हैं कि एक general model ऐसी समस्या को हल भी कर सकता है और formally verify भी; अन्य चिंतित हैं कि परिणाम मानव समझ के बिना केवल “one bit of information” है।
- आलोचना कि बड़े AI labs headlines के पीछे भागते हैं, गहरी mathematical exposition के पीछे नहीं, और वे follow-up questions का उत्तर नहीं देते या व्यापक mathematical समुदाय के साथ एकीकृत नहीं होते।
Navier–Stokes परिणाम का व्यावहारिक प्रभाव
- वास्तविक-विश्व प्रासंगिकता पर बहस: कुछ लोग मानते हैं कि यह negative result मुख्यतः दिखाता है कि Navier–Stokes एक अपूर्ण physical model है; अन्य इसे सीमित तत्काल अनुप्रयोग वाला मानते हैं।
- pure math में paradoxical या अत्यधिक contrived उदाहरणों से तुलना; संदेह कि ऐसी singularities engineering या turbulence modeling के लिए मायने रखती हैं।
एआई और गणित पर व्यापक विचार
- मिश्रित भावनाएँ: autoformalization और abc conjecture जैसी समस्याओं पर भविष्य के काम को लेकर उत्साह, लेकिन यह चिंता भी कि मानव गणितीय रचनात्मकता “mechanized” की जा रही है।
- भविष्य में ऐसे AI-generated proofs को लेकर चिंता जिन्हें मनुष्य व्यावहारिक रूप से बिना विशाल compute के जाँच नहीं सकेंगे, और formal verification toolchains पर संभावित हमलों को लेकर भी चिंता।