गणित में एक भूत है

• Lean गणित को औपचारिक रूप में लिखने के लिए डिज़ाइन की गई प्रोग्रामिंग भाषा है, जो गणितज्ञों को गणितीय प्रमेयों को कोड की तरह संभालने की सुविधा देती है
• उपयोगकर्ता प्रमेय, प्रमाण, स्वयंसिद्ध आदि को कोड के रूप में लिखते हैं, और प्रमाण निर्माण tactic नामक निर्देशों के सेट के माध्यम से आगे बढ़ता है
• प्रमाण सच में पूरा न होने पर भी इसे sorry से अस्थायी रूप से बंद किया जा सकता है, लेकिन यह TypeScript के any जैसा एक झूठा प्रमाण है
• यदि गलत स्वयंसिद्ध जोड़ दिए जाएँ (जैसे 2 = 3), तो तार्किक विरोधाभास और सभी दावों के सिद्ध हो जाने की संभावना जैसी जोखिमपूर्ण स्थिति उत्पन्न होती है
• Lean केवल चुने हुए स्वयंसिद्धों और प्रमाण प्रणाली पर ही निष्कर्ष निकालता है, इसलिए गणितीय वैधता को बनाए रखना इसका बड़ा महत्व रखता है

---

Lean: गणित को कोड में संभालने वाली भाषा

• Lean औपचारिक गणित लिखने के लिए बना हुआ एक विशिष्ट प्रोग्रामिंग भाषा है
• गणितज्ञ Lean की सहायता से गणित को कोड में व्यक्त करते हैं और एक-दूसरे के प्रमेय व प्रमाणों को संगठित कर सहयोग एवं साझा करना आसान बनाते हैं
• आगे चलकर मानवता का विशाल गणितीय ज्ञान कोड के रूप में मशीन-सत्यापन और संयोजन के लिए उपलब्ध हो सकता है—यह भविष्य की दिशा दिखाता है

Lean प्रमाण की पहली सीढ़ी

• theorem two_eq_two : 2 = 2 := by sorry के रूप में Lean में सरल प्रमेय घोषणा की जा सकती है
• यदि प्रमाण अधूरा हो तो sorry डालते हैं, पर यह केवल एक अस्थायी उपाय है, वास्तविक प्रमाण नहीं
  • sorry Lean का प्रमाण सत्यापन पार करा देता है, लेकिन तार्किक दृष्टि से भरोसेमंद नहीं होता
• पूर्ण प्रमाण के लिए rfl (reflexivity) जैसी tactic का उपयोग कर 2 = 2 जैसे सहज समता का प्रमाण दिया जाता है
• पहले से सिद्ध सामग्री को exact जैसे शब्दों के साथ अन्य प्रमेयों में पुनः उपयोग किया जा सकता है, जिससे मॉड्यूलरिटी पर जोर मिलता है

स्वयंसिद्ध और विरोधाभास: जब गणित भुतहा हो

• यदि axiom math_is_haunted : 2 = 3 जैसे कोई स्वयंसिद्ध जोड़ा जाए, तो Lean उसे सत्य के रूप में मान लेता है
• यही स्वयंसिद्ध आगे के प्रमाण चरणों में प्रयोग हो सकता है और गणितीय रूप से गलत निष्कर्ष जैसे (2 + 2 = 6) भी सिद्ध किए जा सकते हैं
• rewrite tactic से 2 को 3 में बदलकर और rfl से समानता सिद्ध करके प्रक्रिया पूरी की जा सकती है
• गलत स्वयंसिद्ध से विरोधाभास पैदा होने पर Lean में भी सभी प्रस्तावों के प्रमाण संभव होने की स्थिति (तार्किक पतन) आ जाती है
• वास्तव में, 20वीं सदी के शुरुआती दौर में रसेल का विरोधाभास आदि स्वयंसिद्ध-प्रणाली में विरोधाभासों ने गणित की मूलभूत पड़ताल को जन्म दिया था
• इस तरह Lean स्पष्ट दिखाता है कि स्वयंसिद्ध का चयन तार्किक प्रणाली की वैधता बनाए रखने में निर्णायक भूमिका निभाता है

