एर्डोश समस्या #728, AI ने लगभग स्वायत्त रूप से हल की

 (mathstodon.xyz)
2 पॉइंट द्वारा GN⁺ 2026-01-10 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • एर्डोश समस्या #728 को हाल ही में AI टूल्स की मदद से लगभग स्वायत्त रूप से हल किया गया, जिससे गणितीय शोध के ऑटोमेशन में एक नया मील का पत्थर स्थापित हुआ
  • यह समस्या मूल रूप से Erdős, Graham, Ruzsa, Strauss द्वारा 1975 में उठाया गया binomial coefficient के prime factorization से जुड़ा प्रश्न था, लेकिन अस्पष्ट शर्तों के कारण इसे लंबे समय तक स्पष्ट रूप से नहीं सुलझाया जा सका
  • ChatGPT ने समायोजित constraints के तहत एक proof तैयार किया, और Aristotle ने उसे Lean formal proof में रूपांतरित करते हुए त्रुटियों को स्वतः सुधारा
  • इसके बाद कई प्रतिभागियों ने ChatGPT की मदद से इसे natural language में फिर से लिखा, और literature connections तथा narrative structure को मजबूत करने वाले संस्करणों को बार-बार बेहतर बनाया
  • Terence Tao ने आकलन किया कि यह प्रक्रिया AI की तेज proof drafting और revision क्षमता दिखाती है, जो शोध-पत्र लिखने के तरीके को ही बदल सकती है

AI ने हल की एर्डोश समस्या #728

  • हाल में AI टूल्स के उपयोग से एर्डोश समस्या के समाधान में नई प्रगति देखी गई, और समस्या #728 को लगभग स्वायत्त रूप से AI द्वारा हल किया गया
    • शुरुआती प्रयासों के बाद feedback को शामिल कर संशोधित संस्करण में सफलता मिली
    • परिणाम मौजूदा literature में ठीक उसी रूप में पुनरुत्पादित नहीं हुआ, हालांकि मिलते-जुलते तरीकों से समान परिणाम मौजूद थे
  • यह मामला दिखाता है कि पिछले कुछ महीनों में गणितीय समस्याएँ हल करने में AI की क्षमता वास्तव में बेहतर हुई है
    • पहले भी AI द्वारा एर्डोश समस्याएँ हल करने के दावे हुए थे, लेकिन उनमें से अधिकांश बाद में existing literature में पहले से मौजूद समाधान निकले
  • इस बार की समस्या में मूल एर्डोश विवरण गलत रूप में प्रस्तुत किया गया था, और हाल ही में ही उसे इच्छित रूप में पुनर्निर्मित किया गया
    • इसी वजह से मौजूदा literature में संबंधित शोध कम होने की व्याख्या मिलती है

समस्या का इतिहास और शुरुआती दृष्टिकोण

  • 1975 में Erdős, Graham, Ruzsa, Strauss ने binomial coefficient (2n choose n) के prime factorization का अध्ययन करते हुए कई संबंधित समस्याएँ रखीं
    • उनमें से एक यह पूछती थी कि क्या ऐसे अनंत a, b, n मौजूद हैं जो a!b! | n!(a+b−n)! शर्त और a+b > n + C log n को संतुष्ट करते हों
    • लेकिन C का परिमाण (छोटा या बड़ा) जैसी कई बातें अस्पष्ट रूप से लिखी गई थीं
  • कुछ महीने पहले AlphaProof टीम ने समस्या का एक सरल समाधान पाया, लेकिन वह समस्या की मूल भावना से मेल नहीं खाता था, इसलिए a,b ≤ (1−ε)n constraint जोड़ा गया
    • इसके बाद AI-सहायित literature search में भी संबंधित शोध लगभग नहीं मिला

