Analysis I का Lean कंपैनियन

• यह Terence Tao द्वारा लिखित real analysis पाठ्यपुस्तक Analysis I की मुख्य सामग्री को Lean proof assistant में रूपांतरित करने वाला प्रोजेक्ट है
• इस प्रोजेक्ट की संरचना मूल संख्या प्रणालियों के निर्माण और proof logic जैसी बातों पर केंद्रित है, जो कठोरता पर जोर देने वाली मूल पुस्तक के लक्ष्य से अच्छी तरह मेल खाती है
• इसमें Mathlib standard library का उपयोग किया गया है, लेकिन साथ ही मुख्य अवधारणाओं को सीधे निर्मित करने और पाठकों के खुद proof करने के अभ्यास भी शामिल हैं
• इसमें Lean code के खाली स्थान (sorry) स्वयं भरकर अभ्यास किया जा सकता है, और आधिकारिक समाधान नहीं दिए जाते, बल्कि fork करके इसे आगे बढ़ाया जा सकता है
• यह Lean शुरुआती और real analysis सीखने वाले दोनों के लिए Mathlib और Lean के वास्तविक उपयोग का अनुभव करने का उपयोगी अवसर है

---

अवलोकन

• यह Terence Tao की real analysis पाठ्यपुस्तक "Analysis I" को Lean proof assistant tool के साथ पुनर्निर्मित करने वाला open source प्रोजेक्ट है
• यह पाठ्यपुस्तक अन्य analysis पुस्तकों की तुलना में natural numbers, integers, rational numbers, और real numbers के निर्माण की प्रक्रिया तथा उस प्रक्रिया में आवश्यक set theory और logical tools पर अधिक ध्यान देती है
• पुस्तक का बड़ा हिस्सा व्यवस्थित कठोर proof क्षमता विकसित करने पर केंद्रित है, इसलिए इसकी संरचना Lean जैसे proof assistant के साथ अच्छी तरह मेल खाती है

Lean कंपैनियन प्रोजेक्ट की विशेषताएँ

• यह मूल पुस्तक की definitions, theorems, और exercises को Lean प्रारूप में "अनुवाद" करके उपलब्ध कराता है
• इन Lean files में exercises के समाधान से संबंधित कई खाली स्थान (sorry) शामिल हैं, जिन्हें पाठक स्वयं भरते हुए सीख सकते हैं
• आधिकारिक व्याख्या या समाधान उपलब्ध नहीं कराए जाते, लेकिन पाठक repository को fork करके अपने उत्तरों का संस्करण बना सकते हैं

Mathlib से जुड़ाव और भिन्नता

• Mathlib (Lean की standard mathematics library) में पहले से लागू अवधारणाओं (जैसे natural numbers) को जानबूझकर अलग से स्वयं बनवाया जाता है, और बाद में Mathlib संस्करण के साथ उसकी समरूपता (equivalence) को सिद्ध करने की प्रक्रिया भी शामिल है
• उदाहरण के तौर पर, Chapter2.Nat में Mathlib के natural numbers से अलग अपनी परिभाषा वाले natural numbers को शुरू से बनाया जाता है, मुख्य परिणामों को सीधे संभालने के बाद अंत में Lean में दोनों संस्करणों की समानता का अभ्यास कराया जाता है
• इसके बाद के अध्यायों से Mathlib की definitions और features का उपयोग धीरे-धीरे अधिक होता जाता है

सीखने और उपयोग के तरीके

• यह Lean कंपैनियन केवल analysis सीखने के लिए नहीं, बल्कि Lean और Mathlib में mathematics formalization कैसे की जाती है, इसकी प्रवेशिका के रूप में भी काम करता है
• "Natural number game" की तरह इसमें ऐसी संरचित exercises शामिल हैं, जिनमें Lean वातावरण में mathematical objects को सीधे परिभाषित और अभ्यास किया जा सकता है
• code स्वयं Lean में compile हो सकता है, लेकिन सभी exercises (sorry) वास्तव में हल किए जा सकते हैं या नहीं, इसका पूर्ण सत्यापन नहीं हुआ है; इस दृष्टि से playtesting और feedback की आवश्यकता है

ओपन सोर्स और योगदान

• repository open source है और कोई भी इसे देख, fork, और contribute कर सकता है
• आधिकारिक solutions अलग से उपलब्ध नहीं हैं, और कई तरह के समाधान संस्करण बनाने का समर्थन है
• 31 मई की स्थिति के अनुसार, प्रोजेक्ट को अलग स्वतंत्र repository में स्थानांतरित किया गया है

[GN⁺]

Hacker News राय