Lean के रूप में प्रमाण-जांचकर्ता (proof checker)

• यदि स्वयंसिद्ध सही चुने गए हों और Lean तार्किक रूप से सही ढंग से काम करे, तो यह सैद्धांतिक रूप से भरोसेमंद निष्कर्ष दे सकता है
• सरल समानताओं से लेकर बहुत जटिल प्रमेयों (उदाहरण: Fermat’s Last Theorem) तक सभी का सत्यापन समान सिद्धांत पर होता है
• बड़े प्रमेय का ढाँचा नीचे की उप-संरचनाओं और अन्य प्रमेयों के बार-बार प्रमाणित होते जाने से चरणबद्ध तरीके से बनता है
• उदाहरण के लिए, Fermat's Last Theorem को Lean में औपचारिक करने का एक बड़े पैमाने का प्रोजेक्ट जारी है, और अंतिम चरण में बिना किसी sorry के पूर्ण औपचारिक प्रमाण संरचना बनाने की अपेक्षा है

Lean सीखने का आनंद

• Lean में प्रमाण निर्माण कोडिंग और गणित का एक रचनात्मक मिश्रण है
• शुरुआत में सरल कथनों के प्रमाण से शुरुआत कर, धीरे-धीरे जटिल और गहरी गणित को कठोरता से क्रमबद्ध करने की प्रक्रिया ही सबसे बड़ा आनंद बन जाती है
• आधिकारिक ट्यूटोरियल और समुदाय संसाधन (जैसे Natural Numbers Game, Mathematics in Lean आदि) शुरुआत के लिए उपयुक्त हैं
• Lean का उपयोग करके आप सीधे तर्क को औपचारिक करते हैं और चतुर विचार व तर्क की सुंदरता को फिर से खोजते हैं
• किसी अतिरिक्त कारण के बिना भी, कुछ लोगों के लिए यह निष्कर्ष निकलता है कि Lean में खास मज़ा है

[GN⁺]

Hacker News की राय

