साइंस के लिए AIमध्यमपाठ 2556 मिनट का पाठ

AI और गणित

Lean जैसे प्रूफ़ असिस्टेंट किसी प्रूफ़ के हर कदम की मशीन द्वारा जांच करते हैं। AI प्रूफ़ खोजने, पैटर्न पहचानने और कंजेक्चर सुझाने में मदद कर सकता है, और चेकर उसे सही बनाए रखता है।

✦ ट्यूटर से पूछें🧪 लैब · 25 min📝 पाठ का टेस्ट
पाठ वीडियो में

60 सेकंड में

AI और गणित

Lean जैसे प्रूफ़ असिस्टेंट किसी प्रूफ़ के हर कदम की मशीन द्वारा जांच करते हैं। AI प्रूफ़ खोजने, पैटर्न पहचानने और कंजेक्चर सुझाने में मदद कर सकता है, और चेकर उसे सही बनाए रखता है।

1/5
आसान शब्दों में
जब आप गणित का कोई सवाल हल करते हैं, तो आपके शिक्षक हर कदम की जांच करते हैं। क्या हो अगर कोई बहुत सख्त, बहुत धैर्यवान चेकर हर छोटे-से कदम को देखे और कभी थके ही नहीं? वही एक प्रूफ़ असिस्टेंट होता है। उसे इससे कोई फ़र्क नहीं पड़ता कि प्रूफ़ किसने लिखा है—किसी छात्र ने, किसी प्रोफ़ेसर ने या किसी AI ने। उसे बस इससे मतलब होता है कि क्या हर कदम सही है।

प्रूफ़, कंजेक्चर और जांच

गणित में, कंजेक्चर एक ऐसा कथन होता है जिसे लोग सच मानते हैं लेकिन उन्होंने उसे साबित नहीं किया होता है। एक प्रूफ़ तार्किक चरणों की एक श्रृंखला होती है जो दिखाती है कि इसे सच होना ही होगा। सिर्फ़ उदाहरण काफ़ी नहीं होते: कोई पैटर्न कई मामलों में सही बैठ सकता है और फिर ग़लत साबित हो सकता है।
n × n + n + 41 को देखिए। n = 0, 1, 2 और कई अन्य मानों के लिए, यह एक अभाज्य संख्या देता है। यह अंदाज़ा लगाना लुभावना लगता है कि यह "हमेशा अभाज्य" होगा। लेकिन n = 40 पर यह 1681 देता है, जो 41 × 41 है। एक काउंटर-एग्ज़ाम्पल पूरे पैटर्न को तोड़ देता है। लैब में आप इसे खुद देख सकते हैं।

प्रूफ़ असिस्टेंट क्या होता है

एक प्रूफ़ असिस्टेंट ऐसा सॉफ़्टवेयर होता है जहाँ आप गणित को एक सटीक भाषा में लिखते हैं, और कंप्यूटर हर कदम की जांच करता है। Lean एक व्यापक रूप से इस्तेमाल होने वाला प्रूफ़ असिस्टेंट है। इसके समुदाय ने फ़ॉर्मल गणित की एक बड़ी शेयर्ड लाइब्रेरी बनाई है जिसे mathlib कहा जाता है।
Two tiny statements checked by Lean 4lean
-- Lean checks that 2 + 2 really equals 4.
example : 2 + 2 = 4 := rfl

-- For every natural number n, n + 0 = n.
theorem add_zero_example (n : Nat) : n + 0 = n := rfl
अगर कोई कदम ग़लत होता है, तो Lean उस प्रूफ़ को स्वीकार करने से मना कर देता है। इससे जांच बहुत भरोसेमंद बन जाती है। हालांकि, यह सिर्फ़ उतना ही अच्छा है जितना कि वह कथन जो आपने लिखा था: अगर आप ग़लत प्रमेय (theorem) लिखते हैं, तो Lean खुशी-खुशी ग़लत चीज़ के प्रूफ़ की जांच कर देगा।

AI गणितज्ञों की कैसे मदद करता है