ChatGPT और Aristotle का सहयोग

  • 4 जनवरी को ChatGPT ने समायोजित constraints के तहत छोटे C के मामले के लिए एक proof तैयार किया
    • इस proof को Aristotle ने Lean formal proof के रूप में औपचारिक बनाया
    • बाद में मूल लेख को दोबारा देखने पर पुष्टि हुई कि original paper पहले से ही छोटे C वाले मामले को कवर करता था
  • एक अन्य प्रतिभागी ने Lean proof को ChatGPT से natural language में बदला, और आगे की बातचीत के जरिए बेहतर संस्करण तैयार किया
    • इस संस्करण ने proof की कुछ कमियाँ भरीं, लेकिन उसमें अब भी AI-विशिष्ट अटपटी शैली और literature citations की कमी थी
    • फिर भी यह मुख्य विचार समझने लायक पर्याप्त पठनीय स्तर तक पहुँच गया

बड़े पैमाने पर पुनर्लेखन और बेहतर परिणाम

  • अतिरिक्त prompts के जरिए ChatGPT ने बड़े C के मामले तक विस्तारित proof तैयार किया
    • कुछ त्रुटियाँ थीं, लेकिन Aristotle ने उन्हें स्वतः ठीक कर Lean-verified proof पूरा किया
  • तीसरे प्रतिभागी ने Lean proof को संक्षिप्त किया, फिर एक अन्य प्रतिभागी ने ChatGPT के साथ लंबी बातचीत के माध्यम से
    • इसे literature connections और narrative structure को मजबूत करने वाले अधिक परिपक्व paper रूप में फिर से लिखा
    • परिणाम को AI-जनित होने का एहसास कम, और research paper स्तर के करीब गुणवत्ता वाला माना गया
    • Tao ने कहा कि उन्होंने इस text की एर्डोश समस्या फोरम में समीक्षा की

AI कैसे बदल रहा है research paper लिखने का तरीका

  • Tao का मानना है कि अंतिम paper में अब भी मुख्य हिस्से इंसानों को ही लिखने होंगे, लेकिन
    • AI और Lean का संयोजन proof लिखने और संशोधित करने की गति को नाटकीय रूप से बढ़ाता है
  • पहले किसी paper को पढ़ने में सहज बनाने में बहुत समय लगता था,
    • और reviewers के feedback के बाद revisions अक्सर local changes तक सीमित रह जाते थे
  • लेकिन अब AI की text generation और revision क्षमता तथा formal proof tools की verification क्षमता के जुड़ने से
    • विभिन्न स्तर की precision और व्याख्या के साथ papers के नए versions तेजी से तैयार किए जा सकते हैं
  • एक “official paper” के अलावा, AI द्वारा बनाए गए अनेक supplementary versions भी मौजूद हो सकते हैं
    • जो अलग-अलग दृष्टिकोण और अतिरिक्त मूल्य प्रदान कर सकते हैं

कम्युनिटी की प्रतिक्रिया

  • कुछ उपयोगकर्ताओं ने AI-जनित दस्तावेज़ों के अतिरिक्त मूल्य को “किसी चीज़ को अलग कोण से देखने की क्षमता” बताया
  • अन्य गणितज्ञों ने AI परिणामों की मौलिकता मापने और existing literature से समानता का आकलन करने की जरूरत उठाई
    • उदाहरण के लिए, Lean formal proof की लंबाई की तुलना के जरिए मात्रात्मक समानता मापने का सुझाव दिया गया
  • एक अन्य टिप्पणी में कहा गया कि AI code refactoring की तरह papers को global स्तर पर rewrite कर सकता है
    • इसलिए शोधकर्ताओं को उच्च-स्तरीय document structure design पर अधिक ध्यान देना चाहिए
  • कुछ लोगों ने AI द्वारा गणितज्ञों की भूमिका बदल देने की संभावना पर संदेह जताया,
    • जबकि अन्य ने इसे सहयोग और सोच के विस्तार का नया अवसर माना

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

