सिर्फ Lean ही क्यों न इस्तेमाल करें

 (lawrencecpaulson.github.io)
1 पॉइंट द्वारा GN⁺ 1 일 전 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • गणित के formalization का इतिहास Lean से शुरू नहीं हुआ; लगभग 60 साल पहले से कई अलग-अलग परंपराओं के systems ने मुख्य techniques और उपलब्धियाँ पहले ही जमा कर ली थीं
  • 1968 का AUTOMATH, LCF परिवार, HOL, Rocq, ACL2, Mizar जैसे tools ने real analysis से लेकर prime number theorem, four color theorem, और Kepler conjecture तक व्यापक formalization किए हैं
  • Lean ने बड़ी library और सक्रिय community के आधार पर आधुनिक गणितीय definitions को तेज़ी से जमा किया है, लेकिन propositions as types या dependent types ही proof assistant का एकमात्र रास्ता नहीं हैं
  • Isabelle मज़बूत automation, उच्च readability, और dependent types से बचाव को अपनी ताकत बताता है, और proof object के बिना भी kernel की abstraction barrier से proof checking बनाने वाली LCF परंपरा को आगे बढ़ाता है
  • AI structured proofs को व्यवस्थित करने और उन्हें दूसरे systems में अनुवाद करने की दिशा भी जोड़ रहा है, इसलिए भविष्य में किसी एक tool को ही अंतिम मानक मानने का दबाव और कम हो सकता है

शुरुआती systems और दूसरी परंपराएँ

  • AUTOMATH

    • AUTOMATH में 1968 में ही गणित के formalization के लिए ज़रूरी लगभग सभी तत्व मौजूद थे
    • 1977 में Jutting ने AUTOMATH के साथ Landau की Foundations of Analysis का formalization किया, और pure logic से शुरू करके complex numbers की construction तक पहुँचे
    • इसमें equivalence classes और rational numbers के set का उपयोग हुआ, और real line की Dedekind completeness भी औपचारिक रूप से सिद्ध की गई
    • यह उपलब्धि 20 साल तक दोबारा नहीं आई, और 1990 के दशक के मध्य में जाकर John Harrison के HOL Light और Jacques Fleuriot के Isabelle/HOL में real numbers का formalization फिर से हुआ
    • notation बहुत असुविधाजनक थी और automation बिल्कुल नहीं था, इसलिए proofs लंबे और पढ़ने में कठिन थे
    • फिर भी equivalence classes को संभालने में इसे Rocq से बेहतर माना गया है; Rocq users जिस setoid hell से जूझते हैं, उसके विपरीत Jutting ने equivalence class formalization को शांत ढंग से किया

  • Boyer और Moore

    • Robert Boyer, J Moore की computational logic परंपरा गणित नहीं बल्कि code verification को लक्ष्य बनाकर शुरू हुई
    • 1973 के पेपर Proving theorems about LISP functions में यह दिशा पहली बार स्पष्ट हुई
    • सामान्य गणित में इसकी साफ सीमाएँ थीं, फिर भी Gödel का incompleteness theorem, quadratic reciprocity, Banach–Tarski theorem जैसे गहरे परिणामों के formalization में भी इसका उपयोग हुआ
    • इसकी वर्तमान परंपरा ACL2 मुख्यतः hardware verification में लागू होती है

LCF के बाद की धारा

  • Edinburgh LCF programming language theory पर केंद्रित था, लेकिन proof assistant की meta-language के रूप में functional language रखने का विचार व्यापक रूप से फैल गया
  • Cambridge, INRIA, Cornell जैसे कई groups ने ML का उपयोग करके शुरुआती HOL, Coq (अब Rocq), Nuprl जैसे tools बनाए
  • HOL group hardware verification पर केंद्रित था, लेकिन floating-point hardware verification के कारण real analysis की ज़रूरत पड़ी
  • John Harrison ने Cauchy integral formula के माध्यम से prime number theorem जैसे गंभीर गणितीय परिणाम HOL परिवार में सिद्ध किए
  • 100 theorems में जितना संभव हो उतने प्रमेय verify करने के लक्ष्य के तहत HOL Light अक्सर शीर्ष स्थानों में रहा
  • 2014 तक इस परिवार के systems कई उन्नत प्रमेयों का formalization कर चुके थे
  • ये प्रमेय अधिकांशतः लंबे और जटिल proofs वाले थे, formalization का काम भी बहुत बड़े पैमाने का था, और उन्होंने प्रमेयों में बचे संदेहों को कम करने में महत्वपूर्ण भूमिका निभाई

