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

• 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 में खास मज़ा है