• मैं इन दिनों Lean जैसे सिस्टम (या खुद Lean) का इस्तेमाल करके समाचार या non-fiction लेखों को फिर से लिखने के विचार पर सोच रहा हूँ, जहाँ हर कथन को एक ऐसे theorem की तरह देखा जाए जिसे साबित करना हो, और proof में citations भी शामिल हों। उदाहरण के लिए, “अगर मेरे द्वारा स्वीकृत तीन स्रोत किसी बात को तथ्य कहते हैं, तो वह तथ्य है” जैसी composite proof के रूप में इसे संभाला जा सकता है। और मुझे लगता है कि पूरे दस्तावेज़ को इस तरह markup करना संभव होगा कि “प्रमाणित” दावों को highlight करके देखा जा सके। यह परफ़ेक्ट नहीं होगा, लेकिन आजकल पत्रकारिता जिस rigor की जिम्मेदारी निभाती थी, उसे तकनीक के ज़रिए फिर से हल करने की एक कोशिश है।
  • प्राकृतिक भाषा के कथनों को formalize करना बहुत सारी कठिनाइयों वाला क्षेत्र है, लगभग उन्हीं कारणों से जिनकी वजह से वास्तविक दुनिया से इंटरैक्ट करने वाला code लिखना कठिन होता है। जिन अवधारणाओं को हम स्वाभाविक मान लेते हैं — जैसे identity, time, causality — उन सबको formal system के भीतर बारीकी से संभालना पड़ता है, तभी तथ्यों को आपस में जोड़ा या व्यक्त किया जा सकता है। फिर भी यह समस्या वास्तव में बहुत दिलचस्प है। OpenCog इस क्षेत्र को अंत तक ले जाने की कोशिश करने वाला एक प्रोजेक्ट था, और knowledge representation and reasoning (KRR) नाम का एक अलग शोध क्षेत्र भी अकादमिक जगत में मौजूद है। IJCAI जर्नल भी इसी तरह के शोध से भरा हुआ है। और दार्शनिकों ने time/modality/probability जैसी विभिन्न दलीलों को formalize करने के लिए कई तरह की logic लिखी हैं, लेकिन अफ़सोस कि ये आसानी से एक-दूसरे के साथ जुड़ती नहीं हैं (कम-से-कम जब तक हाल में यह समस्या हल न हुई हो)।
  • मेरा मानना है कि समाचार के संदर्भ में जिन सबसे महत्वपूर्ण मान्यताओं की हमें ज़रूरत होती है, वे अधिकतर ऐसे absolute statements के समूह नहीं होते जिन्हें साबित किया जा सके। मुझे लगता है Bayesian probability जैसे tools, जो inference chains की गणना कर सकें, ज़्यादा उपयुक्त होंगे। इस तरह के numerical estimation tools मैंने देखे हैं।
  • मेरा अनुभव है कि विश्वविद्यालय में गणित पढ़ने के बाद मेरा non-fiction लेखन काफ़ी बेहतर हुआ। मैं अपने SO (partner) और अपनी बहन के लिखे essay पढ़कर, लगभग किसी logical proof की तरह, इस तरह rigor लागू करता था: “यहाँ C को B से निकला हुआ बताया गया है, लेकिन B के A से निकलने का कारण वास्तव में गायब है, इसलिए यह नहीं कहा जा सकता कि C, A से निकला है।” LLM जैसे tools की मदद से इसे प्रोग्राम के रूप में बनाना संभव लगता है, लेकिन hallucination (तथ्यहीन दावे गढ़ना) की वजह से इसकी सीमाएँ स्पष्ट हैं।
  • सावधान रहने की ज़रूरत है। ऐसा approach अपने-आप किसी भी ऐसे दावे को, जो असल में बेहद कट्टरपंथी या बेतुका हो, logical objectivity का एक aura दे सकता है। आधुनिक logic के प्रमुख जनकों में से एक Gottlob Frege के राजनीतिक विचार इस बारे में चेतावनी हो सकते हैं संबंधित लिंक
  • मुझे तो किसी विशेष विषय की पूरी argument structure को नक्शे की तरह बनाना ज़्यादा दिलचस्प लगेगा। उदाहरण के लिए “क्या ईश्वर है?” जैसे बड़े सवाल से शुरुआत करके, पक्ष और विपक्ष के तर्क, उन पर आपत्तियाँ, और फिर उन आपत्तियों पर जवाब — सबको hierarchy में फैलाकर देखना। हर दावे के साथ “Plato ने ऐसा तर्क दिया था” जैसी citation को प्रमाण के बजाय ऐतिहासिक संदर्भ देने के लिए रखा जाए। लक्ष्य किसी बहस का फ़ैसला करना नहीं, बल्कि argument map बनाना है ताकि हम बार-बार उसी बिंदु पर चक्कर न काटें।