Lean community का उभार

  • गणितज्ञों का मानना था कि पहले की formalization उपलब्धियाँ Grothendieck schemes या perfectoid spaces जैसी मुख्यधारा की आधुनिक गणितीय संरचनाओं तक नहीं पहुँच पाई थीं
  • Tom Hales ने ऐसी definitions को library के रूप में जमा करने का रास्ता चुना, और proofs से अधिक definitions के संचय पर ध्यान देते हुए Lean को चुना
  • उन्होंने Big Proof कार्यक्रम में यह दिशा प्रस्तुत की, और इसी तरह के विचार भी साथ में चर्चा में आए
  • Kevin Buzzard ने यह सुनकर शिक्षा में Lean को आज़माने का निर्णय लिया, जिसके बाद इसका प्रसार तेज़ हो गया
  • Lean community के एक महत्वपूर्ण turning point के रूप में यह बात रखी गई कि वह Rocq पर लंबे समय तक हावी रही constructive proof के प्रति आसक्ति से बाहर निकली
  • intuitionism Russell के paradox के बाद उभरा, और real numbers की अवधारणा पर भी इसके खास निहितार्थ थे
  • Martin-Löf type theory निश्चित रूप से intuitionistic formalism है, लेकिन लिखा गया है कि Rocq को इतनी सरलता से नहीं देखा जा सकता
  • फिर भी Rocq से जुड़े papers में constructive proof बार-बार वहाँ भी सामने आता रहा जहाँ वह अप्रासंगिक या अर्थहीन था, और माना गया कि इसी प्रवृत्ति ने Rocq के गणितीय उपयोग को रोका और जगह Lean को दे दी

propositions as types और LCF का अंतर

  • Propositions as types logical symbols ∀, ∃, →, ∧, ∨ और type constructors Π, Σ, →, ×, + के बीच की द्वैतता है
  • यह ढाँचा सुंदर और सैद्धांतिक रूप से उत्पादक है, लेकिन यह एकमात्र रास्ता नहीं है
  • अगर proof assistant को propositions as types सिद्धांत से proofs check करने वाले software तक सीमित कर दिया जाए, तो पिछले आधे शतक का अधिकांश शोध उसकी परिभाषा के बाहर चला जाएगा
  • तब केवल Rocq, Lean, Agda ही बचेंगे
  • AUTOMATH भी propositions as types का उदाहरण नहीं है; उसमें Π और → जैसे तत्व ज़रूर हैं, लेकिन logic को सामान्य logic textbook की तरह axioms के रूप में स्थापित किया जाता है
  • de Bruijn ने 50 साल पहले ही types और propositions को अलग रखने की ज़रूरत देखी थी
  • उदाहरण के लिए division को तीन arguments लेने चाहिए, और (x/y) का मान (y \ne 0) के proof पर निर्भर होगा, इसलिए proof irrelevance की ज़रूरत पड़ती है
  • यह धारणा कि LCF approach, propositions as types के बराबर है भी तथ्यात्मक रूप से गलत बताई गई है
  • Rocq और Lean में proposition का sort Prop होता है, जहाँ एक ही proposition के सभी proof objects को एक ही value माना जाता है, जिससे proof irrelevance मिलता है
  • लेकिन इससे बड़े proof objects गायब नहीं हो जाते; वे वास्तविक systems में अब भी मौजूद रहते हैं
  • Robin Milner की मुख्य खोज यह थी कि LCF में proof object की स्वयं आवश्यकता नहीं होती
  • proof kernel को ML के abstract data type के अंदर रखकर, और inference rules को constructors के रूप में देकर, proofs को dynamic रूप से check किया जा सकता है
  • ML की abstraction barrier के कारण cheating असंभव मानी जाती है
  • ऐसे विशाल terms जो कुछ भी निर्देशित नहीं करते, फिर भी दर्जनों MB घेरते हैं, RAMmageddon के युग में विशेष रूप से अविवेकपूर्ण लगते हैं
  • ऐसी अनावश्यक terms को और अधिक elegant बनाने तक शोध का जाना भी आलोचना का विषय है

