GPT-5.6 Sol Ultra चक्र डबल कवर अनुमेयता का प्रमाण प्रस्तुत करता है [pdf]
एक OpenAI मॉडल, GPT‑5.6 Sol Ultra, ने कथित तौर पर graph theory में लंबे समय से चली आ रही Cycle Double Cover Conjecture का एक छोटा प्रमाण तैयार किया है, जिससे उत्साह और संदेह दोनों पैदा हुए हैं। टिप्पणीकार इस बात पर ध्यान केंद्रित करते हैं कि क्या प्रमाण स्वतंत्र रूप से सत्यापित या Lean जैसे प्रणालियों में औपचारिकीकृत किया गया है, orchestration, prompting, और trial-and-error कितना आवश्यक था, और परिणाम के चयन व सत्यापन में मानव गणितज्ञों की क्या भूमिका थी। व्यापक रूप से, थ्रेड यह जाँचता है कि यह गणित में AI के भविष्य के लिए क्या संकेत देता है—combinatorial समस्याओं में इसकी मौजूदा ताकत, नई theories बनाने में इसकी सीमाएँ, और ऐसे breakthroughs का मूल्यांकन तथा उन पर भरोसा कैसे किया जाना चाहिए।
प्रमाण की वैधता और सत्यापन
- कई लोग उत्साहित हैं, लेकिन सावधानी बरत रहे हैं: प्रमाण छोटा है, 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 लोगों को बदलने के बजाय उन्हें पूरक करेंगे।