• मैं जानना चाहता हूँ कि क्या हम आख़िरकार कुछ self-evident truths से शुरू होने वाला proofs का एक dictionary बना रहे हैं, जिसके ऊपर तरह-तरह के proofs तर्कसंगत रूप से जुड़ते जाते हैं? फिर अतिरिक्त proofs तो बस पहले से मौजूद proofs के logical combinations होंगे। काश इसे Zachtronics-स्टाइल गेम बना दिया जाए! Euclidea नाम का एक गेम trigonometry के क्षेत्र में कुछ ऐसा एहसास देता है, और इस तरह logic की tower बनाते जाने का concept बेहद आकर्षक है। क्या pure mathematics मूल रूप से यही है? क्या pure mathematics के professors इस logical dictionary को बढ़ाने में आनंद महसूस करते हैं? और मुझे याद है कि किसी प्रसिद्ध गणितज्ञ ने बुनियादी proofs की एक सूची बनाई थी — अगर कोई बता सके कि वह कौन था (या क्या था) और उसे क्या कहा जाता है, तो अच्छा होगा। शायद वही axioms हैं।
  • इससे जुड़ा एक गेम पहले से है, हालाँकि हो सकता है कि वह बिल्कुल वही न हो जो आप चाहते हैं (और वह पूरे गणित को बनाने वाला गेम भी नहीं है)। मैंने इसे खेला है, और यह काफ़ी मज़ेदार था। इस लेख में उल्लिखित leanprover-community/nng4 उसका उदाहरण है।
  • “इसे Zachtronics-स्टाइल गेम बना दो” वाले बिंदु पर कहूँ तो, गणित को ही वह गेम कहा जा सकता है (थोड़ा मज़ाक में)। लेकिन उसका गेम संस्करण सचमुच बहुत मज़ेदार होगा। Pure mathematics वास्तव में ऐसा ही system है। स्नातक स्तर पर यह एहसास सही बैठता है, हालाँकि research papers के स्तर पर जाकर बात थोड़ी बदल जाती है। अगर आपको गेम जैसा अनुभव चाहिए, तो Dummit and Foote जैसी abstract algebra की किताब देखना भी अच्छा रहेगा। Proofs में game-जैसा आनंद है, और मशहूर किताबों में अगर आप अटक जाएँ तो अक्सर online solutions भी मिल जाते हैं।
  • हो सकता है आप Euclid के axioms की बात कर रहे हों, जहाँ point, line, plane, parallel line जैसी अवधारणाओं को परिभाषित किया गया है। लेकिन sphere पर यह system टूट जाता है। या फिर आप Zermelo-Fraenkel set theory (ZF/ZFC) की बात कर रहे हों, जिस पर आधुनिक गणित पूरी तरह निर्मित है।
  • Bombe नाम का एक गेम भी है, जो Minesweeper का एक variant है। इसमें सीधे cells खोलने के बजाय आप “किन परिस्थितियों में flag लगाया जा सकता है” जैसे नियम बनाते हुए खेलते हैं। जैसे-जैसे level बढ़ता है, नियम lemmas की तरह आपस में chain होने लगते हैं। और जब खिलाड़ी की skill बढ़ती है, तो toolkit की constraints हटाकर generalization भी संभव हो जाता है। गेम लिंक
  • गणित मूलतः axioms से शुरू होकर निष्कर्ष निकालने की प्रक्रिया है। बेशक बस इतना ही नहीं है, लेकिन मेरी समझ के स्तर पर मैं इसे ऐसे ही देखता हूँ।
• थोड़ा nitpick कर रहा हूँ, लेकिन यह कहना कि two_eq_two theorem एक function जैसा दिखता है, थोड़ा अजीब है। उसमें कोई arguments नहीं हैं, इसलिए वह constant के ज़्यादा क़रीब है (हालाँकि मैं मानता हूँ कि constants भी बिना arguments वाले functions ही होते हैं)। नीचे की तरह x_eq_x का इस्तेमाल करके 2_eq_2 में function की तरह apply करना ज़्यादा विश्वसनीय लगेगा।

  theorem x_eq_x (x:nat) : x = x := by
    rfl
  
  theorem 2_eq_2 : 2 = 2 := by
    exact (x_eq_x 2)
  

  यहाँ x_eq_x function जैसा दिखता है, और 2_eq_2 में वास्तव में उसी तरह इस्तेमाल भी हुआ है।
  • बिल्कुल सही बात! मैंने ऐसा इसलिए नहीं किया क्योंकि Lean में arguments को संभालने का तरीका (खासकर dependent types जैसी concepts — जहाँ x देने पर x = x का proof लौटता है) मेरे लिए थोड़ा अपरिचित है, और वह अपने-आप में अलग विषय है। अगले लेख में उसी पर बात करूँगा।