1 टिप्पणियां

 
GN⁺ 2026-01-10
Hacker News की राय

  • मैं Harmonic में काम करता हूँ, और हम जो Aristotle बना रहे हैं उसके बारे में कुछ गलतफ़हमियाँ दूर करना चाहता हूँ
    Aristotle नवीनतम AI तकनीकों का सक्रिय रूप से उपयोग करता है, और इसमें language modeling भी शामिल है
    अगर किसी अनौपचारिक अंग्रेज़ी proof को इनपुट दिया जाए, तो यदि वह proof सही है, उसके Lean में अनुवाद होने की संभावना काफ़ी अधिक होती है। यानी यह इस बात का मज़बूत संकेत है कि अंग्रेज़ी proof ठोस है
    एक बार उसे Lean में formalize कर दिया जाए, तो उस proof के सही होने पर कोई संदेह नहीं रहता। यही हमारा मुख्य approach है — AI-आधारित exploration से उत्तर ढूँढो, और फिर उसकी complexity चाहे जो भी हो, नतीजे की correctness की गारंटी पाओ

    • मुझे जिज्ञासा है कि AI ने Lean में जो proof अनुवाद किया है, वह वास्तव में समस्या का सही formalization है, इसे कैसे verify किया जाता है। दूसरे क्षेत्रों में generative AI काफ़ी भरोसेमंद लगने वाले झूठ बना लेता है, इसलिए जानना चाहता हूँ कि यहाँ भी ऐसा हो सकता है या नहीं
    • जानना चाहता हूँ कि क्या इस तरह की तकनीक को software verification में लागू करने की कोशिश हो रही है
      Rust memory safety की गारंटी के लिए fixed rules के एक सेट का उपयोग करता है, लेकिन ये rules काफ़ी सरल और सीमित हैं। अगर Aristotle जैसे सिस्टम को compiler में integrate किया जा सके, ताकि code की correctness proof संभव होने पर वह अपने-आप pass हो जाए, तो वह सचमुच कमाल होगा
    • हर नए LLM के साथ समझना मुश्किल हो जाता है कि यह सचमुच प्रगति है या बस benchmark hacking, लेकिन मुझे लगता है कि math proofs का formalization असली प्रगति दिखाने वाला अच्छा संकेतक है
      Harmonic को इंसानों द्वारा लिखी गई अधिकांश mathematics को formalize करने में कितना समय लगेगा, यह जानना दिलचस्प होगा। प्रतिद्वंद्वी Christian Szegedy कह रहे थे कि यह इस साल के भीतर संभव हो सकता है
    • आपने कहा कि अगर अंग्रेज़ी proof सही हो तो उसके Lean में अनुवाद होने की संभावना अधिक है; मैं जानना चाहता हूँ कि क्या यह गणित के विषय-विशेष की कठिनाई के अनुसार बदलता है। मेरी समझ से अब भी कई research क्षेत्रों को इंसान भी formalize करना मुश्किल पाते हैं
    • “यदि proposition सही ढंग से formalize की गई हो” — यह शर्त काफ़ी बड़ी मान्यता जैसी लगती है। हाल की Navier-Stokes घटना में भी देखा गया कि formalization अपने-आप में आसान नहीं है

  • Terence Tao की व्याख्या पढ़ने पर लगता है कि इंसान दो AI tools के बीच नतीजों का आदान-प्रदान कर रहा था, और AI इंसान द्वारा पाए गए खाली स्थानों को भरने का काम कर रही थी
    इसे पूरी तरह autonomous समाधान कहने की बजाय, यह मानव और AI के सहयोग के ज़्यादा क़रीब लगता है। यानी expert नेतृत्व कर रहा था और AI सहायक की भूमिका में थी

    • हाँ, मेरी समझ भी यही है कि Aristotle, ChatGPT, और एक बेहद कुशल user के interaction के ज़रिए यह आगे बढ़ा
    • मैंने सुना था कि Tao या community ने सीधे gaps नहीं ढूँढे, बल्कि automatic proof verifier का उपयोग किया। उल्टा यह AI 90% / human 10% जैसा दिखता है
    • Reddit पर लेखक की विस्तृत व्याख्या है — reddit पोस्ट
    • मानव expertise और effort के स्तर को समझना हो, तो Erdős problem forum की thread पढ़ने की सलाह दूँगा
    • वैसे, यह साइट mathematician Thomas Bloom ने बनाई थी, और ChatGPT ने technical setup में मदद की (FAQ के अनुसार)

  • मौजूदा proofs को फिर से बनाना या नए तरीक़े से जोड़ना इंसानों के लिए उबाऊ या जटिल प्रक्रिया हो सकता है, लेकिन AI इसे अतिमानवीय गति से कर सकती है
    यह approach AGI से पहले के चरण में भी जबरदस्त संभावनाएँ खोल सकती है। लगता है ऐसा समय आएगा जब mathematicians AI को tool की तरह इस्तेमाल करके Millennium Problems जैसी कठिन चुनौतियों पर काम करेंगे

    • मुझे नहीं लगता कि मौजूदा proofs को पुनर्गठित करने और पूरी तरह नई mathematics बनाने के बीच कोई साफ़ सीमा है
    • क्योंकि mathematics तार्किक है, मुझे लगता है कि इस तरह की खोज के लिए पहले से कई algorithms होंगे; यह सिर्फ़ एक साधारण search problem नहीं लगता
    • मौजूदा proofs को पुनर्गठित करने वाली बात से मैं भी सहमत हूँ। LLM के आउटपुट को verify करना अब भी उबाऊ काम है, लेकिन इंसान के ख़ुद करने से बेहतर है
      LLM की असली value उन विषयों में नए दृष्टिकोण देने में है जिन्हें भाषा में व्यक्त किया जा सकता है
    • मैं इस घटना को “scientific refactoring” कहता हूँ। उदाहरण के लिए, किसी constant को बदलकर तर्क को फिर से विकसित करने जैसे प्रयोग AI अपने-आप कर सकेगी
    • अगर जटिल theorems को साबित कर सकने वाली AI AGI नहीं है, तो फिर AGI आखिर है क्या, यह सवाल उठता है

  • वास्तव में समस्या हल करने वाले व्यक्ति की व्याख्या पोस्ट में यह बात प्रभावशाली लगी कि बड़े pipeline के बिना, सिर्फ़ कुछ prompts से नतीजा मिला
    हाल के models बहुत अधिक computation resources इस्तेमाल करते हैं, इसलिए यह तो उल्टा न्यूनतम स्तर की उपलब्धि जैसा लगता है

  • Terence Tao ने “AI contributions to Erdős problems” नाम का एक wiki page बनाया है
    GitHub page और Mathstodon पोस्ट के अनुसार, इस बार का नतीजा (problem 728) उस page की पहली ‘हरी प्रविष्टि’ है, यानी AI द्वारा वास्तव में हल किया गया पहला मामला

    • दिलचस्प बात यह है कि wiki के section 6 में मौजूद अधिकांश AI-formalized proofs पिछले कुछ महीनों के भीतर पूरे हुए हैं। आगे क्या आता है, यह देखने लायक होगा

  • क्या physics या mathematics जैसे जटिल क्षेत्रों के experts भी AI से बातचीत करके मदद लेते हैं, यह जानने की जिज्ञासा है

    • मैं pure mathematics में postdoc रह चुका हूँ और अब data scientist के रूप में काम कर रहा हूँ। literature review या अपरिचित mathematics को जल्दी दोहराने में AI बहुत मददगार है
      क्षेत्रों के हिसाब से देखें, तो उपयोगिता programming > applied ML > statistics/applied mathematics > pure mathematics के क्रम में घटती है
    • मैं physics का specialist नहीं हूँ, लेकिन AI की वजह से ज़रूरी formulas या papers ढूँढने में लगने वाला समय काफ़ी कम हो गया है। हालाँकि, नतीजों को हमेशा verify करना पड़ता है
    • deep learning models और नई attention architectures पर शोध करने के नज़रिए से, ChatGPT papers खोजने और संबंधित ideas की तलाश में बेहद उपयोगी है
    • गणित को शौक़ से करने वाले के रूप में, LLM मेरे प्रयासों पर feedback देता है या मुझे मौजूदा समाधानों तक ले जाता है। खेल के रूप में mathematics के लिए यह काफ़ी आनंददायक tool है
    • मैं algebraic geometry पर शोध करता हूँ, और literature search के अलावा अभी तक ज़्यादा मदद नहीं मिली। models के बीच फ़र्क़ भी काफ़ी है

  • आप अभी Aristotle को सीधे इस्तेमाल कर सकते हैं — https://aristotle.harmonic.fun/

    • यह भी जानना दिलचस्प होगा कि क्या AI को DeepMind के formal-conjectures dataset पर test किया जाता है
    • docs में “uvx aristotlelib@latest aristotle” लिखा है, लेकिन वास्तव में “uvx --from aristotlelib@latest aristotle” सही है
      और Stanford personal page का link भी ग़लत है (www हटाना होगा)
    • यह इतना दिलचस्प है कि इस पर अलग HN thread बननी चाहिए। अगर मैं CEO होता, तो ख़ुद एक intro post डालता (संदर्भ लिंक)

  • यह नतीजा integers पर एक theorem से जुड़ा है, जो Mathlib infrastructure अच्छी तरह support करता है
    इस्तेमाल की गई definitions भी जटिल नहीं हैं, इसलिए इस तरह के proofs की सफलता की संभावना अधिक होती है। फिर भी, यह सचमुच हैरान करने वाली उपलब्धि है

  • यह LLM से आगे की specialized AI approach की संभावना दिखाने वाला मामला है
    Aristotle का paper arXiv:2510.01346 पर है
    सिर्फ़ Transformer architecture इस्तेमाल करने से सब कुछ LLM नहीं बन जाता — अगर उसे language data पर train नहीं किया गया, तो उसे LLM नहीं कहा जा सकता

    • लगता है काफ़ी लोग “LLM” और “GenAI” को एक ही अर्थ में इस्तेमाल करते हैं, इसलिए भ्रम पैदा होता है
    • आपने “LLM नहीं वाला approach” कहा, लेकिन क्या वास्तव में ChatGPT इस्तेमाल नहीं हुआ था?
    • हाँ, वास्तव में ChatGPT इस्तेमाल हुआ था
    • paper देखने पर लगता है कि तीनों चरणों में बड़े Transformer-आधारित LLM शामिल थे
      1. Monte Carlo Graph Search में policy/value function की भूमिका
      2. अनौपचारिक reasoning system में chain of thought का उपयोग
      3. AlphaGeometry भी neuro-symbolic language model का उपयोग करता है
        यानी हर चरण LLM-आधारित है

  • लगता है 2026 में AI mathematics के unsolved problems पर बढ़ते हुए स्तर पर काम करेगी
    यह मामला भी पूरी तरह autonomous नहीं था, लेकिन human feedback के बाद AI ने लगभग ख़ुद ही समाधान तक पहुँचना शुरू कर दिया
    अब “LLM सिर्फ़ stochastic parrots हैं” वाली बहस ख़त्म हो जानी चाहिए। आगे असली चर्चा का केंद्र यह होगा कि इसे व्यावहारिक रूप से कैसे इस्तेमाल किया जाए

    • 2026 में mathematics के क्षेत्र में विस्फोटक प्रगति हो सकती है
    • संभव है कि यह नतीजा training data में मौजूद मिलते-जुलते proofs का remix हो, लेकिन remix करने की वही क्षमता अपने-आप में बहुत शक्तिशाली है
    • अब भी स्वतंत्र verification की ज़रूरत है। सिर्फ़ कंपनी के दावों पर भरोसा करना मुश्किल है