Knuth की ‘Claude Cycles’ समस्या में मानव·AI·प्रूफ असिस्टेंट सहयोग की प्रगति

 (twitter.com/BoWang87)
2 पॉइंट द्वारा GN⁺ 2026-03-30 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Donald Knuth द्वारा प्रस्तुत Hamiltonian decomposition problem के अनसुलझे हिस्से को मानव और AI के सहयोग से आगे बढ़ाते हुए सुलझाया गया
  • Claude ने विषम m के लिए समाधान खोजा, जिसे “Claude’s Cycles” नाम दिया गया; इसके बाद 11,502 cycles में से 996 को सभी विषम m के लिए सामान्यीकृत किया गया
  • Dr. Ho Boon Suan ने GPT-5.4 Pro के साथ सम m≥8 के लिए 14-पृष्ठ का प्रमाण तैयार किया और m=2000 तक computational verification किया
  • Dr. Keston Aquino-Michaels ने GPT और Claude के multi-agent workflow के जरिए विषम और सम, दोनों m के लिए एक सरल construction खोजी
  • Dr. Kim Morrison ने Lean proof assistant से Knuth के समाधान का formal verification किया, जिससे मानव·AI·प्रूफ टूल सहयोगी ecosystem पूरा हुआ

Claude’s Cycles समस्या-समाधान में विस्तारित सहयोग

  • Donald Knuth द्वारा प्रस्तुत Hamiltonian decomposition problem के अनसुलझे हिस्से को मानव और AI के सहयोग से सुलझाया गया
    • शुरुआत में Claude ने लगभग एक घंटे की खोज के बाद विषम m के लिए समाधान निकाला, और Knuth ने इसे “Claude’s Cycles” नाम दिया
  • बाद में अपडेट किए गए शोधपत्र में, base case m=3 के लिए ठीक 11,502 Hamiltonian cycles मौजूद पाए गए, जिनमें से 996 को सभी विषम m तक सामान्यीकृत किया गया
    • Knuth ने इनमें से 760 वैध “Claude-type” decompositions की पुष्टि की
  • सम m के मामले में Claude समाधान पूरा नहीं कर पाया, लेकिन Dr. Ho Boon Suan ने GPT-5.4 Pro का उपयोग कर m≥8 के लिए 14-पृष्ठीय प्रमाण लिखा और m=2000 तक computational verification किया
  • इसके बाद Dr. Keston Aquino-Michaels ने GPT और Claude को साथ इस्तेमाल करने वाले multi-agent workflow के माध्यम से विषम और सम, दोनों m पर लागू होने वाली एक सरल construction खोजी
  • Dr. Kim Morrison ने Knuth के विषम-m समाधान को Lean proof assistant में formalize करके verify किया
    • नतीजतन, मनुष्य, कई AI सिस्टम, और formal proof tools के समानांतर सहयोग से एक पूर्ण गणितीय collaborative ecosystem बना
  • यह पूरी प्रक्रिया एक AI द्वारा एकल समस्या-समाधान से शुरू होकर multi-AI·मानव·प्रूफ असिस्टेंट सहयोग तक विस्तारित हुए गणितीय शोध के एक नए मॉडल को दिखाती है
  • नवीनतम शोधपत्र Stanford CS Faculty वेबसाइट(www-cs-faculty.stanford.edu/~knuth/papers/) पर उपलब्ध है

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

