एर्डोश समस्या वेबसाइट पर AI सहायता अब सामान्य होती जा रही है

 (mathstodon.xyz)
1 पॉइंट द्वारा GN⁺ 2025-11-25 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • एर्डोश समस्या #367 को हल करने की प्रक्रिया में AI टूल्स ने केंद्रीय भूमिका निभाई, और मानव गणितज्ञों के साथ सहयोग का एक उदाहरण सामने आया
  • Wouter van Doorn ने समस्या के दूसरे हिस्से के लिए मानव-निर्मित प्रतिवाद प्रस्तुत किया, जिसके बाद Gemini Deepthink ने संबंधित कॉन्ग्रुएंस का पूरा प्रमाण तैयार किया
  • Terence Tao ने Gemini के p-adic algebraic number theory आधारित प्रमाण को अधिक सरल रूप में बदलकर पोस्ट किया, और बाद में Lean formalization की संभावना का उल्लेख किया
  • Boris Alexeev ने Harmonic के Aristotle टूल का उपयोग करके Lean formalization पूरा किया, और AI के दुरुपयोग को रोकने के लिए अंतिम प्रतिज्ञप्ति को हाथ से सत्यापित किया
  • यह पूरी श्रृंखला दिखाती है कि गणितीय शोध में AI सहायता धीरे-धीरे मानक प्रक्रिया बनती जा रही है

एर्डोश समस्या #367 में AI सहयोग का मामला

  • 20 नवंबर को, Wouter van Doorn ने समस्या के दूसरे हिस्से के लिए एक प्रतिवाद प्रस्तुत किया, जो इस धारणा पर निर्भर था कि एक विशेष कॉन्ग्रुएंस सत्य है
    • उन्होंने अन्य प्रतिभागियों से उस कॉन्ग्रुएंस की वैधता की पुष्टि करने का अनुरोध किया
  • कुछ घंटों बाद Terence Tao ने यह समस्या Gemini Deepthink को दी, और लगभग 10 मिनट में कॉन्ग्रुएंस का पूरा प्रमाण तथा पूरे तर्क का सत्यापन प्राप्त कर लिया
    • Gemini के प्रमाण में p-adic algebraic number theory का उपयोग किया गया था, और Tao ने इसे अधिक सरल, प्राथमिक प्रमाण में बदलकर साइट पर पोस्ट किया
    • Tao ने उल्लेख किया कि इस प्रमाण का Lean में ‘vibe formalizing’ संभव हो सकता है

Lean formalization और सत्यापन

  • दो दिन बाद Boris Alexeev ने Harmonic के Aristotle टूल का उपयोग करके Lean formalization पूरा किया
    • AI के दुरुपयोग को रोकने के लिए अंतिम प्रतिज्ञप्ति को हाथ से सीधे formalize किया गया
    • पूरी प्रक्रिया में लगभग 2~3 घंटे लगे, और परिणाम ऑनलाइन सार्वजनिक किए गए
  • Tao ने बाद में AI का उपयोग करके साहित्य खोज भी की, लेकिन कुछ संबंधित शोध मिलने के बावजूद समस्या #367 से सीधे जुड़ा कुछ नहीं मिला