• Lean सीखते हुए मुझे यह कठिन लगा कि tactics (rfl जैसी) बहुत ज़्यादा व्यापक हैं, और tutorial से भी उनका सटीक मतलब समझना कठिन है। उदाहरण के लिए, C भाषा में आप bit-level तक state changes को ट्रैक कर सकते हैं, लेकिन Lean में चीज़ें कुछ धुंधली लगती हैं। और rewrite (rw) tactic की syntax भी स्वाभाविक नहीं लगती।
  • Coq (अब Rocq) में भी tactics की आदत डालना हमेशा कठिन था। उदाहरण के लिए, जब आपके पास “A = B” और “P(A,A)” हो, और आप “P(A,B)” तक जाना चाहें, तो rewrite किसी समझ में न आने वाले कारण से काम नहीं करता था (शायद बीच की structure definitions की वजह से)। दूसरी ओर, Metamath और उसका set.mm database बिना किसी tactic के सिर्फ़ concrete reasoning से proofs करवाते हैं (जैसे ax-mp जैसी inference rules), लेकिन वहाँ समस्या यह है कि आपको काम के utility lemmas काफ़ी याद रखने पड़ते हैं, इसलिए वह भी आसान नहीं है।
  • यही उन कारणों में से एक है जिनकी वजह से मैं Agda को ज़्यादा पसंद करता हूँ। Agda में लगभग tactics होते ही नहीं; Curry-Howard correspondence का उपयोग करके आप functional programming language की तरह सीधे proof terms लिखते हैं। लेकिन अगर आप abstraction और functions बनाने में आलसी हो जाएँ, तो मामूली चीज़ें भी बेहिसाब झंझट बन जाती हैं, इसलिए discipline ज़रूरी है।
  • कम-से-कम Lean में आप tactics की definition पर “go to definition” करके उसका अंदरूनी व्यवहार देख सकते हैं। सीखते समय उसकी मात्रा बहुत भारी लगती है, लेकिन अंततः सब कुछ देखा जा सकता है (हालाँकि basic type theory तक पहुँचने पर समझना मुश्किल हो जाता है)। और आपने कहा कि rewrite syntax स्वाभाविक नहीं लगती, तो मुझे जानने में दिलचस्पी है कि आपके लिए स्वाभाविक rewrite syntax कैसी होगी?
  • मुझे जो बात दिलचस्प लगी, वह यह कि tactics पूरी तरह “user-level” code हैं, proof kernel के बाहर। यह समझ में आता है, क्योंकि आप छोटे और सत्यापित kernel को बिना बदले बनाए रखना चाहते हैं। लेकिन इसका यह भी मतलब है कि जब tactics अपग्रेड हों या बदले जाएँ, तो पुराने proofs टूट सकते हैं। व्यवहार में यह कितनी बड़ी समस्या बनती है, यह जानने की जिज्ञासा है।
  • मेरी अपेक्षा के विपरीत, Lean में reflection और rewrite शायद addition से भी अधिक मूलभूत होंगे, ऐसा लगा था। Lean addition तो built-in देता है, लेकिन rfl या rewrite हर बार खुद लिखना पड़ता है। शायद Lean में कोई prelude जैसी चीज़ हो, जो इसे अपने-आप कर दे।