कार्यAI क्या करता हैक्या चीज़ इसे सही बनाए रखती है
प्रूफ़ खोजनाएक लैंग्वेज मॉडल Lean में प्रूफ़ का अगला कदम या पूरा प्रूफ़ सुझाता है।Lean इसकी जांच करता है। ग़लत कदम खारिज कर दिए जाते हैं।
लाइब्रेरी में खोजनाAI एक बड़ी लाइब्रेरी में ऐसा लेम्मा खोजने में मदद करता है जो मौजूदा कदम में फ़िट बैठता हो।कदम का जांच में खरा उतरना फिर भी ज़रूरी है।
पैटर्न पहचाननामशीन लर्निंग ढेर सारे गणितीय डेटा को देखती है और ऐसे संबंध ढूंढती है जो कोई इंसान देखने से चूक सकता है।फिर गणितज्ञों को उस पैटर्न को साबित करना होता है।
समझाना और लिखनाAI किसी प्रूफ़ को आसान शब्दों में समझाता है या कोई ड्राफ़्ट तैयार करता है।इंसान को इसे ध्यान से और परखते हुए पढ़ना चाहिए। स्पष्टीकरण में गलतियाँ हो सकती हैं।
शोधकर्ताओं ने दिखाया है कि AI सिस्टम कुछ कठिन प्रतियोगिता वाले सवालों को हल कर सकते हैं, जिनके प्रूफ़ किसी फ़ॉर्मल सिस्टम द्वारा जांचे जाते हैं। शोधकर्ताओं ने ऐसे पैटर्न पहचानने के लिए भी मशीन लर्निंग का इस्तेमाल किया है जिससे गणितज्ञ नए कंजेक्चर और प्रूफ़ तक पहुंचे। प्रगति तेज़ी से हो रही है, और बारीकियाँ बदलती रहती हैं, इसलिए दावों को दोहराने से पहले मूल रिसर्च पेपर ज़रूर पढ़ें।

मुख्य विचार: बनाएं, फिर सत्यापित करें

  1. 1

    प्रस्तावित करना

    एक मॉडल कोई प्रूफ़, कदम या कंजेक्चर सुझाता है। यह ग़लत भी हो सकता है।
  2. 2

    जांचना

    Lean एक फ़ॉर्मल प्रूफ़ की जांच करता है। टेस्ट या काउंटर-एग्ज़ाम्पल की खोज किसी कंजेक्चर की जांच करती है।
  3. 3

    रखना या खारिज करना

    सिर्फ़ जांचे गए प्रूफ़ ही रखे जाते हैं। असफल प्रयास अगली कोशिश के लिए फ़ीडबैक देते हैं।
  4. 4

    समझना

    गणितज्ञ नतीजे को पढ़ते और समझाते हैं, ताकि लोग जान सकें कि यह सच क्यों है।
नोट
यही वजह है कि गणित AI के लिए एक ख़ास क्षेत्र है। अधिकांश विज्ञान में, किसी भविष्यवाणी की जांच के लिए एक धीमी प्रक्रिया वाले प्रयोग की ज़रूरत होती है। फ़ॉर्मल गणित में, एक कंप्यूटर किसी प्रूफ़ को तेज़ी से और बहुत भरोसे के साथ जांच सकता है। एक भरोसेमंद चेकर AI के सुझावों का उपयोग करना बहुत सुरक्षित बना देता है।
जोखिम भरा इस्तेमाल
  • बिना जांचे चैटबॉट के प्रूफ़ को होमवर्क में कॉपी करना
  • किसी पैटर्न पर सिर्फ़ इसलिए भरोसा करना क्योंकि वह 100 मामलों में सही रहा
  • ऐसे कथन के प्रूफ़ को स्वीकार करना जिसे आपने ध्यान से नहीं पढ़ा
अच्छा इस्तेमाल
  • AI से हिंट मांगना, फिर खुद प्रूफ़ लिखना और उसकी जांच करना
  • काउंटर-एग्ज़ाम्पल खोजना, फिर उसे साबित करने की कोशिश करना
  • यह जांचना कि क्या फ़ॉर्मल कथन वही कह रहा है जो आपका मतलब है
इसे आज़माएं। किसी ऐसे पैटर्न के बारे में सोचें जिसे आपने गणित की कक्षा में देखा हो, जैसे "दो विषम संख्याओं का योग सम होता है"। क्या आप समझा सकते हैं कि यह हमेशा सच क्यों होता है, सिर्फ़ उन्हीं उदाहरणों के लिए नहीं जिन्हें आपने आज़माया था?

और देखें और पढ़ें

Lean programming language and theorem proverLean · reading

लैब

एक छोटा Python सर्च जो एक लुभावने कंजेक्चर का परीक्षण करता है, और उदाहरण बनाम प्रूफ़ पर एक लिखित विचार।

~25 min

समस्या

आप काउंटर-एग्ज़ाम्पल खोजकर दो कंजेक्चर का परीक्षण करेंगे।

  1. शुरुआती कोड चलाएं। यह n = 0 से 50 के लिए "n × n + n + 41 हमेशा अभाज्य संख्या है" का परीक्षण करता है। यह किस n पर पहली बार असफल होता है?
  2. दूसरे कंजेक्चर का परीक्षण करने के लिए कोड बदलें: "पहली n विषम संख्याओं का योग n × n होता है"। n = 1 से 1000 तक जांचें। क्या यह कभी असफल होता है?
  3. दूसरे कंजेक्चर के लिए, अपने शब्दों में (या वर्गों के चित्र के साथ) समझाने की कोशिश करें कि यह हमेशा सच क्यों होता है। यह एक प्रूफ़ की शुरुआत है।
  4. "1000 मामलों के लिए जांचा गया" और "साबित किया गया" के बीच के अंतर पर तीन वाक्य लिखें।