समुदाय की प्रतिक्रिया और चर्चा

  • कुछ उपयोगकर्ता Tao के अपडेट के माध्यम से शैक्षणिक गणित में AI के उपयोग की वर्तमान स्थिति को दिलचस्पी से देख रहे हैं
  • अन्य उपयोगकर्ताओं ने Lean के formalist approach पर आलोचनात्मक राय दी, यह कहते हुए कि गणितीय समझ compression है, जबकि Lean उसे low-level details में decompression कर देता है
    • संबंधित दस्तावेज़ “Against Lean: Why Proof Assistants Formalize the Wrong Thing” में दावा किया गया है कि Lean जैसे proof assistants गणित के सार को गलत तरीके से पकड़ते हैं
  • एक अन्य उपयोगकर्ता ने AI वार्तालापों की सटीकता की समस्या का उल्लेख करते हुए कहा कि सूक्ष्म समायोजन की ज़रूरत है, लेकिन इसका उपयोग आनंददायक है

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2025-11-25
Hacker News की राय

  • यह हैरान करने वाला अनुभव है कि गणित-केंद्रित ML पेपर को AI assistant को देकर उसका सरल explanation या pseudocode वापस पाया जा सकता है
    मेरे जैसे व्यक्ति के लिए, जिसने यूनिवर्सिटी में सीखी चीज़ों का 25 साल से ज़्यादा समय तक कभी इस्तेमाल नहीं किया, यह सचमुच बहुत मददगार है

    • यह जानना दिलचस्प है कि उसकी explanation सही है या नहीं, इसे कैसे verify किया जाता है। गणितीय definitions में बहुत सूक्ष्म बारीकियाँ होती हैं
    • मुझे लगता है कि यही वह क्षेत्र है जहाँ LLM learning में सबसे ज़्यादा चमकते हैं
      आप पेपर को Claude में डालकर उसका outline ले सकते हैं और फिर आगे सवाल पूछ सकते हैं
      biology जैसे उन क्षेत्रों में भी, जो मैंने bachelor या master के दौरान नहीं पढ़े थे, मैं ऐसे गहराई में जा सका जैसे किसी जानकार tutor से बात कर रहा हूँ
    • गणितीय notation बहुत context-dependent होती है, इसलिए अगर LLM से इसे Lisp जैसी low-context language में बदलने को कहें, तो संरचना जल्दी समझ में आ सकती है

  • उम्मीद है कि शोधकर्ता और कंपनियाँ वैज्ञानिक research में और अधिक productivity gains हासिल करेंगी
    एक imperfect assistant भी leverage को काफ़ी बढ़ा देता है

    • Tao ने जिस iOS formalization app beta का ज़िक्र किया था, वह मौजूद है → Aristotle
      कहा जाता है कि यह Robin Hood CEO द्वारा शुरू किया गया startup है

  • 'Vibe formalizing' मुझे 'vibe engineering' और 'vibe coding' का तार्किक विस्तार लगता है
    जब समस्या के हिस्से ठीक से फिट नहीं बैठते, तब informal तरीकों और mathematical rigor को जोड़ने वाला 'Move 37 as a Service' जैसा approach दिलचस्प लगता है

    • पहले polyhedral compilation पर एक पेपर पढ़ते समय मैं एक हिस्से पर अटक गया था, और ChatGPT ने reasoning process को काफ़ी अच्छे से आगे बढ़ाया
      बेशक उसमें कुछ गलतियाँ थीं, लेकिन वह मेरी उलझन को reflect करते हुए बातचीत कर सकता था, जिससे समझ और गहरी हुई
      AI खास तौर पर यूज़र के confusion points पहचानने में मज़बूत है

  • मैंने हंगेरियन गणितज्ञ Erdős के नाम के उच्चारण की बात सुनी
    हंगेरियन में spelling और pronunciation लगभग मेल खाते हैं, लेकिन नामों में कुछ exceptions होते हैं
    अंग्रेज़ी ढंग से यह लगभग “airdish” जैसा सुनाई देता है

    • Ő बस œ(oe) की ध्वनि है। हंगेरियन नामों में -y, कुलीन वंश को दर्शाने वाले -i suffix का अवशेष है
      उदाहरण: Görgey, Széchényi, Lánczos आदि
      हंगेरियन में नामों का क्रम जापानी की तरह surname-given name (big endian) होता है। उदाहरण: “Erdős Pál”, “Neumann János”
    • 1960 में गणित विभाग के notice board पर देखी एक मज़ेदार कविता याद है — मज़ाक यह था कि Erdos के पेपर ने 'वृत्त गोल होता है' प्रमेय का खंडन कर दिया
    • अलग-अलग भाषाओं में उच्चारण चिह्न का मतलब अलग होता है, इसलिए मुझे लगता है कि हंगेरियन चिह्नों को अंग्रेज़ी वाक्य में ज्यों-का-त्यों रखना अटपटा है
    • शुरुआत में “airdish” उच्चारण अजीब लगा, लेकिन जब मैंने 'os' ending को palatalize करके देखा, तो वह काफ़ी स्वाभाविक लगा
    • शायद मैं अमेरिकी नहीं हूँ, इसलिए लगता है कि ऐसे pronunciation मुद्दों की किसी को ज़्यादा परवाह नहीं है

  • यह दिलचस्प है कि comments में कुछ anti-Lean झुकाव वाले responses भी हैं

    • मैं गणितज्ञ नहीं हूँ, लेकिन यह जानने में दिलचस्पी है कि वह anti-Lean material कितना भरोसेमंद है
      क्या वह सिर्फ़ किसी दूसरे approach का प्रचार है, या दार्शनिक रूप से Lean के विरोध में है, यह जानना चाहता हूँ
    • Tao जैसे मशहूर लोगों पर eccentrics और conspiracy theorists का ध्यान जाना आम बात है

  • research mathematics में AI इस्तेमाल करने के नतीजे mixed रहे हैं
    कभी यह non-trivial arguments को autocomplete कर देता है, तो कुछ क्षेत्रों में पूरी तरह भटक जाता है
    अभी के लिए मुझे लगता है कि AI गणितज्ञों की जगह लेने के बजाय सिर्फ़ support tool के रूप में ही उपयोगी है

    • मेरा अनुभव भी कुछ ऐसा ही रहा। मैंने एक पेपर में इससे एक साधारण permutation calculation problem हल करने को कहा, और उसमें खुद हल करने से ज़्यादा समय लग गया
      coding में भी कभी-कभी यह मामूली bugs नहीं पकड़ पाया, लेकिन complex कामों में इससे काफ़ी मदद मिली
      आख़िरकार ये tools experts को replace करने से अभी बहुत दूर हैं, और ज़रूरत से ज़्यादा hype उल्टा भरोसा कम कर सकती है
      जैसे कहा जाता है, ‘अगर चाँद देने का वादा किया है, तो चाँद देना चाहिए’ — यानी realistic expectations महत्वपूर्ण हैं

  • यह विश्वास करना मुश्किल है कि मेरी ज़िंदगी में ‘Star Trek’ जैसी दुनिया आ जाएगी, जहाँ कहा जा सके, “Computer, इस गणित समस्या का proof draw करके दिखाओ”
    काश “Beam me up Scotty” भी संभव होता

    • लेकिन अगर हर बार उसमें मरने का खतरा हो, तो वह थोड़ा मुश्किल होगा

  • आज रात ड्राइव करते समय मैंने ChatGPT के साथ LLVM और GCC pipeline scheduler की बारीक संरचना पर बातचीत की
    इससे productivity बहुत बढ़ी, और जिस compiler-संबंधित notes पर मैं प्रयोग कर रहा था, उन्हें इसने अपने आप व्यवस्थित भी कर दिया
    पहले ऐसी चीज़ की कल्पना भी नहीं की जा सकती थी

    • मेरे अनुभव में LLM के कुछ details गलत होने की संभावना काफ़ी ज़्यादा होती है
      बेशक, अलग-अलग लोगों का अनुभव अलग हो सकता है

  • अगर AI का नाम Erdos रख दिया जाए, तो शायद हम सबका Erdos number 1 हो जाएगा

    • या फिर यह DR-DOS के sequel जैसा लगेगा
    • वास्तव में Erdos नाम का एक AI-integrated IDE प्रोडक्ट मौजूद है

  • यह प्रभावशाली है कि उन्होंने मौजूदा frontier tools का अच्छा इस्तेमाल करके एक collaborative mathematics research environment बनाया

    • अच्छी बात यह है कि गणित ऐसा क्षेत्र है जहाँ idolization या popularity contest किसी नतीजे की सच्चाई तय नहीं करते
      इसी वजह से मुझे लगता है कि गणित अब भी छद्मवैज्ञानिक प्रभाव से अपेक्षाकृत मुक्त दुर्लभ विधाओं में से एक है