• मैं जानना चाहता हूँ कि Lean में proofs को noninteractive तरीके से पढ़ने का कोई तरीका है या नहीं। natural number game खेलते समय proofs सिर्फ़ rw [x] कमांडों की सूची जैसे लगते थे, इसलिए उन्हें पढ़ना बहुत मुश्किल था। editor में हर लाइन की state देखी जा सकती है, लेकिन लगातार क्लिक करना पड़ता है, जिससे flow टूट जाता है। Python में भी अगर indentation न हो और flow समझने के लिए block structure पर क्लिक करना पड़े, तो वही समस्या होगी। हो सकता है यह मेरी नज़र में game की शुरुआती सीमित commands की वजह से हो, लेकिन मैं जानना चाहता हूँ कि full Lean environment में यह flow बेहतर लगता है या नहीं।

  • क्या Lean में proofs को noninteractive तरीके से पढ़ने का कोई तरीका है?
    मैंने भी हाल में यही सोचा और खोजा था। lean-in-latex ब्लॉग ऐसा तरीका देता है जिससे editor के बाहर, बिना क्लिक किए, उस flow का पीछा किया जा सकता है। और इससे यह भी देखने को मिलता है कि Lean community इसे कैसे approach करती है।

  • Rocq में पहले “mathematical proof language” नाम की चीज़ हुआ करती थी। इसके असली उपयोग के उदाहरण मिलना मुश्किल है, लेकिन यह कुछ ऐसा दिखता था:

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.
    

    यह approach proofs को research papers में लिखे “हाथ से किए गए proofs” जैसा पढ़ने योग्य बनाती थी। लेकिन इसका लगभग उपयोग नहीं हुआ, इसलिए यह गायब हो गई। Isabelle की Isar proof language भी कुछ ऐसी ही है, और बल्कि वह standard शैली के अधिक क़रीब है। उदाहरण:

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed
    

    इसमें पूरी logical structure और intermediate results साफ़-साफ़ लिखे जाते हैं, और सिर्फ़ वहीं by ... से tactics को छोटा किया जाता है जहाँ बारीक details महत्वपूर्ण हों। Lean में इसका कोई समकक्ष है या नहीं, यह नहीं जानता, लेकिन कम-से-कम इसे search keywords या Lean forum में पूछने के विषय के रूप में इस्तेमाल किया जा सकता है।
  • यह वास्तव में बहुत अच्छा सवाल है! मैं अभी भी शुरुआती हूँ, इसलिए पूरी तरह भरोसे के साथ नहीं कह सकता, लेकिन जो महसूस किया है वह साझा कर सकता हूँ। Lean को लगभग दो महीने इस्तेमाल करने के बाद मुझे लगा कि proof code पढ़ना programming code पढ़ने जैसा नहीं, बल्कि “scan” करने जैसा है। आप समग्र argument structure, कौन-सी tactics इस्तेमाल हो रही हैं, कौन-से lemmas बुलाए जा रहे हैं — इन चीज़ों पर ध्यान देते हैं। असली Lean code style में हर नए goal पर indentation बढ़ती है, और goal समाप्त होने पर फिर कम हो जाती है। इसलिए argument का “shape” महत्वपूर्ण हो जाता है। मेरे PR का उदाहरण देखें। जब tactics की आदत हो जाती है, तो intro देखकर पता चल जाता है कि quantifier के भीतर जा रहे हैं, constructor goal split कर रहा है, वगैरह। आखिरकार tactics proofs का tree (term tree) बनाने वाला macro/DSL हैं। मैं proof code को tree manipulation की तरह देखता हूँ — टुकड़ों में बाँटना, क्रम भरना, आदि। फिर भी proof code के बीच की assertions को ठीक-ठीक जानने के लिए क्लिक करना पड़ता है, यह बात बनी रहती है। जिन proofs में अच्छा idea होता है, वे paper की logical exposition की तरह साफ़ पढ़े जा सकते हैं। इसलिए जो लोग इरादा स्पष्ट करना चाहते हैं, वे readable names, साफ़ progression, छोटे lemmas निकालना, और hypotheses पहले लिखकर छोटे proof code से बात ख़त्म करना — इस तरह लिखते हैं। दूसरी ओर, मशीन के लिए तो मेहनत भरा लेकिन गणितज्ञ की नज़र में बिल्कुल स्पष्ट हिस्सा अक्सर “golfing” (सबसे छोटा code) से निपटाया जाता है। Golf style में code छोटा तो हो जाता है, लेकिन वह अक्सर वही हिस्से समेटता है जो इंसान सहज रूप से समझता है। संक्षेप में, Lean में पढ़ी जाने वाली structure कुछ हद तक implicit है, लेकिन उसे अधिक स्पष्ट करने के तरीके भी हैं; और tactics में निपुणता बढ़ने पर बिना क्लिक किए भी structure ज़्यादा समझ आने लगती है। सिर्फ़ lemma names को सरसरी नज़र से देखकर भी बड़ी तस्वीर का पता चल जाता है, और क्रम आसानी से फिर से बनाया जा सकता है।