प्रैक्टिस लैब

कोड में बदलाव करें और इसे रन करें। Python आपके ब्राउज़र में चलता है — हमारे सर्वर पर कुछ नहीं भेजा जाता।

आउटपुट

कोई आउटपुट नहीं। वैल्यूज़ देखने के लिए print(...) जोड़ें।

आपका काम तब पूरा होगा जब

कठिन सवाल

उत्तर देखने से पहले ख़ुद जवाब देने की कोशिश करें। अगर आप इनके जवाब दे सकते हैं, तो आप पाठ समझ गए हैं।

Q1अगर कोई कंप्यूटर बिना किसी काउंटर-एग्ज़ाम्पल के एक अरब मामलों के लिए किसी कंजेक्चर की जांच करता है, तो क्या वह प्रूफ़ है?दिखाएं

नहीं। यह कथन अनंत संख्याओं के बारे में है, और एक अरब अभी भी एक सीमित संख्या ही है। कुछ प्रसिद्ध कंजेक्चर बहुत बड़े दायरे तक सही रहे, जिसके बाद कोई काउंटर-एग्ज़ाम्पल मिला। बड़े पैमाने पर की गई जांच अच्छे साक्ष्य हैं और गणितज्ञों का मार्गदर्शन कर सकते हैं, लेकिन एक प्रूफ़ को तर्क द्वारा हर मामले को कवर करना चाहिए।

Q2एक AI Lean में प्रूफ़ लिखता है जिसे स्वीकार कर लिया जाता है, लेकिन गणितज्ञों को समझ नहीं आता कि यह काम कैसे करता है। क्या यह कोई समस्या है?दिखाएं

नतीजा अभी भी सही है: Lean ने इसकी जांच कर ली है। लेकिन गणित का मतलब समझना भी है। ऐसा प्रूफ़ जिसे कोई नहीं समझता, वह कम सिखाता है और उस पर आगे काम करना कठिन होता है। गणितज्ञ फिर मुख्य विचार निकालने के लिए उस प्रूफ़ का अध्ययन कर सकते हैं, या अधिक स्पष्ट प्रूफ़ की तलाश कर सकते हैं। सही होने और समझ दोनों का महत्व है।

जारी रखने के लिए कृपया साइन इन करें।

अक्सर पूछे जाने वाले सवाल

क्या चैटबॉट द्वारा लिखे गए प्रूफ़ पर भरोसा किया जा सकता है?

सिर्फ़ अपने दम पर नहीं। एक चैटबॉट ऐसा प्रूफ़ लिख सकता है जो सुनने में सही लगे लेकिन उसमें कोई कमी या ग़लत कदम हो। इसे खुद ध्यान से जांचें, या किसी प्रूफ़ असिस्टेंट का उपयोग करें। Lean द्वारा जांचा गया फ़ॉर्मल प्रूफ़ सामान्य भाषा की तुलना में कहीं अधिक भरोसेमंद होता है।

क्या Lean सीखना कठिन है?

किसी भी सटीक भाषा की तरह, इसमें अभ्यास की ज़रूरत होती है। lean-lang.org और Lean समुदाय से जुड़े मुफ़्त शुरुआती ट्यूटोरियल और इंटरैक्टिव गेम्स उपलब्ध हैं। सबसे सरल से शुरुआत करने के लिए स्कूली बीजगणित काफ़ी है।

क्या AI गणितज्ञों की जगह ले लेगा?

प्रूफ़ खोजने और जांचने के लिए AI एक बेहतरीन मददगार बन रहा है। लेकिन महत्वपूर्ण सवालों को चुनना, नए विचार बनाना और यह समझाना कि चीज़ें सच क्यों हैं, गणित के बेहद मानवीय पहलू हैं। कई गणितज्ञ AI को एक नए तरह के सहयोगी और टूल के रूप में देखते हैं।

क्या हो अगर Lean को दिया गया कथन ही ग़लत हो?

तब Lean ग़लत कथन के सही प्रूफ़ की जांच कर सकता है। यह एक वास्तविक जोखिम है। लोगों को फ़ॉर्मल कथन को ध्यान से पढ़ना चाहिए और यह पक्का करना चाहिए कि यह वही है जो उनका मतलब था। चेकर प्रूफ़ को सत्यापित करता है, आपके इरादे को नहीं।

पाठ का टेस्ट

5 सवाल। पास होने और इस पाठ को पूरा करने के लिए 3 सही होने चाहिए (60%)।

टेस्ट देने और अपनी प्रोग्रेस सेव करने के लिए साइन इन करें