2 पॉइंट द्वारा GN⁺ 2024-12-13 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Xena प्रोजेक्ट और फर्मा का अंतिम प्रमेय

    • Xena प्रोजेक्ट का लक्ष्य गणित को कंप्यूटर पर formalize करना है। इसका उद्देश्य यह है कि यदि AI-आधारित गणित क्रांति होती है, तो कंप्यूटर आधुनिक संख्या सिद्धांत की सीमाओं का विस्तार करने में मदद कर सकें।
  • फर्मा के अंतिम प्रमेय का formalization

    • फर्मा के अंतिम प्रमेय (FLT) को कंप्यूटर पर सिद्ध करने का काम जारी है। इस प्रक्रिया में कंप्यूटर को R=T प्रमेय सिखाना एक प्रमुख चुनौती है।
    • Wiles के मूल प्रमाण के बजाय, आधुनिक, अधिक सामान्यीकृत और सरल किए गए प्रमाण को formalize करने की कोशिश की जा रही है।
  • crystalline cohomology और divided power structure

    • crystalline cohomology 1960-70 के दशक में विकसित किया गया एक सिद्धांत है, जो गणितीय formalization में महत्वपूर्ण भूमिका निभाता है।
    • divided power structure वह अवधारणा है जो crystalline cohomology को कंप्यूटर को सिखाने के लिए आवश्यक है।
  • मानव गणित documentation की समस्या

    • गणितीय documentation की अशुद्धता उजागर होती है। यह विशेषज्ञों के बीच ज्ञात बात है, लेकिन कई मामलों में documentation ठीक से नहीं किया गया है।
    • formalization का काम इन समस्याओं को हल करने में मदद कर सकता है।
  • formalization का महत्व

    • गणित को formalize करना एक महत्वपूर्ण कदम है, ताकि मशीनें स्वयं गणितीय तर्क कर सकें।
    • कई गणितज्ञ formalization की आवश्यकता महसूस नहीं करते, लेकिन मानव त्रुटि को कम करने के लिए यह आवश्यक है।
  • निष्कर्ष

    • हाल की प्रस्तुति में divided power के formalization की समस्या हल कर ली गई। इसका अर्थ है कि प्रोजेक्ट फिर से सही रास्ते पर आ गया है।

1 टिप्पणियां

 
GN⁺ 2024-12-13
Hacker News की राय
  • ग्रेजुएट स्कूल के दिनों को याद किया, जब तेज़ कोड लिखकर Birch और Swinnerton-Dyer conjecture में मदद करते थे। सेमिनार में जब कहा कि वे counterexample ढूंढना चाहते हैं, तो विशेषज्ञ नाराज़ हो गए। गणित की गहराई पूरी तरह समझ नहीं पाए थे, लेकिन जिज्ञासा ज़रूर जागी।

  • गणित में formalism के विकास पर खुशी जताई। एक programmer के तौर पर यह गणित को अधिक सुलभ बनाता है। formalism की कमी को लेकर चिंता का जवाब जिज्ञासा से देना चाहिए।

  • गणितज्ञ अक्सर विवरण छोड़ देते हैं। अगर सख्त proof चाहिए, तो विशेषज्ञ की मदद ज़रूरी होती है। आधुनिक गणित अस्थिर नींव पर खड़ा है।

  • Andrew Wiles द्वारा FLT को सिद्ध करने की प्रक्रिया को याद किया। 1990 के दशक का proof करने का तरीका अब पुराना महसूस होता है।

  • आधुनिक गणित में documentation की कमी पर ज़ोर दिया। formal systems के ज़रिए त्रुटियाँ कम करने की ज़रूरत है। मशीनों को गणितीय तर्क सिखाना महत्वपूर्ण है।

  • UI/UX designer और developer की भूमिकाओं का अंतर समझाया। design और development अलग तरह की सोच मांगते हैं।

  • उम्मीद जताई कि Lean जैसे theorem prover गणित में महत्वपूर्ण tool बनेंगे।

  • Lean code को देखना दिलचस्प लगा। अंतिम proof statement unit test जैसी भूमिका निभाता है।

  • यह सवाल उठाया कि क्या दशकों से इस्तेमाल हो रही कुछ गणितीय अवधारणाएँ गलत हो सकती हैं।

  • 'vitiated' शब्द का परिचय दिया और कहा कि proof गलत होने पर इसका इस्तेमाल अच्छा रहेगा।

  • गणितज्ञों और engineers के बीच की खाई का ज़िक्र किया, और उम्मीद जताई कि जब मशीनें गणित हल करेंगी तब performance में भी सुधार होगा।

  • गणितीय literature की स्थिति पर निराशा जताई। अंदाज़ा लगाया कि 1960 के दशक से 1990 के दशक तक की number theory literature में समस्याएँ हो सकती हैं। विशेषज्ञ समुदाय जितना छोटा होता है, त्रुटियाँ उतनी आसानी से नज़रअंदाज़ हो सकती हैं।