GPT-5.6 ने उत्तल अनुकूलन में 30 साल के अंतर को पाटने के लिए एक प्रॉम्प्ट का उपयोग किया
एक AI model (GPT‑5.6 “Sol Pro”) ने convex optimization में 30 साल पुराने खुले परिणाम को साबित करने में मदद की है, एक दस-पृष्ठीय, expert-crafted prompt का उपयोग करके और बाद में Lean theorem prover में सत्यापित proof के साथ। टिप्पणीकार बहस करते हैं कि सिस्टम ने कितनी वास्तविक नवीनता दी बनाम एक अत्यंत शक्तिशाली automated assistant की तरह काम किया, और इसका गणितज्ञों और programmers की भविष्य की भूमिका, विशेषकर “low- और medium-hanging fruit” समस्याओं पर, क्या अर्थ है। यह चर्चा आगे बढ़कर इस प्रश्न तक जाती है कि large language models क्या केवल “stochastic parrots” हैं, वे कितनी जल्दी विभिन्न क्षेत्रों में मानव काम को विस्थापित कर सकते हैं, और यदि AI आगे बढ़ती रही तो किस तरह के सामाजिक और आर्थिक परिवर्तन आवश्यक होंगे।
परिणाम का दायरा और इसे कैसे प्राप्त किया गया
- टिप्पणीकारों का कहना है कि यह प्रमाण Lean-verified है, लेकिन अभी peer reviewed नहीं हुआ है, इसलिए इसकी स्थिति “आशाजनक लेकिन अस्थायी” है।
- मुख्य सूक्ष्मता यह है: GPT‑5.6 Sol Pro ने लगभग 10 पृष्ठों का, domain-expert prompt इस्तेमाल किया, जो मनुष्यों के एक वर्ष के पूर्व कार्य पर आधारित था (जिसमें पहले के LLM-assisted प्रयास भी शामिल थे)।
- इसे इस बात के मजबूत प्रमाण के रूप में देखा जा रहा है कि LLMs मौजूदा तकनीकों से पहुंच योग्य रास्ते होने पर gaps बंद कर सकते हैं, लेकिन “बस ‘solve this’ टाइप करो और चल दो” जैसी autonomy नहीं है।
गणित और शोध करियर पर प्रभाव
- कुछ लोगों का तर्क है कि गणित/TCS में low- और “medium-hanging fruit” increasingly AI को सौंप दिए जाएंगे, जिससे इंसान वास्तव में नई ideas और problem selection पर ध्यान देंगे।
- दूसरों को चिंता है कि इससे पारंपरिक training paths कमजोर होंगे, जहाँ junior लोग ऐसे problems पर हाथ आजमाकर सीखते हैं।
- कई लोग इसकी तुलना software से करते हैं: juniors और “recipe-followers” पहले displaced हो सकते हैं; deep domain और systems-level understanding अब भी महत्वपूर्ण है।
LLMs: intelligence, creativity, और “stochastic parrot” बहस
- उत्साही लोग कहते हैं कि 30-वर्षीय समस्याओं को हल करना और अन्य conjectures में योगदान देना “सिर्फ तोते” वाले दृष्टिकोण को खारिज करता है और वास्तविक reasoning दिखाता है।
- संशयवादी बनाए रखते हैं कि LLMs human-generated patterns पर आधारित sophisticated prediction engines हैं, न कि वास्तव में creative या समझ रखने वाले।
- कुछ सुझाव देते हैं कि अगर यह “intelligence” नहीं है, तो इस शब्द का अर्थ ही खत्म हो जाता है; अन्य उत्तर देते हैं कि statistical pattern-matching plus brute-force search इसे समझाने के लिए पर्याप्त हो सकता है।
Prompting, agents, और “harness engineering”
- कई टिप्पणियाँ जोर देती हैं कि अच्छे prompts और processes लिखना “magic prompting” से अधिक process/harness engineering के करीब है।
- multi-agent systems (Pro vs Ultra) पर चर्चा है, जहाँ models loops में plan, execute, test, और self-critique करते हैं।
- लोग नोट करते हैं कि LLMs अपने prompts और workflows खुद भी generate करने में मदद कर सकते हैं, जिससे समय के साथ manual prompt craft की जरूरत कम हो सकती है।
Formal verification और proof infrastructure
- Lean को आज Mizar जैसे पुराने systems के समकक्ष के रूप में रेखांकित किया गया है; machine-checked proofs को AI-generated math पर भरोसा करने के लिए महत्वपूर्ण माना जा रहा है।
- कुछ लोग चाहते हैं कि LLMs बहुत लंबे या opaque proofs (जैसे बड़े classification theorems) को पूर्ण formalization के माध्यम से संभालें।
व्यापक सामाजिक और आर्थिक चिंताएँ
- प्रतिक्रियाएँ उत्साह (“intelligence is cheap, हम science को तेज कर सकते हैं”) से लेकर नौकरी जाने, stratification, और “technofeudal” भविष्य की चिंता तक फैली हुई हैं।
- कई लोगों का तर्क है कि असली समस्या political economy है: लाभ कैसे वितरित होते हैं, न कि गणित स्वयं।