1 टिप्पणियां

 
GN⁺ 2026-03-30
Hacker News टिप्पणियाँ

  • मैं हमेशा कहता रहा हूँ कि AI McDonald's चलाने से पहले Fields Medal जीत लेगा
    गणित इंसानों को वैसा कठिन लगता है जैसे हथौड़े से स्क्रू घुमाना
    LLM उथली लेकिन व्यापक खोज में मज़बूत हैं, इसलिए वे कई नए गणितीय पैटर्न खोज रहे हैं
    मेरा अनुमान है कि आगे चलकर LLM की जगह Lean syntax tree-आधारित AlphaGo-शैली reinforcement learning ले लेगा
    अगर गणितज्ञों के इस्तेमाल की जाने वाली ‘10 tricks’ को latent vector में कोड किया जा सके, तो खेल खत्म है

    • आखिरकार tricks सिर्फ़ तार्किक अभिव्यक्तियों के patterns ही तो हैं
      हम ज्यामितीय analogy के ज़रिए वैसे सोचते हैं जैसे algebraic geometry को number theory की समस्याओं पर लागू करते हैं
      Lean tree पर प्रशिक्षित AI इंसानों से भी अधिक व्यापक intuition system रख सकता है
      जैसे chess में StockFish ने दिखाया, इस तरह के दृष्टिकोण का mechanistic interpretability के नज़रिए से अध्ययन करना सार्थक होगा
    • मैं एक पेशेवर गणितज्ञ हूँ, और अच्छी proof में समस्या को व्यक्त करने का तरीका सबसे अहम होता है
      tricks निकालकर इस्तेमाल करना तो LLM अभी भी काफ़ी अच्छी तरह कर लेते हैं
      लेकिन समस्या को सही रूप में व्यक्त करना अब भी इंसानों का काम है, और यह स्वाभाविक है
    • अगर सिस्टम को खुद नई tricks खोजने के लिए प्रशिक्षित किया जाए, तो वह सचमुच हैरान करने वाली बात होगी
    • “AI McDonald's चलाने से पहले Fields Medal जीत लेगा” — यह बात मुझे बहुत पसंद आई
      मैं इसमें अपना version जोड़ना चाहूँगा: “आख़िर में automation का शिकार होने वाली नौकरी QA होगी”
      तकनीक की इस लहर ने हमें knowledge work की प्रकृति पर फिर से सोचने पर मजबूर किया है, और इसकी वजह से हम और अधिक पैने होंगे
    • मैं भी Lean tree-आधारित reinforcement learning approach को खुद prototype के रूप में लागू करने की धीमी कोशिश कर रहा हूँ

  • जब से मैंने 4chan की कहावत “trolls trolling trolls” सुनी, तब से मैं इंटरनेट पर होने वाली बातचीत को हमेशा शक की नज़र से देखने लगा हूँ
    मुझे पहले ही लग रहा था कि Reddit ‘dead internet’ बन चुका है, और इस thread को देखकर तो अब यह भी समझ नहीं आता कि कौन bot है और कौन इंसान

    • मुझे लगता है कि यह insight सचमुच बहुत महत्वपूर्ण है
      इसलिए मैंने RememberBuddy नाम की एक service बनाई — रोज़मर्रा की insights को भूलने से बचाकर रखने की जगह

  • लगता है AI गणित का विकास वही रास्ता पकड़ेगा जिसकी 90 के दशक में Greg Egan ने अपने उपन्यासों में कल्पना की थी
    गणित का सार नहीं बदलेगा, लेकिन हम उसे ‘क्यों’ करते हैं यह बदल जाएगा
    Egan की 『Diaspora』 में गणितीय खोज को नमक की खदान में रत्न निकालने जैसी क्रिया की तरह वर्णित किया गया है
    कुछ लोग उन रत्नों की शुद्ध सुंदरता का पीछा करते हैं, जबकि कुछ उनके व्यावहारिक मूल्य का
    अभी Terence Tao द्वारा स्थापित संस्थान जैसी जगहें इस भविष्य से जुड़ती दिखती हैं
    अल्पकाल में, इस तरह का शोध AI systems की सटीक जानकारी उत्पन्न करने की क्षमता को काफ़ी बेहतर करेगा

  • कुछ लोग मानते हैं कि ज्ञान की खोज बस अतीत के व्यवहार की नकल करना है, लेकिन मैं ऐसा नहीं मानता

  • अगर कोई expert मॉडल को ठीक से guide करे, तो ज़्यादातर समस्याएँ हल की जा सकती हैं
    मॉडल expert के उबाऊ काम की जगह लेने वाले tool के रूप में शानदार हैं, लेकिन जटिल समस्याओं में अब भी blind spots मौजूद हैं

  • मैंने paper में system prompt का एक हिस्सा देखा,
    उसमें नियम था: “हर exploreXX.py चलाने के तुरंत बाद plan.md को update करो”
    मुझे जिज्ञासा है कि ऐसे prompts उन्नत problem-solving performance को बेहतर क्यों बनाते हैं

    • शायद यह प्रक्रिया को खोए बिना फिर से शुरू करना आसान बनाने के लिए होगा

  • हम धीरे-धीरे OpenAI CEO के “intelligence as a subscription” वाले विज़न के और क़रीब पहुँच रहे हैं

  • tab switching कम करने की अहमियत को कम आँका जा रहा है
    AI tools की आधी लड़ाई UX की नहीं, बल्कि model access की स्थिरता सुनिश्चित करने की है

  • “अगर 100 बंदरों को 100 बंदूकें और निर्माण सामग्री दे दी जाए, तो क्या वे घर बनाएँगे या बैंक लूटेंगे?”
    अगर ऐसा कोई नतीजा सामने आए, तो मैं पूछना चाहूँगा कि क्या वह इरादतन किया गया व्यवहार माना जाएगा

  • मैंने यह ट्वीट देखा

    • ज़्यादातर replies साफ़ तौर पर AI द्वारा बनाए गए वाक्य-पैटर्न जैसे लगे — “वह X नहीं, Y है” जैसी दोहराव वाली शैली