• सामग्री सचमुच बहुत अच्छी थी। बहुत कम लोग इस तरह की चीज़ों को आसानी से समझ आने वाले तरीके से समझा पाते हैं। जो छोटे-छोटे कदम विशेषज्ञ लोग यूँ ही छोड़ देते हैं, उन्हें सब दिखा देना ही शायद इसका राज़ है।
  • धन्यवाद!
• क्या इस थ्रेड में Lean बनाम idris/coq/agda के भविष्य पर लोगों की राय मिल सकती है? मैं knowledge representation पढ़ना चाहता हूँ, लेकिन किसी एक चीज़ में गहराई से उतरने से पहले community size और future risk की चिंता होती है। पहले मैंने clojure core.logic में समय लगाया था और बहुत कम रुचि/छोटी community की वजह से बुरा अनुभव हुआ था, इसलिए आसानी से शुरुआत नहीं कर पा रहा।
  • मेरे वास्तविक अनुभव के आधार पर Lean और Coq/Rocq, Idris और Agda की तुलना में कहीं ज़्यादा इस्तेमाल होते दिखते हैं, और उनकी libraries व communities भी बड़ी हैं। Rocq का उपयोग program verification में अधिक है, जो शायद उसके लंबे इतिहास की वजह से है; उसमें कई विशिष्टताएँ भी हैं, इसलिए Lean भविष्य में उसे पकड़ सकता है। Lean सबसे ज़्यादा mathematical theorem proving में दिखता है। Rocq के प्रसिद्ध projects में CompCert, CertiCoq, sel4 शामिल हैं, और विमान सॉफ़्टवेयर verification में इसके उपयोग के उदाहरण भी हैं (संकलित project list देखें)। Lean में mathlib (गणितीय proofs का संग्रह), Fermat’s Last Theorem (FLT proof project), PFR जैसे बड़े प्रोजेक्ट हैं। मेरी जानकारी में Idris और Agda के पास ज़्यादा “real-world” प्रोजेक्ट नहीं हैं, हालाँकि मैं गलत भी हो सकता हूँ। बेशक इन सबका पैमाना C++ या JavaScript जैसी भाषाओं या communities की तुलना में बहुत छोटा है। और सच कहें तो program verification बहुत धीमा और उबाऊ काम है। संभव है कि AI जैसी किसी बुनियादी प्रगति से भविष्य में बड़ा बदलाव आए, लेकिन जो कौशल आप सीखते हैं, वे तब भी उपयोगी रहेंगे।
  • मुझे लगता है कि इस क्षेत्र पर दांव लगाना शायद सही तरीका नहीं है। वास्तव में अधिकांश गणितज्ञ formalization में बहुत रुचि नहीं रखते, क्योंकि हाथ से लिखे proofs और कंप्यूटर द्वारा माँगी गई सख़्त syntax के बीच बहुत बड़ा अंतर है। इसे बस सीखने और प्रयोग करने की खुशी से अपनाना चाहिए। भविष्य की दृष्टि से Lean हाल के समय में सबसे सक्रिय दिखता है, लेकिन हर सिस्टम का पुराना user base है, इसलिए कोई ठोस भविष्यवाणी करना मुश्किल है।
