Analysis I का Lean companion
(terrytao.wordpress.com)- Terence Tao ने real analysis की पाठ्यपुस्तक Analysis I की definitions, theorems और exercises को Lean code में बदलने के लिए एक companion repository शुरू की है
- natural numbers, integers, rationals, reals की रचना और set theory व logic को कड़ाई से संभालने वाली इस किताब की प्रकृति के कारण, यह proof assistant के साथ सीखने के लिए अच्छी संरचना देती है
- अभी दायरा Chapter 2 के कुछ हिस्सों, 3.1 basic set theory, और 4.1 integers तक है, और Mathlib natural numbers के साथ isomorphism भी शामिल है
- code Lean में compile होता है, लेकिन कई
sorryअभी बाकी हैं, और आधिकारिक solutions के बजाय fork में उन्हें भरने का तरीका सुझाया गया है - यह सामग्री exercises को Lean में हल करने का एक वैकल्पिक रास्ता होने के साथ-साथ, आगे बढ़ने पर Mathlib के उपयोग को सीखने के लिए एक शुरुआती संसाधन की तरह भी काम कर सकती है
Analysis I को Lean में ले जाने की परियोजना
- Lean companion to “Analysis I” Analysis I की कई definitions, theorems और exercises को Lean में “translate” करने की परियोजना है
- किताब के exercises को Lean code में संबंधित
sorryभरकर भी हल किया जा सकता है - आधिकारिक exercise solutions को companion में host करने की योजना नहीं है, और
sorryभरा हुआ version repository के fork के रूप में बनाया जा सकता है
किताब और Lean एक-दूसरे के लिए उपयुक्त क्यों हैं
- Analysis I एक ऐसी किताब है जो पारंपरिक real analysis textbooks को पूरक बनाने के लिए बुनियादी मुद्दों पर अधिक ध्यान देती है
- natural numbers, integers, rationals, reals की construction
- set theory और logic, ताकि उच्च स्तर की rigor के साथ proofs विकसित किए जा सकें
- किताब लिखे जाने के समय Coq और Agda जैसे proof assistants पहले से मौजूद थे, लेकिन उस समय formal verification मुख्य रुचि का विषय नहीं था
- बाद में formal verification का अनुभव मिलने पर यह स्पष्ट हुआ कि किताब की सामग्री proof assistant के साथ अच्छी तरह मेल खाती है
- किताब में standard number systems बनाते समय जिस naive type theory का परोक्ष उपयोग किया गया था, वह Lean की dependent type theory के साथ अच्छी तरह मेल खाती है
- Lean का quotient type support भी किताब की construction शैली के साथ फिट बैठता है
अभी तक Lean में बदला गया दायरा
- फिलहाल निम्नलिखित sections को Lean में translate किया गया है
Mathlib के साथ संबंध
- formalization को इस तरह डिज़ाइन किया गया है कि कुछ जगहों पर यह standard Lean mathematics library Mathlib से अलग चलता है, और अन्य जगहों पर Mathlib पर निर्भर रहता है
- Mathlib में standard natural numbers की अवधारणा पहले से मौजूद है
- Lean formalization में पहले
Chapter2.Natनाम से natural numbers को “हाथ से” फिर से बनाया जाता हैChapter2namespace में काम करने पर इसेNatके रूप में इस्तेमाल किया जा सकता है- natural numbers से जुड़ी Mathlib की सहायक प्रमेयों के समानांतर बुनियादी परिणाम स्थापित किए जाते हैं
- इनमें से कई proofs पाठकों के exercises के रूप में छोड़े गए हैं और अभी
sorryसे बदले गए हैं
- epilogue section में इस वैकल्पिक natural number system और Mathlib natural numbers के बीच isomorphism स्थापित किया जाता है
- अधिक सटीक रूप से, वह isomorphism भी एक exercise के रूप में रखा गया है
- इसके बाद Chapter 2 की natural number construction का आगे उपयोग नहीं किया जाता, और Mathlib natural numbers का उपयोग किया जाता है
- योजना यह है कि किताब के आगे के chapters में शुरुआती chapters की अपनी constructions की तुलना में Mathlib definitions और functions पर और अधिक निर्भरता बढ़ती जाए
उपयोग का तरीका और verification की स्थिति
- repository का code Lean में compile होता है
- लेकिन code के भीतर मौजूद कई
sorryवास्तव में सभी भरे जा सकते हैं या नहीं, यह अभी परीक्षणित नहीं है - यह भी जांचना बाकी है कि ज़रूरी सहायक प्रमेय या Lean files का API पर्याप्त है या नहीं
- लक्ष्य यह देखना है कि क्या कठिन Lean programming techniques पर निर्भर हुए बिना, वैचारिक रूप से स्वाभाविक तरीके से
sorryभरे जा सकते हैं
- लक्ष्य यह देखना है कि क्या कठिन Lean programming techniques पर निर्भर हुए बिना, वैचारिक रूप से स्वाभाविक तरीके से
- अपेक्षा है कि स्वयंसेवक इस companion को playtest करें और देखें कि exercises वास्तव में Lean में हल किए जा सकते हैं या नहीं
- अन्य feedback का भी स्वागत है
Lean·Mathlib परिचय सामग्री के रूप में इसका स्वरूप
- यह companion सिर्फ real analysis के लिए नहीं, बल्कि Lean और Mathlib के परिचय के लिए भी उपयोगी हो सकता है
- इस अर्थ में यह Natural number game से कुछ हद तक मिलता-जुलता है
- Natural number game का विषयगत overlap Analysis I के Chapter 2 के साथ काफी अधिक है
1 टिप्पणियां
Hacker News की रायें
गणित को Lean से पढ़ाने में मुझे सबसे दिलचस्प बात तुरंत feedback लगती है। अगर छात्र का proof गलत है, तो वह बस compile नहीं होता
पहले feedback पाने के लिए TA, instructor या expert जैसे किसी व्यक्ति को देखना पड़ता था, लेकिन अब Lean compiler जल्दी feedback दे सकता है
आगे चलकर अच्छा होगा अगर Lean compiler भी Rust compiler की तरह code सुधारने के सुझाव दे और ज्यादा educational feedback दे; शायद इसके लिए dedicated LLM की जरूरत भी पड़ सकती है
पहले गणित पढ़ते समय assignment लेकर कागज पर तरह-तरह की कोशिशें करते हुए लंबे समय तक उस पर विचार करने का समय बहुत होता था, और वही प्रक्रिया concepts को भीतर तक बैठाने और नए ideas तक भी ले जाती थी
Lean इस्तेमाल करने पर क्या यह बस अंधाधुंध कोशिश करने, random तरीके से check करने और चीजें उगलते जाने जैसा नहीं हो सकता? Coq को कुछ बार छूने पर भी मेरी याद यही है कि मैं मुख्यतः इधर-उधर छेड़छाड़ करके कोशिशें करता रहा
reduce(r.num, r.denom) = reduce(a, b)cross_equals(a, b, r.num, r.denom)r.denom * a = r.num * bLLM का इस्तेमाल नहीं होता; VS Code extension के अंदर एक छोटा local model चल रहा है। उम्मीद है कि कभी वह छोटा local model इंसानों से कहीं ज्यादा ताकतवर हो जाएगा। ज्यादा जानकारी https://acornprover.org/docs/tutorial/proving-a-theorem/ पर है
सचमुच उत्साहित हूं। अच्छा होगा अगर इसे अलग repository में ले जाया जाए, ताकि इसे ढूंढना और दूसरों को भेजना आसान हो
मुझे मूल रूप से गणित में जिज्ञासा थी, और Tao की Analysis वह पहली textbook थी जिसने मुझे दिखाया कि programming करने वाला दिमाग जिस rigor की उम्मीद करता है, उस तरीके से गणित कैसे बनाया जाता है
बाद में मैंने Lean भी थोड़ा आजमाया और वह भी वैसा ही संतोषजनक लगा, लेकिन Mathlib गणितीय concepts सीखने के उद्देश्य से काफी जटिल थी। इसलिए book और tool के बीच एक bridge बनना अच्छा लग रहा है
analysis जैसे mainstream गणितीय विषयों में theorem proving को momentum मिलते देखना अच्छा है
programming language theory में, 2010s के मध्य तक tools काफी polished होने लगे थे, तब Winskel की The Formal Semantics of Programming Languages जैसी प्रमुख textbook को Isabelle में formally verified किया गया था। यह पूरी तरह 1:1 transcription नहीं है, लेकिन http://concrete-semantics.org इसका उदाहरण है
अगर theorem proving में रुचि है, तो व्यक्तिगत रूप से मुझे लगता है कि वह क्षेत्र कहीं ज्यादा आसान starting point है। क्योंकि analysis के theorems अपने आप में ही काफी कठिन होते हैं
structural induction करना, induction hypothesis लागू करके दिखाना कि invariant बना रहता है, और आगे बढ़ते जाना
मैंने बहुत ज्यादा theorem proving नहीं की है, न ही proof assistants में analysis जैसे “mathematical” proofs किए हैं, लेकिन अगर mathematical proofs बहुत अलग approach मांगते हैं, तो सोचता हूं कि दोनों के बीच skill transfer कितना होता होगा
Rocq की Software Foundations का भी जिक्र करना चाहूंगा। शायद इसका Lean port भी हो, लेकिन जब मैंने शुरुआती हिस्से follow किए थे, तो अनुभव काफी smooth था
mainstream “textbook” वाले approach और Mathlib के approach में फर्क का मूल्यांकन करना बहुत दिलचस्प होगा
आम तौर पर formalized mathematics libraries results को यथासंभव general रूप में बयान करती हैं और proof development को ज्यादा intuitive और elegant तरीके से refactor करना आसान बनाती हैं
refactoring आसान इसलिए होती है क्योंकि system हमेशा track करता है कि logically कौन-सी चीज किससे follow करती है। कागज और pen से काम करते समय यह नहीं होता, इसलिए rework के मौके अक्सर छूट जाते हैं
undergraduate course में Mathlib-style “maximum generality” version की real analysis पढ़ाना समझ में आता है या नहीं, यह भी स्वाभाविक सवाल है। जाहिर है, proof-based mathematics के दूसरे क्षेत्रों पर भी यही बात लागू होती है
वास्तव में जिन्होंने इसे आजमाया है, उन faculty का अनुभव भी मुझे इसी तरह का पता है। advanced students के लिए ठीक है, लेकिन average student के लिए class time बर्बाद होने की संभावना बड़ी है
मेरा bias शायद इस बात से आता है कि मैंने mathematical concepts papers से सीखे हैं
code बहुत बड़ा extra burden है, और अक्सर लगता है कि वह किसी style standard का पालन भी नहीं करता। यह बात मैं एक ऐसे व्यक्ति के रूप में कह रहा हूं जिसे ऐसे math papers भी पढ़ने पड़े जिन्हें incomprehensible कहा जाता था; code के लिए readability standards व्यवहार में लगभग नहीं होते, इसलिए वह 10 गुना खराब है
Terence Tao के अपने YouTube channel पर भी Lean इस्तेमाल करने के कुछ videos हैं। https://www.youtube.com/@TerenceTao27
विस्तार से नहीं जानता, लेकिन उन्हें LLM का इस्तेमाल करते या बिना इस्तेमाल किए काम करते देखना शानदार था
analysis जैसे foundational विषय के लिए यह बहुत अच्छा project और अच्छा approach लगता है
तुरंत दिमाग में आने वाली चिंताएं दो हैं। पहली, Mathlib के core analysis results filters concept का इस्तेमाल करके limits को general और unified तरीके से handle करते हैं। फिर भी कुछ results epsilon-delta form में specialized हैं। मुझे लगता है Tao की Analysis ज्यादा traditional epsilon-delta approach इस्तेमाल करेगी
दूसरी, Mathlib तेजी से बदलती है और अक्सर टूटती है। नाम बदलते हैं और refactoring लगातार होती रहती है, इसलिए downstream repository को निरंतर maintenance चाहिए
https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6
यह काफ़ी radical विचार है, लेकिन मुझे लगता है कि गणित शिक्षा का फोकस Mathematica जैसे computer algebra systems और Lean जैसे theorem provers बनाने पर होना चाहिए। Visualization और practical applications को भी मज़बूती से शामिल करना चाहिए
चरम रूप में यह ऐसा हो सकता है कि कागज़ पर गणित बिल्कुल न करते हुए भी Lean के अंदर सीखी गई हर चीज़ को prove किया जा सके
अभी की व्यवस्था अंतहीन हाथ से की जाने वाली calculations पर केंद्रित है, जो मुझे बहुत बेकार और उबाऊ लगती है, और इसी वजह से लोग गणित से नफ़रत करने लगते हैं
Lean की textbook, बढ़िया। लेकिन HoTT क्यों नहीं है?
“Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
https://news.ycombinator.com/item?id=43196452
इस हफ़्ते HN पर आई अतिरिक्त Lean सामग्री:
“100 theorems in Lean”
https://news.ycombinator.com/item?id=44075061
“Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean” https://news.ycombinator.com/item?id=44119725
सटीक motivation मेरे क्षेत्र से बाहर है, इसलिए नहीं जानता, लेकिन लगता है कि Agda इन ideas को formalize करने के लिए Lean से बेहतर तरीका है
इस साल के अंत में मौजूदा HoTT book का ज़्यादा modern update कहे जा सकने वाला एक नया textbook भी आने वाला है, और उसका Agda formalization भी है
https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
https://github.com/HoTT-Intro/Agda
HoTT किसी reasonable standard के रूप में स्वीकार किए जाने के करीब बिल्कुल नहीं है, और ज़्यादातर लोगों के लिए यह शुरुआत से ही अटकाने वाला विषय है
यह JavaScript framework developer से पूछने जैसा है कि उसने Elm या Haskell के लिए framework क्यों नहीं बनाया
HoTT theorem provers को इस्तेमाल में आसान बनाने पर बहुत कम काम हुआ है, और documentation भी कहीं ज़्यादा कमजोर है
HoTT के फायदे भी स्पष्ट नहीं हैं। ऐसा लगता है कि यह सिर्फ category theory के बहुत obscure constructions से निपटते समय काम कम करता है
Terrence Tao के पास analysis की कुछ textbooks हैं, और यह उनकी पहली book के लिए Lean companion material है। उनके पास type theory की textbook नहीं है, इसलिए higher type theory नहीं है। शुरू से ही करने का मकसद पूरी तरह अलग है
बहुत शानदार। Analysis I वह पहली “real” math textbook थी जिसे मैं, mathematician नहीं बल्कि engineer होते हुए, Rudin जैसी दूसरी books को कई बार आज़माने के बाद पूरी तरह follow करके solve कर सकता हूँ, ऐसा महसूस कर पाया
उम्मीद है कि Lean companion material इसे उन लोगों के लिए और accessible बनाएगा जो math और programming से परिचित हैं और rigorously सीखना चाहते हैं
पिछले कुछ वर्षों में Tao की Analysis I किताब को Lean में formalize करने की लगातार कोशिशें होती रही हैं, और कुछ लोग ठीक वही काम करना चाहते थे जो Tao अभी कर रहे हैं। अफसोस, ज़्यादातर प्रयास शुरुआती कुछ chapters से आगे नहीं बढ़ पाए, लेकिन उम्मीद है कि Tao और आगे तक जा पाएँगे
मैंने भी सोचा था कि इसे खुद करके देखूँ। वजह यह थी कि मेरे Analysis I commentary blog https://taoanalysis.wordpress.com/ पर हर exercise के formalized proof जोड़ना किताब के साथ चल रहे लोगों के लिए उपयोगी हो सकता था
मैंने इसे किताब के private Discord server पर भी पोस्ट किया था, लेकिन यहाँ भी मददगार लगेगा, इसलिए संबंधित resources साझा कर रहा हूँ
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 की किताब का अनुसरण नहीं करता, लेकिन यह Lean4 version का natural number game है, इसलिए chapter 2 से इसकी सामग्री बहुत मिलती-जुलती है
https://github.com/djvelleman/STG4/ — यह Lean4 set theory game है, इसलिए chapter 3 से मिलता-जुलता हो सकता है। हालांकि https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean में
import Mathlib.Data.Set.Basicदिखता है, इसलिए लगता है कि sets को नए सिरे से define कर axioms बनाने के बजाय Lean के sets import किए जा रहे हैं। यह approach Lean को set theory के बारे में “बहुत ज़्यादा” जानने देती है, जो इस उद्देश्य के लिए अच्छा नहीं हो सकताhttps://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — integers construct करने के लिए
https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean — ऊपर वाली ही file हो सकती है
https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean — rational numbers construct करने के लिए
https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — custom
Settype define करने का एक तरीका दिखाता है