सिर्फ Lean ही क्यों नहीं इस्तेमाल करते?
(lawrencecpaulson.github.io)- गणितीय औपचारिककरण का इतिहास Lean से शुरू नहीं हुआ, और लगभग 60 साल पहले से कई अलग परंपराओं के सिस्टम मुख्य तकनीकों और उपलब्धियों को पहले ही संचित कर चुके थे
- 1968 का AUTOMATH, LCF परिवार, HOL, Rocq, ACL2, Mizar जैसे टूल्स ने real analysis से लेकर prime number theorem, four color theorem, और Kepler conjecture तक व्यापक औपचारिककरण किए हैं
- Lean ने बड़ी library और सक्रिय community के आधार पर आधुनिक गणित की परिभाषाएँ तेज़ी से खड़ी कीं, लेकिन propositions as types या dependent types ही proof assistant का एकमात्र रास्ता नहीं हैं
- Isabelle मज़बूत automation, उच्च पठनीयता, और dependent types से बचाव को अपनी ताकत बताता है, और proof object के बिना भी kernel की abstraction barrier के ज़रिए proof checking बनाने वाली LCF परंपरा को आगे बढ़ाता है
- AI structured proofs को व्यवस्थित करने और दूसरे सिस्टमों में अनुवाद करने की दिशा भी जोड़ रहा है, इसलिए आगे चलकर किसी एक टूल को ही अंतिम मानक मानने का दबाव और कम हो सकता है
शुरुआती सिस्टम और अन्य परंपराएँ
-
AUTOMATH
- AUTOMATH में 1968 में ही गणितीय औपचारिककरण के लिए ज़रूरी लगभग सभी तत्व मौजूद थे
- 1977 में Jutting ने AUTOMATH में Landau की Foundations of Analysis का औपचारिककरण किया, और pure logic से शुरू करके complex numbers के निर्माण तक पहुँचे
- इसमें equivalence classes और rational number sets का उपयोग किया गया, और real line की Dedekind completeness भी औपचारिक रूप से सिद्ध की गई
- यह उपलब्धि 20 साल तक दोबारा नहीं आई, और 1990 के दशक के मध्य में जाकर John Harrison के HOL Light और Jacques Fleuriot के Isabelle/HOL में फिर से real numbers का औपचारिककरण हुआ
- notation बहुत असुविधाजनक थी और automation बिल्कुल नहीं था, इसलिए proofs लंबे और पढ़ने में कठिन थे
- फिर भी equivalence classes को संभालने में इसे Rocq से बेहतर माना गया है; Rocq उपयोगकर्ताओं के 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 जैसे गहरे परिणामों के औपचारिककरण में भी इसका उपयोग हुआ
- इसकी वर्तमान परंपरा ACL2 मुख्यतः hardware verification में लागू होती है
LCF के बाद की धारा
- Edinburgh LCF programming language theory पर केंद्रित था, लेकिन proof assistant की meta-language के रूप में functional language रखने का विचार व्यापक हो गया
- Cambridge, INRIA, Cornell सहित कई समूहों ने ML का उपयोग करके शुरुआती HOL, Coq (अब Rocq), और Nuprl जैसे टूल बनाए
- HOL समूह hardware verification पर केंद्रित था, लेकिन floating-point hardware verification के कारण real analysis की ज़रूरत पड़ी
- John Harrison ने Cauchy integral formula के माध्यम से prime number theorem जैसे गंभीर गणितीय परिणाम HOL परिवार में सिद्ध किए
- 100 theorems में जितना संभव हो सके उतने प्रमेयों को verify करने के लक्ष्य के तहत HOL Light अक्सर शीर्ष स्थानों पर रहा
- 2014 तक इस परिवार के सिस्टम कई उन्नत प्रमेयों का औपचारिककरण कर चुके थे
- four color theorem
- odd order theorem
- axiom of choice की relative consistency
- Gödel का second incompleteness theorem
- Tom Hales का Kepler conjecture
- ये प्रमेय आम तौर पर लंबे और जटिल proofs वाले थे, औपचारिककरण का काम भी बहुत बड़े पैमाने का था, और इन्होंने प्रमेयों में बचे संदेह को कम करने में महत्वपूर्ण भूमिका निभाई
Lean community का उभार
- गणितज्ञों का मानना था कि पहले के औपचारिककरण Grothendieck schemes या perfectoid spaces जैसी मुख्यधारा की आधुनिक गणित की परिष्कृत संरचनाओं तक नहीं पहुँचे थे
- Tom Hales ने ऐसी परिभाषाओं को library के रूप में जमा करने की दिशा चुनी, और proofs से अधिक परिभाषाओं के संचय पर ध्यान देते हुए Lean को चुना
- उन्होंने Big Proof कार्यक्रम में यह दिशा प्रस्तुत की, और इसी तरह की योजनाएँ भी साथ में चर्चा में आईं
- Kevin Buzzard ने यह सुनकर शिक्षा में Lean आज़माने का निर्णय लिया, जिसके बाद इसका प्रसार तेज़ हो गया
- Lean community के एक महत्वपूर्ण मोड़ के रूप में, Rocq पर लंबे समय तक हावी रही constructive proof के प्रति आसक्ति से बाहर निकलना बताया गया
- intuitionism Russell के paradox के बाद उभरा था, और real numbers की अवधारणा पर भी इसके विशेष निहितार्थ थे
- Martin-Löf type theory स्पष्ट रूप से intuitionistic formalism है, लेकिन लिखा गया है कि Rocq को इतनी सरलता से नहीं देखा जा सकता
- फिर भी Rocq से जुड़े पेपर्स में constructive proof बार-बार वहाँ भी सामने आया जहाँ वह अप्रासंगिक या अर्थहीन था, और यह प्रवृत्ति Rocq के गणितीय उपयोग में बाधा बनकर उसकी जगह Lean को देने लगी
propositions as types और LCF का अंतर
- Propositions as types logical symbols ∀, ∃, →, ∧, ∨ और type constructors Π, Σ, →, ×, + के बीच की द्वैतता है
- यह ढाँचा सुंदर और सैद्धांतिक रूप से उत्पादक है, लेकिन यही एकमात्र रास्ता नहीं है
- यदि proof assistant को propositions as types सिद्धांत के आधार पर proofs जाँचने वाले 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 में propositions का sort Prop मौजूद है, जहाँ एक ही proposition के सभी proof objects एक ही value माने जाते हैं, जिससे proof irrelevance मिलती है
- फिर भी इससे विशाल proof objects गायब नहीं हो जाते; वे वास्तविक सिस्टम में बने रहते हैं
- Robin Milner की मुख्य खोज यह थी कि LCF में proof object की खुद आवश्यकता नहीं होती
- यदि proof kernel को ML के abstract data type के भीतर रखा जाए, और inference rules को constructors बनाया जाए, तो proofs को dynamic रूप से जाँचा जा सकता है
- ML की abstraction barrier के कारण cheating असंभव मानी जाती है
- ऐसे विशाल terms जो कुछ भी निर्देशित नहीं करते, फिर भी दर्जनों MB घेर लेते हैं, RAMmageddon के युग में विशेष रूप से अव्यावहारिक लगते हैं
- ऐसे अनावश्यक terms को और अधिक सुंदर बनाने वाले शोध की दिशा की भी आलोचना की गई है
Isabelle चुनने के कारण
- यदि सहकर्मी Lean का उपयोग करते हों, टीम की विशेषज्ञता भी Lean में हो, और ज़रूरी prerequisite library भी Lean में हो, तो Lean चुनना स्वाभाविक है
- लेकिन यदि स्वतंत्र रूप से चुनने की गुंजाइश हो, तो Isabelle पर विचार करने के स्पष्ट कारण हैं
-
automation
- इसे सबसे शक्तिशाली automation की ताकत के रूप में पेश किया गया है; सामान्य “hammer” टूल्स की तुलना में भी sledgehammer का मुकाबला मुश्किल माना गया है
- computer algebra की दिशा को भी अलग से महत्वपूर्ण बताया गया है
-
पठनीयता
- इसे पठनीयता के लिहाज़ से सर्वोत्तम विकल्प कहा गया है, और Isar के उदाहरणों को आधार बनाया गया है
-
dependent types से बचाव
- dependent types न होने के कारण universe level और शुरुआती उपयोगकर्ताओं को परेशान करने वाली कई विचित्रताओं से बचा जा सकता है
- लिखा गया है कि Lean की mathlib और Rocq की SSReflect, Mathematical Components में भी dependent types के उपयोग की सिफारिश नहीं की जाती
- dependent types की मुख्य कठिनाई यह है कि यदि इन्हें ठीक से लागू किया जाए तो type checking स्वयं undecidable हो जाती है
- इसका कारण equality decision का undecidable होना है, और शुरुआती दौर में इसे स्वाभाविक माना जाता था
- लगभग 1990 के बाद type checking को decidable बनाने के लिए equality को definitional/intensional equality तक घटाने की दिशा में सहमति बनी
- इसके परिणामस्वरूप (T(N+1)) और (T(1+N)) अलग-अलग types बन जाते हैं
- ऐसी सीमाएँ वास्तविक proofs को भी प्रभावित करती हैं, और definitional equality checking स्वयं अब भी computationally expensive है
dependent types के बिना भी आधुनिक गणित
- लिखा गया है कि 2017 तक यह आकलन कहीं अधिक सावधान था कि Isabelle किस स्तर के गणित को संभाल सकता है
- उस समय ऐसा लग सकता था कि निम्नलिखित विषयों के लिए dependent types अनिवार्य हैं
- लेकिन Alexandria से जुड़े शोध से बहुत कुछ सीखा गया, और निष्कर्ष यह निकला कि मुख्य बात हर चीज़ को types में ठूँसना नहीं है
आगे की दिशा और AI
- Lean कई बातों में सही दिशा में है, और nested proof blocks का समर्थन भी करता है, इसलिए संभावित रूप से यह पर्याप्त रूप से पठनीय proof language बन सकता है
- अब Lean community को इन सुविधाओं का वास्तव में उपयोग करना चाहिए, जबकि Isabelle उपयोगकर्ता ऐसा पहले से बड़े पैमाने पर करते आए हैं
- computer-checkable proof objects की तुलना में मनुष्यों द्वारा वास्तव में पढ़े जा सकने वाले proof text की transparency अधिक महत्वपूर्ण है
- AI का उभार इस अंतर को और अधिक स्पष्ट बना रहा है
- AI द्वारा बने proofs अक्सर अव्यवस्थित होते हैं, लेकिन उन्हें sledgehammer से व्यवस्थित करना आसान होता है, और यदि संरचना अच्छी हो तो अत्यधिक विवरण के बावजूद वे पढ़े जा सकते हैं
- इससे प्रगति की धारा को समझना और proofs को अधिक सरल रूप में घटाना आसान हो जाता है
- हाल में ऐसे शोध भी आए हैं जहाँ language model सीधे sledgehammer को call करता है
- AI एक proof assistant से दूसरे proof assistant में पढ़ने योग्य structured proofs का अनुवाद भी आसानी से कर सकता है
- ऐसा होने पर कौन-सा सिस्टम चुना जाए, इस प्रश्न का दबाव स्वयं कम हो जाता है
Mizar की छूटी कड़ी की पूर्ति
- गणितीय औपचारिककरण का इतिहास Mizar और उसकी विशाल mathematics library के बिना पूरा नहीं हो सकता
- Isabelle की Isar language पर भी Mizar का गहरा प्रभाव रहा है
- Mizar को छोड़ देने की बात अलग से सुधारी गई है, और लिखा गया है कि अगली पोस्ट में Mizar पर चर्चा की जाएगी
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...
https://github.com/dharmatech/symbolism.lean
यह C# कोड का पोर्ट है, और Lean की expressiveness हैरान करने वाली है
कुछ समय पहले इसका थोड़ा शोर सुना था, लेकिन हाल में मैंने इस क्षेत्र को बारीकी से फॉलो नहीं किया है
और मुझे दो और बाधाएँ दिखती हैं। पहली, यह जानना ही मुश्किल है कि software को क्या करना चाहिए, और उपयोगकर्ता जो करना चाहता है वह ज़रूरी नहीं कि वही हो जिसके लिए ग्राहक पैसे देता है
दूसरी, कई डेवलपर्स के काम की गुणवत्ता इतनी कम होती है कि उनसे Java जैसी भाषा की तुलना में truth language को बेहतर संभालने की उम्मीद करना मुश्किल है
हालांकि दूसरी समस्या शायद उन AI systems के आने से कम हो जाए जो ज़रूरी सावधानी बरतते हों, और तब स्थिति बदल सकती है
मेरी नज़र में फ़ंक्शनल प्रोग्रामिंग भी, पहले से ही किनारे की गई गणित की तरह, अधिकांश प्रोग्रामरों के लिए बहुत कम प्रासंगिक है
लगता है कि लेखक ने 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 क्या था
LCF में proof और term अलग चीज़ें हैं, और मेरे हिसाब से मूलतः ऐसा ही होना चाहिए। इस तरह की Curry-Howard शैली की गड़बड़ी अनावश्यक है, लेकिन बहुत से लोग मानते हैं कि कंप्यूटर के साथ गणित करने का वही एकमात्र तरीका है
चाहें तो LCF में भी proofs को स्टोर और reuse किया जा सकता है, और Lean में भी चाहें तो optimization से उन्हें हटाया जा सकता है
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 बड़ी होने में दिखती है
यह समझ आता है कि वह आकर्षक क्यों है, लेकिन इसकी कीमत पर थोड़ी सुंदरता और ताकत कम हो गई लगती है
हालाँकि ऐसे प्रभाव उस समय स्थायी लग सकते हैं, लेकिन वास्तव में वे अक्सर उतने लंबे नहीं टिकते। अगर सच में वही सब कुछ होता, तो 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 भी उधर ले जा सकूँ
मुख्य बात perfect tool नहीं, बल्कि पर्याप्त अच्छे tool के साथ काम निकाल लेना है
Lean में इतने विकसित होने की गुंजाइश दिखती है कि वह सचमुच Haskell का उत्तराधिकारी बन सके, यानी software development के लिए एक functional language के रूप में
लगता है फ़र्क़ मुख्यतः tooling support में था। Agda का documentation कमज़ोर है, system पर install करके चलाना भी झंझट भरा है, और लगभग Emacs इस्तेमाल करने पर ज़ोर देता है
दूसरी ओर Lean के अपने documentation में
catutility लिखने तक का तरीका है, और कुल मिलाकर यह कहीं अधिक modern tooling experience देता हैआमतौर पर इसकी तारीफ़ 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 देखकर, काफ़ी हास्यास्पद है
व्यवहार में यह लगभग formal proof लिखने जितना ही कठिन है
हो सकता है मैं इसे किसी दूसरे HOL के साथ गड़बड़ा रहा हूँ
grindजैसा ही tool लगता हैhttps://leanprover-community.github.io/mathlib4_docs/Init/Gr...
Lean में दिलचस्प बात यह है कि Lean एक language है, लेकिन लोग जिस चीज़ की सबसे ज़्यादा चर्चा करते हैं वह वास्तव में Mathlib नाम की library है
Mathlib बनाने वाले लोग काफ़ी व्यावहारिक लगते हैं, इसलिए वे शायद Lean types के भीतर classical logic डालते हैं और intuitionistic logic का उपयोग केवल कुछ हिस्सों में करते हैं
"कोई चीज़ एक ही समय में true और false नहीं हो सकती" यह excluded middle नहीं बल्कि law of noncontradiction है
excluded middle का अर्थ है
ptrue है याnot ptrue हैhttps://en.wikipedia.org/wiki/Law_of_noncontradiction
https://www.cslib.io https://www.github.com/leanprover/cslib
intuitionistic logic का मतलब मूलतः गणितीय तर्कों को computable constructions में बदलना है, इसलिए यह देखना रोचक होगा कि वे इस मुद्दे को कैसे संभालते हैं
सच तो यह है कि जैसे ही आप Lean में algorithm लिखते हैं, आप किसी न किसी रूप में constructive constraints के भीतर आ ही जाते हैं, और उस उद्देश्य के लिए शायद इतनी logic ही काफ़ी हो
denial, anger, bargaining, depression, acceptance
Andrej Bauer की इस विषय पर talks और लेख भी देखने लायक हैं
https://www.youtube.com/watch?v=21qPOReu4FI
http://dx.doi.org/10.1090/bull/1556
मुझे लगता है ऐसी और पोस्टें होनी चाहिए
उस 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 या फिर अच्छा और लोकप्रिय होना ही पर्याप्त होने जैसी स्थिति लगती है
खासकर इसलिए कि इस क्षेत्र में translation के नतीजों का काफ़ी हिस्सा automatically verify किया जा सकता है, इसलिए चुनाव उतना बड़ा मुद्दा नहीं भी हो सकता
AI बिना किसी विशाल community library के भी खुद code लिख सकती है, और इंटरनेट पर लाख ट्यूटोरियल न हों तब भी documentation और specs पढ़ सकती है
ऐसी language से बचने की ज़रूरत भी नहीं जिसमें job market न हो। AI करियर नहीं बना रही होती, उसे बस अभी का काम करना होता है
इसलिए पहले जिन छोटी languages और DSLs के पास मौका नहीं था, उनके अपनाए जाने की संभावना बढ़ जाती है
प्रोग्रामिंग में लंबे समय से चली आ रही language monoculture को भी AI खत्म कर सकती है
"आज लगभग जो कुछ भी किसी system में formalize किया गया है, वह AUTOMATH में भी formalize किया जा सकता था" कहना कुछ वैसा ही है जैसे कहना कि आज जो कुछ modern languages में लिखा जाता है, वह 50 साल पहले की assembly में भी लिखा जा सकता था
तकनीकी रूप से सही हो सकता है, लेकिन आर्थिक रूप से बिल्कुल अलग बात है
लगभग 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 और भी मज़बूत हो जाता है