GPT-5.6 Sol Ultra चक्र डबल कवर अनुमेयता का प्रमाण प्रस्तुत करता है [pdf]
प्रमाण की वैधता और सत्यापन
- कई लोग उत्साहित हैं, लेकिन सावधानी बरत रहे हैं: प्रमाण छोटा है, 1990-पूर्व ग्राफ़ सिद्धांत का उपयोग करता है, और संभावित लगता है, फिर भी इसमें सूक्ष्म त्रुटियाँ हो सकती हैं।
- कुछ का तर्क है कि इसकी घोषणा पेशेवर गणितज्ञों द्वारा या Lean औपचारिकीकरण / जर्नल peer review के बाद की जानी चाहिए थी।
- अन्य लोग नोट करते हैं कि OpenAI ने Lean formalization repo प्रकाशित किया है, लेकिन ग्राफ़ सिद्धांत की लाइब्रेरी अभी भी अपरिपक्व हैं, इसलिए यंत्रीकरण trivial नहीं है।
- कई टिप्पणीकारों ने अन्य LLMs और टूल्स से प्रमाण की जाँच कराने की कोशिश की; वे सामान्यतः कोई स्पष्ट त्रुटियाँ नहीं बताते, लेकिन जोर देते हैं कि यह विशेषज्ञ समीक्षा का विकल्प नहीं है।
- Reddit पर उठाई गई कम-से-कम एक तकनीकी चिंता को थ्रेड में notation issue माना गया है, न कि घातक दोष। कुल मिलाकर निष्कर्ष: आशाजनक, लेकिन अभी सार्वभौमिक रूप से स्वीकृत नहीं।
प्रॉम्प्टिंग, harness, और समय-सचेतता
- जारी किया गया प्रॉम्प्ट बहुत meta है: यह मॉडल को मान लेने के लिए कहता है कि एक प्रमाण मौजूद है, कम-से-कम 8 घंटे तक काम करे, अस्पष्ट status reports से बचे, और कई रणनीतियों का अन्वेषण करे।
- टिप्पणीकार इसे “motivation hacking” और pure autonomy के बजाय metaheuristic guidance के रूप में देखते हैं।
- agent harnesses में time-tracking (timestamps, OS
date, quota tools) बनाम मॉडलों की अंतर्निहित समय-बोध की कमी पर चर्चा है। - Sol Ultra को कई parallel sub-agents के साथ max reasoning के रूप में वर्णित किया गया है, जो Sol Pro के “best-of-N” दृष्टिकोण से अलग है।
कार्यप्रणाली की अस्पष्टता और survivorship bias
- कई टिप्पणीकार पूछते हैं कि कितनी समस्याएँ और prompt variants आज़माए गए, और इस सफलता से पहले कितनी failed runs हुईं।
- अटकल है कि OpenAI पहले की unit-distance result के बाद से कई समस्याओं पर काम कर रहा है; “failure rate” की अनुपस्थिति से क्षमता का आकलन करना कठिन है।
- चिंता है कि कंपनियाँ मार्केटिंग के लिए दुर्लभ सफलताओं को उजागर करेंगी जबकि null results को दबा देंगी।
गणित और proof assistants के लिए महत्व
- कुछ लोग इसे एक बड़ा मील का पत्थर मानते हैं: एक off-the-shelf model का एक प्रसिद्ध open problem को एक घंटे से कम में हल करना।
- अन्य लोग बताते हैं कि यह “clever trick” शैली का प्रमाण है, कोई लंबा, theory-building breakthrough नहीं; उनका तर्क है कि अगली कसौटी पर्याप्त नई theory का autonomous विकास है।
- AI-जनित प्रमाणों की बड़ी मात्रा से निपटने और मानव जाँच bottlenecks को कम करने के लिए Lean-शैली की formal verification की ओर बढ़ने का मजबूत समर्थन है।
व्यापक निहितार्थ और चिंताएँ
- इस पर बहस कि कौन-से कार्य सबसे अधिक automatable हैं: जिनमें correctness आसानी से जाँची जा सकती है (गणित, code, security, कुछ विज्ञान) वे विशेष रूप से vulnerable हो सकते हैं।
- शुद्ध गणित के मूल्य, क्या AI-जनित परिणाम “खाली” महसूस होते हैं, और क्या चीज़ें विशेष रूप से मानवीय हैं (conjecture बनाना, taste, explanation, जिम्मेदारी) पर दार्शनिक चर्चा।
- कुछ लोग नौकरियों, मानव मूल्य और AI hype को लेकर चिंता व्यक्त करते हैं; अन्य जवाब देते हैं कि मानव मूल्य आर्थिक उत्पादकता से जुड़ा नहीं है और tools लोगों को बदलने के बजाय उन्हें पूरक करेंगे।