Isabelle चुनने के कारण

  • अगर सहकर्मी Lean इस्तेमाल करते हैं, टीम की expertise भी Lean में है, और ज़रूरी foundational library भी Lean में है, तो Lean चुनना स्वाभाविक है
  • फिर भी अगर स्वतंत्र रूप से चुनना संभव हो, तो Isabelle पर विचार करने के स्पष्ट कारण हैं

  • automation

    • इसे सबसे शक्तिशाली automation का लाभ बताया गया है; रोज़मर्रा के “hammer” tools की तुलना में भी sledgehammer की बराबरी करने वाला कुछ नहीं माना गया
    • computer algebra की दिशा को भी अलग से देखने की बात कही गई है

  • readability

    • readability के लिहाज़ से इसे सबसे अच्छा विकल्प माना गया है, और Isar के उदाहरणों को इसका आधार बनाया गया है

  • dependent types से बचाव

    • dependent types न होने के कारण universe level और beginners को उलझाने वाली कई विचित्रताओं से बचा जा सकता है
    • लिखा गया है कि Lean की mathlib और Rocq की SSReflect, Mathematical Components में भी dependent types के उपयोग की सिफारिश नहीं की जाती
    • dependent types की मुख्य कठिनाई यह है कि सही तरह से लागू करने पर type checking स्वयं undecidable हो जाती है
    • ऐसा इसलिए है क्योंकि equality checking undecidable हो जाती है, और शुरुआत में इसे स्वाभाविक माना गया था
    • लगभग 1990 के बाद type checking को decidable बनाने के लिए equality को definitional/intensional equality तक घटाने की दिशा में सहमति बनी
    • नतीजतन (T(N+1)) और (T(1+N)) अलग-अलग types बन जाते हैं
    • ऐसे प्रतिबंध वास्तविक proofs को भी प्रभावित करते हैं, और definitional equality check स्वयं भी अब तक computationally costly है

dependent types के बिना भी आधुनिक गणित

  • लिखा गया है कि 2017 तक Isabelle किस स्तर का गणित संभाल सकेगा, इसे लेकर दृष्टि कहीं अधिक सावधान थी
  • उस समय निम्न विषयों को संभालने के लिए dependent types अनिवार्य लग सकते थे
  • लेकिन Alexandria से जुड़े शोध के माध्यम से बहुत कुछ सीखा गया, और निष्कर्ष यह रहा कि मुख्य बात हर चीज़ को types में ठूँसना नहीं है

आगे की दिशा और AI

  • Lean कई मामलों में सही दिशा पकड़ता है, और nested proof blocks तक का समर्थन करता है, इसलिए उसमें संभावित रूप से पर्याप्त readable proof language बनने की क्षमता है
  • अब Lean community को उन सुविधाओं का वास्तव में उपयोग करना चाहिए, जबकि लिखा गया है कि Isabelle users पहले से अधिकतर ऐसा करते हैं
  • computer-checkable proof objects की तुलना में मनुष्यों के लिए वास्तव में पढ़े जा सकने वाले proof text की पारदर्शिता अधिक महत्वपूर्ण है
  • AI का उभार इस अंतर को और स्पष्ट बना रहा है
  • AI द्वारा बनाए गए proofs अक्सर अव्यवस्थित होते हैं, लेकिन sledgehammer से उन्हें व्यवस्थित करना आसान है, और अगर structure अच्छी हो तो details ज़्यादा होने पर भी वे पढ़े जा सकते हैं
  • इससे आगे की दिशा समझना और उन्हें अधिक सरल रूप में घटाना आसान हो जाता है
  • हाल में ऐसा शोध भी सामने आया है जिसमें language model सीधे sledgehammer को call करता है
  • AI एक proof assistant से दूसरे proof assistant में पढ़ने योग्य structured proofs का अनुवाद भी आसानी से कर सकता है
  • ऐसा होने पर कौन-सा system चुनना है, इस बोझ में ही कमी आ जाएगी

