20 Codex खातों को समानांतर चलाकर 20 Erdős समस्याओं का समाधान
Lean 4 और बड़े पैमाने के cloud compute से जुड़े AI agents अब दर्जनों कठिन Erdős समस्याओं के machine-checked proofs बना रहे हैं, जिससे गणितीय शोध के भविष्य को लेकर उत्साह और बेचैनी दोनों बढ़ रही हैं। टिप्पणीकार तकनीकी सेटअप, funding, और open-sourcing योजनाओं पर सवाल उठाते हैं, और नोट करते हैं कि formal proofs प्रभावशाली होने के बावजूद उन्हें human-readable, insightful arguments में बदलना अभी भी एक अलग चुनौती है। यह चर्चा “बेकार” शुद्ध गणित के मूल्य, proof search के स्वचालित होने पर human mathematicians की भविष्य की भूमिका, और AI-driven theorem proving के real-world impact तथा आर्थिक बदलावों से जुड़ने की संभावनाओं तक फैल जाती है.
इन्फ्रास्ट्रक्चर, कंप्यूट, और मॉडल एक्सेस
- प्रोजेक्ट कई Codex खातों का उपयोग OAuth टोकनों और एक कस्टम ब्रोकर के जरिए करता है, जो API कॉल्स को लोड-बैलेंस करता है; “running GPT locally” वाली बात शब्दावली की समस्या थी, मॉडल को self-host नहीं किया गया था।
- स्थानीय कंप्यूट एक multi‑vCPU सर्वर है; टिप्पणीकारों का कहना है कि ऐसा हार्डवेयर hobbyists के लिए किफायती है।
- AI एजेंट्स के पास bash टूल्स और VMs पर पहले से इंस्टॉल गणितीय पैकेजों की पहुँच है।
- उल्लेखित मॉडल: GPT‑5.6 (generation के लिए), Fable (Lean proof checking/summaries के लिए), Gemini embeddings।
Harness, Open Sourcing, और Contributions
- प्रश्न “agentic harness” पर केंद्रित हैं: loops कैसे orchestrate होते हैं, कौन-से मॉडल “drive” करते हैं, और प्रगति कैसे मापी जाती है; विवरण उच्च-स्तरीय ही हैं।
- एक अन्य प्रतिभागी एक समान स्वतंत्र system का वर्णन करता है: intranet पर sovereign inference, Lean/Sage के लिए sandboxed workers, open-weight models, और आगे fine-tuning की योजनाएँ।
- system को open-source करने और contributions सक्षम करने में रुचि है; author का कहना है कि project एक जल्दी, self-contained experiment के रूप में शुरू हुआ था और बाद में खोला जा सकता है।
Validity, Rigor, और Writeups
- Lean 4 proofs machine-checked हैं; Fable एक तरह के referee की भूमिका निभाता है।
- आलोचना: proof summaries तकनीकी रूप से घनी हैं और human readers के लिए ठीक से अनुकूलित नहीं; formal proofs को स्पष्ट, सौंदर्यपूर्ण explanations में बदलना एक अलग, अभी-अपूर्ण कदम है।
- author इसे स्वीकार करता है और writeups सुधारने की योजना बनाता है।
- कुछ प्रस्तुत Erdős solutions को अस्थायी रूप से वापस लिया गया, गलत होने के कारण नहीं बल्कि भ्रमित framing या आंशिक होने के कारण; काम जारी है।
- सुझाव: context बदलते समय subtle unsoundness से बचने के लिए Lean के “comparator” टूल को integrate किया जाए।
शुद्ध गणित और AI Theorem Proving का मूल्य
- इस पर बहस कि क्या “बेकार” शुद्ध गणित अपने आप में बंद और सामाजिक रूप से महत्वहीन है, या फिर उसका अप्रत्याशित अनुप्रयोगों का इतिहास है (जैसे cryptography) और अंतर्निहित सौंदर्यात्मक मूल्य।
- कुछ लोग Erdős समस्याएँ हल करने को एक benchmark और तकनीकों के स्रोत के रूप में देखते हैं, न कि सीधे अनुप्रयोगों के रूप में; वास्तविक दुनिया का प्रभाव frontier या Millennium समस्याओं से अधिक आ सकता है।
- अन्य लोग तर्क करते हैं कि, भले ही यह purely recreational हो, यह किसी भी intellectual hobby जितना ही वैध है।
गणितज्ञों और समाज पर प्रभाव
- चिंता है कि AI proof systems math का मज़ा “छीन” सकते हैं और mathematicians की नौकरियों को खतरा पहुँचा सकते हैं; प्रत्युत्तर में इसे पुराने automation fears (जैसे looms, calculators) से जोड़ा जाता है।
- कई लोगों का कहना है कि mathematicians, AI-generated proofs को समझने, conjecture करने और जाँचने की दिशा में शिफ्ट होंगे; उन्नत proofs पहले से ही अक्सर एक अकेले मानव की क्षमता से बाहर हैं।
- व्यापक चर्चा काम से जीविका को अलग करने, संभावित UBI, और AI firms पर कर लगाने पर है; policy changes कितनी urgent हैं, इस पर असहमति है।
गणित में AI की वर्तमान स्थिति और भविष्य
- बहुत से लोग इस बात से चकित हैं कि LLMs अब nontrivial Erdős problems हल कर सकते हैं; धारणा “क्या LLMs math कर सकते हैं?” से बदलकर “हम इसे कितनी दूर तक ले जा सकते हैं?” की ओर जा रही है।
- भविष्य की अपेक्षा: मौजूदा गणित का बड़े पैमाने पर autoformalization, बड़े पैमाने पर automated conjecture generation और evaluation, और संभवतः distributed, BOINC‑style efforts for mathematical exploration.