• मैं इस बात को लेकर सचमुच उत्साहित हूँ कि अगर यह प्रोजेक्ट एक स्वतंत्र repo में चला जाए, तो इसे दूसरों के साथ साझा करना और ढूँढ़ना कहीं आसान होगा। मुझे गणित को लेकर हमेशा जिज्ञासा रही है, और Tao की Analysis वह पहली पाठ्यपुस्तक थी जिसने मेरी programming सोच के अनुकूल तरीके से दिखाया कि कठोर गणित कैसे निर्मित किया जाता है। बाद में मैं Lean में भी काफ़ी रुचि लेने लगा, लेकिन Mathlib के ज़रिए गणितीय अवधारणाएँ सीखना मुझे थोड़ा जटिल लगा। इसलिए यह प्रोजेक्ट, जो किताब से टूल तक पुल का काम करता है, मुझे वास्तव में बहुत पसंद है।

  • मेरा अनुभव भी कुछ ऐसा ही रहा। मैंने convergence, Cauchy sequence वगैरह इसी से सीखे, और यह भी याद है कि यह किताब भारत में Hindustan Book Agency नामक एक non-profit publisher से प्रकाशित हुई थी, इसलिए यह बहुत सस्ते में मिल गई थी।

• Lean का उपयोग करके गणित शिक्षा में मुझे सबसे रोमांचक बात यह लगती है कि यह तुरंत feedback देता है। अगर छात्र का proof ग़लत है, तो वह compile ही नहीं होगा। पहले यह feedback किसी TA या professor को देना पड़ता था, लेकिन अब Lean compiler तेज़ी से बता देता है। आगे चलकर काश इसमें Rust compiler की तरह और भी मददगार सुधार-सुझाव देने की सुविधा आ जाए (इसके लिए शायद dedicated LLM की ज़रूरत पड़े)।

  • मैं लगभग पूरी तरह सहमत हूँ, लेकिन proof पर विचार करने की प्रक्रिया भी महत्वपूर्ण है। मेरा गणित का अनुभव काफ़ी पुराना है, लेकिन assignments या problems को कागज़ पर लिखकर धीरे-धीरे सोचने के बहुत से ऐसे पल थे जो किसी "गणितीय स्वर्ग" जैसे लगते थे। Lean का उपयोग करने पर मुझे चिंता है कि कहीं यह बस random input डालते रहने या अपने-आप सही होने तक कोशिश करते रहने जैसी "हाथ चलाने वाली" प्रक्रिया न बन जाए। मैंने पहले थोड़ी देर के लिए coq भी आज़माया था, और लगभग लगातार बस छेड़छाड़ ही करता रहा था। कुल मिलाकर, theorem solver कई मायनों में उपयोगी हैं, लेकिन मुझे चिंता है कि यह धीमे-धीमे चबाकर सोचने की प्रक्रिया ग़ायब हो सकती है, और उसके साथ internalization, conceptualization, तथा नए विचार आने के रास्ते भी कमज़ोर पड़ सकते हैं। इस बारे में आपका क्या विचार है, यह जानना चाहूँगा।