Mizar की अनुपस्थिति की भरपाई

  • गणित के formalization का इतिहास Mizar और उसकी विशाल mathematics library के बिना पूरा नहीं हो सकता
  • Isabelle की Isar language भी Mizar से बहुत प्रभावित रही है
  • Mizar को छूट जाने की बात अलग से सुधारते हुए लिखा गया है कि अगली पोस्ट में Mizar पर चर्चा की जाएगी

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

1 टिप्पणियां

 
GN⁺ 1 일 전
Hacker News की राय

  • ज़्यादातर HN पाठक गणितज्ञों की तुलना में प्रोग्रामर के ज़्यादा करीब हैं, इसलिए गणितीय प्रमाणों की बजाय Lean को प्रोग्रामिंग के नज़रिये से देखना अधिक व्यावहारिक लगता है
    फ़ंक्शनल प्रोग्रामिंग के दृष्टिकोण से Lean को समझाने वाली यह किताब काफ़ी अच्छी है: https://leanprover.github.io/functional_programming_in_lean/
    मैं भी Lean सीख रहा हूँ, इसलिए हो सकता है कि मुझमें एक शुरुआती की गुलाबी नज़र कुछ हद तक हो, लेकिन हाल की lean-zip मिसाल की तरह मेरा लक्ष्य वास्तविक compression/decompression algorithm जैसे साधारण प्रोग्रामर के कोड को लिखना और सिद्ध करना है
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • यह किताब पढ़ते हुए मैंने Lean में एक बुनियादी computer algebra simplifier से खुद प्रयोग किया
      https://github.com/dharmatech/symbolism.lean
      यह C# कोड का पोर्ट है, और Lean की expressiveness हैरान करने वाली है
    • ऐसे उपयोग के लिए क्या Dafny भी एक समान विकल्प नहीं है?
      कुछ समय पहले इसका थोड़ा शोर सुना था, लेकिन हाल में मैंने इस क्षेत्र को बारीकी से फॉलो नहीं किया है
    • मुझे 1990 के दशक के वे प्रयोग याद हैं जिनमें software correctness proof पर काम हुआ था, और याद पड़ता है कि अंतिम proof annotation हिस्से में असली software से भी ज़्यादा गलतियाँ निकल आई थीं
      और मुझे दो और बाधाएँ दिखती हैं। पहली, यह जानना ही मुश्किल है कि software को क्या करना चाहिए, और उपयोगकर्ता जो करना चाहता है वह ज़रूरी नहीं कि वही हो जिसके लिए ग्राहक पैसे देता है
      दूसरी, कई डेवलपर्स के काम की गुणवत्ता इतनी कम होती है कि उनसे Java जैसी भाषा की तुलना में truth language को बेहतर संभालने की उम्मीद करना मुश्किल है
      हालांकि दूसरी समस्या शायद उन AI systems के आने से कम हो जाए जो ज़रूरी सावधानी बरतते हों, और तब स्थिति बदल सकती है
    • फिर non-functional programming का क्या?
      मेरी नज़र में फ़ंक्शनल प्रोग्रामिंग भी, पहले से ही किनारे की गई गणित की तरह, अधिकांश प्रोग्रामरों के लिए बहुत कम प्रासंगिक है

  • लगता है कि लेखक ने Lean को काफ़ी गलत समझा है, और यह इसलिए और भी चौंकाने वाला है क्योंकि वह इस क्षेत्र को अच्छी तरह जानने वाले व्यक्ति जैसे लगते हैं
    ऐसा प्रतीत होता है कि वे सोचते हैं Lean proof objects को जस का तस सुरक्षित रखता है, और अंत में सभी definitions खुल जाने के बाद बने एक विशाल proof object की जाँच करता है, जबकि वास्तविकता इससे काफ़ी अलग है
    Lean वास्तव में वही optimization लागू करता है जिसे लेखक ने LCF की ताकत बताकर सराहा है। उपमा दें तो यह ब्लैकबोर्ड मिटाते हुए प्रमाण आगे बढ़ाने जैसा है
    Lean4 में यदि कुछ def की जगह theorem के रूप में लिखा जाए, तो उसका proof object फिर उपयोग नहीं होता, और यह सिर्फ एक optimization नहीं बल्कि भाषा का मूल गुण है। theorem opaque होता है
    proof term बचा भी रहे तो वह केवल interactive mode में उपयोगकर्ता को दिखाने के लिए होता है, kernel को इस बात से कोई मतलब नहीं होता कि वह proof object क्या था

    • यह implementation से ज़्यादा conceptual difference के करीब है
      LCF में proof और term अलग चीज़ें हैं, और मेरे हिसाब से मूलतः ऐसा ही होना चाहिए। इस तरह की Curry-Howard शैली की गड़बड़ी अनावश्यक है, लेकिन बहुत से लोग मानते हैं कि कंप्यूटर के साथ गणित करने का वही एकमात्र तरीका है
      चाहें तो LCF में भी proofs को स्टोर और reuse किया जा सकता है, और Lean में भी चाहें तो optimization से उन्हें हटाया जा सकता है
    • Dependent type theory में proof object तो बस किसी type को भरने वाला term ही होता है, तो क्या इसका मतलब यह है कि Lean का implementation ऐसे terms बनाए बिना भी proofs बना सकता है?
    • यह बात सही लगती है
      abstract type approach कुछ memory बचा सकती है, लेकिन यह सिर्फ constant-factor अंतर है, asymptotic improvement नहीं
      Lean के दर्जनों MB बर्बाद करने जैसी शिकायतें 1980-90 के दशक में महत्वपूर्ण रही होंगी, लेकिन आज वे शायद उतनी निर्णायक बढ़त नहीं देतीं

  • Lean के बारे में बहुत सुनते हैं कि वह functional programming के लिए अच्छा है, लेकिन Agda से आने पर यह काफ़ी भद्दा downgrade लगता है
    tactic को भी लोग अच्छा कहते हैं, लेकिन मेरे अनुभव में Coq के tactic ज़्यादा शक्तिशाली और इस्तेमाल में आसान थे
    यह सब शायद first-impression bias भी हो सकता है, लेकिन अब तक तो Lean की ताकत किसी एक चीज़ में सर्वश्रेष्ठ होने से ज़्यादा, कुल मिलाकर ठीक-ठाक होने और community बड़ी होने में दिखती है
    यह समझ आता है कि वह आकर्षक क्यों है, लेकिन इसकी कीमत पर थोड़ी सुंदरता और ताकत कम हो गई लगती है

    • आखिरकार बात network effect की भी है
      हालाँकि ऐसे प्रभाव उस समय स्थायी लग सकते हैं, लेकिन वास्तव में वे अक्सर उतने लंबे नहीं टिकते। अगर सच में वही सब कुछ होता, तो Perl आज भी बड़ा नाम होता
      Lean के लिए खास बात यह है कि उसने बड़ी library पहले हासिल कर ली। यह Perl के लिए CPAN जैसी बात है
      लेकिन scaling law देखें तो ज़्यादातर उपयोगकर्ताओं के लिए बड़ी library का मूल्य उसके आकार के log के अनुपात में बढ़ता हुआ लग सकता है
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      शुरुआत में यह फ़र्क़ अपराजेय लग सकता है, लेकिन किसी बिंदु के बाद पैमाने को पकड़ना ज़रूरी नहीं रहता, usability ज़्यादा मायने रखने लगती है
      और math library porting ऐसा काम भी है जो LLM के लिए उपयुक्त है। source verified है, target भी verifiable है, और reasoning path भी आम तौर पर ट्रांसफ़र किया जा सकता है
      उल्टा कहें तो LLM की वजह से छोटे platform पर काम करने की बाधा भी उम्मीद से कम हो जाती है। अगर मैं उनकी library को अपने platform पर ला सकता हूँ, तो संभव है कि मैं अपना proof भी उधर ले जा सकूँ
    • बल्कि यह तो इस बात का संकेत लगता है कि community आख़िरकार mature हुई है और वास्तविक काम करना शुरू कर चुकी है
      मुख्य बात perfect tool नहीं, बल्कि पर्याप्त अच्छे tool के साथ काम निकाल लेना है
    • Agda proof checker के रूप में बेहतर है, लेकिन software बनाने के लिए व्यावहारिक विकल्प नहीं लगता
      Lean में इतने विकसित होने की गुंजाइश दिखती है कि वह सचमुच Haskell का उत्तराधिकारी बन सके, यानी software development के लिए एक functional language के रूप में
    • मैंने Agda थोड़ा और Lean उससे कुछ ज़्यादा इस्तेमाल किया है, और गणितीय proofs की तुलना में सामान्य functional programs लिखना Lean में कहीं आसान लगा
      लगता है फ़र्क़ मुख्यतः tooling support में था। Agda का documentation कमज़ोर है, system पर install करके चलाना भी झंझट भरा है, और लगभग Emacs इस्तेमाल करने पर ज़ोर देता है
      दूसरी ओर Lean के अपने documentation में cat utility लिखने तक का तरीका है, और कुल मिलाकर यह कहीं अधिक modern tooling experience देता है
    • मुझे जिज्ञासा है कि Agda की functional programming में ठीक-ठीक क्या बेहतर है
      आमतौर पर इसकी तारीफ़ dependent pattern matching के लिए सुनता हूँ, और उस हिस्से में Lean सचमुच काफ़ी कमज़ोर लगता है
      फिर भी अगर सामान्य FP में भी Agda ज़्यादा अनुकूल लगती है, तो जानना चाहूँगा कि किस मामले में

  • Isabelle/HOL में भाषा अपने-आप में ठीक है, लेकिन tooling में desktop-केंद्रित दृष्टिकोण से आगे भी गहरी खामियाँ हैं
    भाषा Lean से अनिवार्य रूप से बेहतर नहीं है, और dependent types पर की गई कुछ आलोचनाओं से मैं सहमत भी हूँ
    अंततः दोनों भाषाओं ने अलग-अलग trade-off किए हैं, और उन्हीं चुनावों ने उन्हें अपने-अपने क्षेत्रों में काफ़ी प्रभावी tool बनाया है। proof का क्षेत्र इतना बड़ा है कि हर paradigm की अपनी ताकत और कमज़ोरी है, और Lean बस उसके किसी दूसरे हिस्से में specialized है
    Sledgehammer अच्छा है, लेकिन Lean में भी वैसा कुछ आना केवल समय की बात लगती है
    खोज के चरण में वह उपयोगी हो सकता है, लेकिन काफ़ी resource खाता है, और भले ही proof छोटा कर दे, मैं public code में आधे-जादुई by sledgehammer की तुलना में proof के पूरे चरणों का सीधे दिखना ज़्यादा पसंद करता हूँ
    दूसरी ओर Isabelle खुद विकसित करना Lean की तुलना में कहीं ज़्यादा तकलीफ़देह है, और खासकर डेवलपर्स के साथ संवाद करना तो और भी
    mailing list पर bug नहीं हैं, बस अनपेक्षित व्यवहार है जैसी मानसिकता बचकानी और गैर-पेशेवर लगी
    और Lean जैसे systems के RAM उपयोग का मज़ाक उड़ाना भी, Isabelle की अपनी memory gluttony देखकर, काफ़ी हास्यास्पद है

    • यहाँ समस्या यह है कि UNSAT certificate को जल्दी जाँचे जा सकने वाले रूप में बदलना बिल्कुल भी मामूली काम नहीं है
      व्यवहार में यह लगभग formal proof लिखने जितना ही कठिन है
    • आख़िरी बार जब देखा था, Isabelle/HOL interface के रूप में एक custom Emacs mode इस्तेमाल करता था
      हो सकता है मैं इसे किसी दूसरे HOL के साथ गड़बड़ा रहा हूँ
    • मुझे नहीं पता Sledgehammer क्या है, लेकिन विवरण से यह Mathlib के grind जैसा ही tool लगता है
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • Lean में दिलचस्प बात यह है कि Lean एक language है, लेकिन लोग जिस चीज़ की सबसे ज़्यादा चर्चा करते हैं वह वास्तव में Mathlib नाम की library है
    Mathlib बनाने वाले लोग काफ़ी व्यावहारिक लगते हैं, इसलिए वे शायद Lean types के भीतर classical logic डालते हैं और intuitionistic logic का उपयोग केवल कुछ हिस्सों में करते हैं

    • law of excluded middle को समझाने के लिए दिया गया उदाहरण गलत था
      "कोई चीज़ एक ही समय में true और false नहीं हो सकती" यह excluded middle नहीं बल्कि law of noncontradiction है
      excluded middle का अर्थ है p true है या not p true है
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • computer science वाली तरफ अब लोग अपनी CSLib बना रहे हैं
      https://www.cslib.io https://www.github.com/leanprover/cslib
      intuitionistic logic का मतलब मूलतः गणितीय तर्कों को computable constructions में बदलना है, इसलिए यह देखना रोचक होगा कि वे इस मुद्दे को कैसे संभालते हैं
      सच तो यह है कि जैसे ही आप Lean में algorithm लिखते हैं, आप किसी न किसी रूप में constructive constraints के भीतर आ ही जाते हैं, और उस उद्देश्य के लिए शायद इतनी logic ही काफ़ी हो
    • constructive mathematics को स्वीकार करने के पाँच चरण वाला मज़ाक याद आ गया
      denial, anger, bargaining, depression, acceptance
      Andrej Bauer की इस विषय पर talks और लेख भी देखने लायक हैं
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • यहाँ intuitive logic नहीं, intuitionistic logic होना चाहिए
    • इतनी पाबंदियों और रुकावटों के बावजूद, कब और क्यों कोई intuitionistic logic को प्राथमिकता देता है, यह जानने में दिलचस्पी है

  • मुझे लगता है ऐसी और पोस्टें होनी चाहिए
    उस groupthink के खिलाफ़ भी, जहाँ सब मान लेते हैं कि बस X इस्तेमाल करो, कम-से-कम विकल्पों की जाँच करने के लिए हमेशा कुछ न कुछ ठोस कारण होते हैं
    अंत में अगर मुख्यधारा का विकल्प ही चुनना हो, तब भी स्थिति को समझकर चुनना बेहतर है

    • मैं पूरी तरह सहमत नहीं हूँ
      अभी भी हम frameworks और alternatives बहुत ज़्यादा बना रहे हैं, और शायद इसलिए भी कि यह मज़ेदार लगता है
      मौजूदा tools को सुधारने या बस वास्तविक काम आगे बढ़ाने के बजाय, लोग language, library और build tool की संख्या अंतहीन बढ़ाते जाते हैं
      मेरे हिसाब से अगर language, library और build tool अभी की तुलना में आधे होते, तो शायद बेहतर होता
    • अंततः यह स्थिति पर निर्भर करता है
      जितना आप मुख्यधारा से दूर जाते हैं, उतना documentation कम होता जाता है, कम खोजे गए कोनों के कारण bugs बढ़ते हैं, और मदद करने वाले लोग घटते जाते हैं
      जब विकल्प बीस से ऊपर पहुँच जाएँ, तो औसतन standard option चुनकर आगे बढ़ जाना सही है। ध्यान सीमित होता है; अगर हर dependency पर जाँच-रिपोर्ट लिखने लगें, तो मुख्य समस्या ही नहीं सुलझेगी
      अपवाद दो हैं: या तो standard tool मेरे use case पर सचमुच फिट नहीं बैठता, या फिर standard tool खुद उसी मुख्य समस्या से गहराई से जुड़ा है जिसे मैं हल करना चाहता हूँ

  • यह चर्चा मुझे Python की scientific computing सीमाओं की ओर इशारा करने वाले लेखों जैसी लगती है
    जब किसी ठीक-ठाक tool के आसपास community critical mass पार कर लेती है, तो वह बाकी अधिकांश कारकों पर भारी पड़ती है
    momentum बनता है, tutorials, explainers और बेहतर documentation जमा होते जाते हैं, और चीज़ लगभग escape velocity तक पहुँच जाती है
    Lean अभी ठीक उसी जगह पर दिखता है, खासकर क्योंकि उसके पास Terrance Tao जैसे मज़बूत समर्थक भी हैं
    इसलिए "language X बेहतर है" कहना पूरी तरह गलत नहीं, लेकिन इससे असली महत्वपूर्ण सवाल छूट सकता है
    असली प्रश्न यह है कि क्या वह उस tool से वास्तव में बेहतर है जिसे सब जानते हैं, तुरंत इस्तेमाल कर सकते हैं, और जिसके सुधार पर अधिक समय लगाया जा रहा है
    आख़िरकार यह worse is better या फिर अच्छा और लोकप्रिय होना ही पर्याप्त होने जैसी स्थिति लगती है

    • अलग-अलग formal systems के बीच translation को LLM काफ़ी प्रभावी बना सकते हैं, यह एक अच्छा बिंदु है
      खासकर इसलिए कि इस क्षेत्र में translation के नतीजों का काफ़ी हिस्सा automatically verify किया जा सकता है, इसलिए चुनाव उतना बड़ा मुद्दा नहीं भी हो सकता
    • लेकिन AI युग में critical mass का महत्व बहुत कम हो जाता है
      AI बिना किसी विशाल community library के भी खुद code लिख सकती है, और इंटरनेट पर लाख ट्यूटोरियल न हों तब भी documentation और specs पढ़ सकती है
      ऐसी language से बचने की ज़रूरत भी नहीं जिसमें job market न हो। AI करियर नहीं बना रही होती, उसे बस अभी का काम करना होता है
      इसलिए पहले जिन छोटी languages और DSLs के पास मौका नहीं था, उनके अपनाए जाने की संभावना बढ़ जाती है
      प्रोग्रामिंग में लंबे समय से चली आ रही language monoculture को भी AI खत्म कर सकती है

  • "आज लगभग जो कुछ भी किसी system में formalize किया गया है, वह AUTOMATH में भी formalize किया जा सकता था" कहना कुछ वैसा ही है जैसे कहना कि आज जो कुछ modern languages में लिखा जाता है, वह 50 साल पहले की assembly में भी लिखा जा सकता था
    तकनीकी रूप से सही हो सकता है, लेकिन आर्थिक रूप से बिल्कुल अलग बात है

    • assembly language आम तौर पर Turing-complete होती है, लेकिन proof engines की दुनिया में उसके अनुरूप सही तुलना क्या होगी, यह मुझे स्पष्ट नहीं है

  • लगभग 15 साल पहले मैंने Coq/Rocq और कुछ दूसरे tools को छूकर देखने की कोशिश की थी, लेकिन concepts से भी ज़्यादा software खुद समझना बेहद कठिन लगा
    proof assistant / interactive theorem prover की अजीब बात यह है कि उसकी interactive प्रकृति के कारण वह language और IDE के संयुक्त रूप में बदल जाता है, और व्यवहार में दोनों काफ़ी कसकर जुड़े होते हैं
    इसलिए सिर्फ language की अलग से बात करना मुश्किल है; यह भी देखना पड़ता है कि उसे किस environment में इस्तेमाल किया जाता है
    मैं खुद भी VS Code का जबरदस्त प्रशंसक नहीं हूँ, लेकिन यह साफ़ है कि बहुत-से लोगों द्वारा इस्तेमाल किया गया, बड़े निवेश से तराशा गया extensible IDE विकल्पों के environment से बहुत आगे है
    Natural Numbers Game जैसे बेहतरीन onboarding paths भी शायद VS Code की hackability और ecosystem की वजह से ही संभव हुए हैं
    हालाँकि Lean सीखते हुए मेरी चिंता यह है कि syntax extensibility दोधारी तलवार है
    भाषा सीख लेने के बाद आप उसी भाषा में लिखा code पढ़ना चाहते हैं, लेकिन अगर हर project अपना DSL ढेरों बनाने लगे, तो हालात काबू से बाहर जा सकते हैं
    अंत में यह सब इस बात पर निर्भर करेगा कि community और ecosystem कितनी संयमित रहती है, इसलिए मैं इसे उम्मीद और चिंता दोनों के साथ देख रहा हूँ

  • Lean न तो गणितज्ञों का सबसे प्रिय proof assistant है, न ही software formal verification के लिए सबसे उपयुक्त tool
    लेकिन यह दोनों काम किसी-न-किसी हद तक कर लेता है, और बदले में उसने वह momentum हासिल कर लिया है जिसे पाना सबसे कठिन होता है
    और AI युग में, सार्वजनिक रूप से उपलब्ध मानव-लिखित code की मात्रा सीधे इस बात को प्रभावित करती है कि agents नया code कितना अच्छी तरह बना पाते हैं, इसलिए यह momentum और भी मज़बूत हो जाता है