• मैं यह जानना चाहता हूँ कि क्या बिना किसी technique या tricks के, Lean में बस कोई random चीज़ फेंक देने से, सिर्फ़ उसके pass/fail होने के आधार पर दिलचस्प discoveries निकाली जा सकती हैं। या फिर क्या इसे automation systems या LLMs के साथ चलाकर कठिन proofs/theories पर अंधाधुंध कोशिश की जा सकती है और सफलता/असफलता देखी जा सकती है? सवाल थोड़ा अजीब लग सकता है, लेकिन मैं Prolog भी बस मुश्किल से समझता हूँ।
  • certified programming को पेशेवर रूप से करने वाले व्यक्ति के रूप में, मुझे लगता है कि generative AI और formal methods एक बेहतरीन मेल हैं। आगे चलकर LLM programmers की जगह ले पाएँगे या नहीं, यह काफी हद तक इस पर निर्भर करेगा कि AI certified programming और combinatorial reasoning को कितना अच्छे से कर पाता है।

    क्या random चीज़ें फेंकने से दिलचस्प खोजें होती हैं?
    पुरानी AI checkers जैसे कम branching-factor वाले खेलों में अच्छी थी। Chess थोड़ा कठिन है, और Go तो machine learning के बिना पारंपरिक AI के लिए लगभग असंभव था। Formal languages में possibilities और searchable states की संख्या कल्पना से परे होती है। अगर समस्या की प्रकृति पर्याप्त साफ़ हो, तो SMT solver के ज़रिए brute force संभव है। मूल रूप से SMT solver और proof assistant formal methods की अलग-अलग शाखाएँ थे, लेकिन अब वे एक-दूसरे के पूरक बनते जा रहे हैं (Sledgehammer, Lean-SMT देखें)।
    अगर LLM या automated system को मनमाने proofs/theories आज़माने दिए जाएँ?
    यह अभी मुख्यधारा शोध तो नहीं है, लेकिन इस दिशा में काफ़ी काम हो रहा है। LLM boom से पहले भी कई सालों से बड़े funders इस पर पैसा लगा रहे थे। “Learning to Find Proofs and Theorems by Learning to Refine Search Strategies” जैसे पुराने प्रयास रहे हैं, और DeepSeek-Prover जैसे नए शोध भी हैं। अभी यह पूरी तरह खुला प्रश्न है कि इन्हें कैसे train किया जाए और भविष्य की सीमा कहाँ तक हो सकती है।
    मौजूदा LLMs Rocq और Lean भाषाओं में अभी भी कमज़ोर हैं, और जब वे गलत उत्तर देते हैं तो उसे ठीक करना बेहद कष्टदायक होता है। फिर भी मुझे उम्मीद है कि समय के साथ AI tools का स्तर बहुत ऊपर जाएगा।

  • यह वास्तव में बहुत सक्रिय शोध और प्रयोग का क्षेत्र है!
    Lean community का बड़ा हिस्सा Zulip पर इकट्ठा होता है, और Machine-Learning-for-Theorem-Proving चैनल में कई उपयोगी threads मिलेंगे।
• alphaproof को देखकर ही मेरी पहली बार Lean में रुचि जगी थी, और यह परिचयात्मक लेख बहुत अच्छा लगा। क्या आप बता सकते हैं कि आप Lean में अभी क्या कर रहे हैं?
  • अभी तो मैं सिर्फ़ Lean के साथ गणित पढ़ रहा हूँ। खास तौर पर Tao की Lean पाठ्यपुस्तक को follow कर रहा हूँ, और exercises में छोड़े गए sorry वाले हिस्सों को खुद भरकर सीख रहा हूँ (मेरे solutions यहाँ हैं)।
• क्या Lean में ऐसा कोई verification mode है जो अपने-आप यह रोक दे कि proofs में अविश्वसनीय चीज़ें (जैसे sorry) इस्तेमाल हों या बार-बार नए axioms जोड़ दिए जाएँ? जैसे यह जाँचना कि “proof किसी भी तरह sorry का उपयोग नहीं करता” या “यह एक निश्चित axiom set की proof power पर निर्भर है” — क्या ऐसा verify किया जा सकता है?
  • लेख के बाद के हिस्से में उल्लिखित #print axioms some_theorem शायद यही उदाहरण है। इससे आप देख सकते हैं कि वह proof प्रत्यक्ष या अप्रत्यक्ष रूप से sorry या किसी unreviewed axiom पर निर्भर करता है या नहीं।
  • print axioms से यह जाँचा जा सकता है कि कोई अतिरिक्त axioms तो नहीं जोड़े गए, और यह भी देखा जा सकता है कि चीज़ें बिना warning या error के compile होती हैं या नहीं। SafeVerify utility उन कुछ tricks को भी पकड़ लेती है जो RL systems ने खोज निकाली थीं।
  • यह भी बताया गया है कि macros से ऐसा किया जा सकता है, यहाँ देखें।