• यह भी बताया गया कि Terence Tao का एक व्यक्तिगत YouTube चैनल है जहाँ उन्हें सीधे Lean का उपयोग करते हुए देखा जा सकता है। मैं इस क्षेत्र का विशेषज्ञ नहीं हूँ, लेकिन उन्हें LLM के साथ या बिना काम करते देखना भी मुझे बेहद दिलचस्प लगा (https://www.youtube.com/@TerenceTao27)।

• पारंपरिक "पाठ्यपुस्तक-शैली" दृष्टिकोण की Mathlib शैली से तुलना करना वास्तव में बहुत दिलचस्प होगा। Formalized mathematics libraries आम तौर पर परिणामों को अधिकतम सामान्य रूप में व्यक्त करती हैं, और proof संरचना को refactor करके उसे सुंदर बनाना भी आसान होता है। Refactoring आसान है क्योंकि सिस्टम हमेशा logical dependencies को track करता रहता है, जबकि सिर्फ़ कागज़ और पेन के साथ ऐसा करना आसान नहीं होता। इसलिए यह स्वाभाविक सवाल है कि क्या Mathlib जैसी "अधिकतम सामान्यता" वाली analysis को university courses में पढ़ाना ठीक रहेगा। मेरा मानना है कि यह सवाल proof-आधारित गणित के लगभग हर क्षेत्र पर लागू होता है।

  • कम-से-कम शुरुआती course में तो यह उपयुक्त नहीं लगता। Curriculum में पहले से ही बहुत कुछ शामिल करना होता है — proof लिखना, programming करना, और foundational theory तक। जिन professors ने सच में इसे आज़माया है, उनका अनुभव भी कुछ ऐसा ही रहा है; advanced students के लिए यह अच्छा हो सकता है, लेकिन सामान्य students के लिए समय की बर्बादी साबित होता है।

  • मैं एक ऐसा गणितज्ञ हूँ जिसने लंबे समय तक programming भी की है, और मेरा मानना है कि कोई भी programmatic formalization बुनियादी समझ अपने-आप विकसित नहीं करेगी। मेरा यह पक्षपात शायद इसलिए भी है क्योंकि मैंने concepts papers पढ़कर सीखे हैं। Code अक्सर style की परवाह नहीं करता और readability के लिहाज़ से बहुत भारी पड़ता है; खराब लिखे papers भी मुश्किल होते हैं, लेकिन code तो standard के बिना 10 गुना ज़्यादा कठिन लग सकता है — यह मेरा निजी अनुभव है।

• यह देखकर अच्छा लगता है कि theorem proving को analysis जैसे mainstream गणितीय क्षेत्रों में भी धीरे-धीरे ध्यान मिल रहा है। PLT में पहले से ही Winskel की The Formal Semantics of Programming Languages जैसी प्रमुख पुस्तक का Isabelle में formal verification हुआ था (http://concrete-semantics.org)। अगर कोई theorem proving शुरू करना चाहता है, तो मुझे लगता है कि वह दिशा ज़्यादा आसान है और सिफ़ारिश करने लायक भी। साथ ही, analysis के theorem मूल रूप से काफ़ी कठिन होते हैं।

  • मुझे भी यह सुनकर हैरानी नहीं होगी कि PL proofs में entry barrier कम हो। अक्सर यह भी सुनने को मिलता है कि वहाँ बहुत कुछ routine जैसा होता है — structural induction, induction लगाना, invariants साबित करना, repeat करना, ऐसा flow। मैंने theorem proving बहुत ज़्यादा नहीं की है, लेकिन mathematical proofs (ख़ासकर analysis) theorem prover के साथ कभी नहीं किए। मैं जानना चाहता हूँ कि क्या "गणितीय" proofs के लिए बहुत अलग तरह का approach चाहिए होता है, और दोनों के बीच skill transfer कितना संभव है। संदर्भ के लिए, मैंने Software Foundations in Rocq (शायद इसका Lean port भी हो?) पढ़ा था और वह काफ़ी आनंददायक लगा।

• मुझे लगता है कि यह प्रोजेक्ट और इसका दृष्टिकोण analysis जैसे बुनियादी विषयों के लिए बहुत उपयुक्त है। लेकिन मुझे दो चिंताएँ हैं

  1. Mathlib में analysis के मुख्य परिणामों को filter की अवधारणा के ज़रिए एकीकृत रूप से संभाला जाता है, जबकि विशेष मामलों को epsilon-delta शैली में अलग से लिया जाता है। Tao की Analysis शायद अधिक पारंपरिक epsilon-delta दृष्टिकोण अपनाएगी।
  2. Mathlib बहुत तेज़ी से बदलने वाला प्रोजेक्ट है, इसलिए नाम और संरचना लगातार बदलते रहते हैं। Mapping information को लगातार maintain करना पड़ेगा।
  • लोगों को ख़ुद देखकर जाँचने के लिए कहा गया, और यह भी बताया गया कि sequence limits वाले अध्याय का अधिकांश हिस्सा sample pages के रूप में सार्वजनिक है, इसलिए संदर्भ के लिए यह लिंक साझा किया गया: https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6

• यह मुझे बहुत शानदार प्रोजेक्ट लगता है। Analysis I वह "वास्तविक" गणित की पाठ्यपुस्तक थी जिसे मैं, एक engineer होने के बावजूद, सच में शुरू से अंत तक पढ़ पाया था। मैंने दूसरी किताबों (जैसे Rudin) को कई बार पढ़ने की कोशिश की थी और असफल रहा था। अगर इसका Lean संस्करण हो, तो गणित और programming दोनों से परिचित लोग अवधारणाओं को और अधिक rigorously सीख सकेंगे — यह सोचकर उत्साह होता है।

• कई वर्षों से Tao की Analysis I की आधिकारिक Lean formalization की कोशिशें होती रही हैं, लेकिन वे हमेशा कुछ chapters से आगे बढ़ने में कठिनाई महसूस करती रही हैं। कुछ समय तक मैं ख़ुद भी यह प्रयास करना चाहता था — मेरा विचार था कि अगर Analysis I solutions blog (https://taoanalysis.wordpress.com/) के साथ formalized proofs भी जोड़े जाएँ, तो किताब से पढ़ने वाले लोगों के लिए यह उपयोगी होगा। मैंने पहले एक private Discord में इस विषय पर संकलित सामग्री साझा की थी, लेकिन यहाँ एक बार में कई उपयोगी reference Lean projects (github, gist, official docs आदि) के links साझा कर रहा हूँ:

  • https://github.com/cruhland/lean4-analysis
  • https://github.com/cruhland/lean4-axiomatic
  • https://github.com/Shaunticlair/tao-analysis-lean-practice
  • https://github.com/vltanh/lean4-analysis-tao
  • https://github.com/gabriel128/analysis_in_lean
  • https://github.com/mk12/analysis-i
  • https://github.com/melembroucarlitos/Tao_Analysis-LEAN
  • https://github.com/leanprover-community/NNG4/ (यह Tao की किताब नहीं है, बल्कि Natural Number Game का Lean4 संस्करण है, और इसका content Chapter 2 से लगभग मेल खाता है)
  • https://github.com/djvelleman/STG4/ (इसी तरह set theory game, जो Chapter 3 से मिलता-जुलता है; लेकिन Game/Metadata.lean में "import Mathlib.Data.Set.Basic" दिखता है, यानी यह set theory को पूरी तरह नए सिरे से परिभाषित करने के बजाय import करता है — इस स्थिति में Lean पहले से ही set theory को "जानता" है, इसलिए हमारे उद्देश्य के लिए यह पूरी तरह उपयुक्त न भी हो)
  • https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc (integers बनाने का उदाहरण)
  • https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean (यह शायद ऊपर वाली ही फ़ाइल हो सकती है)
  • https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean (rational numbers बनाने का उदाहरण)
  • https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality (custom Set type परिभाषित करने के लिए संदर्भ उदाहरण)

• मुझे जिज्ञासा है कि "Mathlib में संबंधित object के साथ isomorphism का proof" वास्तव में कितना महत्वपूर्ण है। क्या ऐसा हो सकता है कि isomorphism वाले हिस्से को हटा देने पर व्यवहार में कुछ भी न बदले? उदाहरण के लिए, क्या इसका उपयोग theorems को स्वतः translate करने जैसी किसी वास्तविक चीज़ में होता है?

  • ऐसे isomorphism proofs

    1. यह साबित करने देते हैं कि आपके बनाए object और Mathlib में पहले से मौजूद object वास्तव में समान हैं, ख़ासकर तब जब Mathlib की तरफ़ वे किसी जटिल generalized construction के रूप में परिभाषित किए गए हों, जिससे फ़र्क समझने में मदद मिलती है।
    2. Mathlib में उस object को पढ़ते या लिखते समय इस्तेमाल होने वाले औपचारिक notation और terminology को समझने में निर्णायक भूमिका निभाते हैं।

  • कम-से-कम इसका शैक्षिक मूल्य तो है। यह वह प्रक्रिया बनती है जिसमें आप ख़ुद को संतुष्ट करते हैं कि आपने जो set और operations बनाए हैं, वे किताब के अन्य हिस्सों में भी "वही" हैं।

• Lean-आधारित पाठ्यपुस्तकों का आना अच्छा लग रहा है, लेकिन HoTT (Homotopy Type Theory) क्यों नहीं है? "क्या Type Theory(HoTT) को (ZFC) set theory की जगह लेनी चाहिए" इस विषय पर एक लेख भी है (https://news.ycombinator.com/item?id=43196452)। इस हफ़्ते HN पर आए Lean से जुड़े कुछ अतिरिक्त community resources भी साझा किए गए — "100 theorems in Lean" (https://news.ycombinator.com/item?id=44075061), और DeepMind Lean project (https://news.ycombinator.com/item?id=44119725)।

  • लेकिन मुझे समझ नहीं आता कि HoTT की विशेष ज़रूरत ही क्यों होनी चाहिए। HoTT theorem provers अभी भी usability के मामले में काफ़ी कमज़ोर हैं, documentation भी पर्याप्त नहीं है, और HoTT से मिलने वाला वास्तविक लाभ भी स्पष्ट नहीं लगता। आम तौर पर यह तभी मायने रखता है जब आप category theory जैसी बेहद असामान्य संरचनाओं से निपट रहे हों।

  • चूँकि यह पारंपरिक पाठ्यपुस्तक वाला दृष्टिकोण है, इसलिए "यह HoTT क्यों नहीं है" इस प्रश्न का उत्तर तो इसमें पहले से ही निहित है। इसके अलावा, मुझे लगता है कि शिक्षण-प्रभावशीलता को लेकर संदेह रखने वाले विशेषज्ञ भी काफ़ी हैं।