कंप्यूटर-सहायता प्रमाण: Difference between revisions

Latest revision as of 11:50, 28 June 2023

एक कंप्यूटर-सहायता प्राप्त प्रमाण एक गणितीय प्रमाण है जो कम से कम आंशिक रूप से कंप्यूटर द्वारा उत्पन्न किया गया है।

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

स्वचालित तर्क विधियों जैसे अनुमानी खोज का उपयोग करके नीचे से ऊपर तक गणितीय प्रमेय के छोटे स्पष्ट नए प्रमाण बनाने के लिए कृत्रिम बुद्धि अनुसंधान के क्षेत्र में भी प्रयास किए गए हैं। इस तरह के स्वचालित प्रमेय सिद्ध करने वालों ने कई नए परिणामों को सिद्ध किया है और ज्ञात प्रमेयों के लिए नए प्रमाण खोजे हैं। इसके अतिरिक्त इंटरैक्टिव प्रमाण सहायक गणितज्ञों को मानव-पठनीय प्रमाण विकसित करने की अनुमति देते हैं जो अभी भी शुद्धता के लिए औपचारिक रूप से सत्यापित हैं। चूँकि ये प्रमाण सामान्यतः मानव-सर्वे योग्य हैं (यद्यपि रॉबिन्स अनुमान के प्रमाण के साथ कठिनाई के साथ) वे कंप्यूटर-एडेड प्रमाण-बाय-एग्जॉशन के विवादास्पद निहितार्थों को साझा नहीं करते हैं।

विधि

गणितीय प्रमाणों में कंप्यूटरों का उपयोग करने का एक विधि तथाकथित मान्य संख्यात्मक या कठोर संख्यात्मक के माध्यम से है। इसका अर्थ है संख्यात्मक रूप से फिर भी गणितीय कठोरता के साथ गणना करना एक निर्धारित मान अंकगणित का उपयोग करता है और inclusion principle^[clarify] यह सुनिश्चित करने के लिए कि संख्यात्मक प्रोग्राम का निर्धारित मान आउटपुट मूल गणितीय समस्या के समाधान को संलग्न करता है। यह राउंड-ऑफ और ट्रंकेशन त्रुटियों को नियंत्रित करने, घेरने और प्रचारित करने के द्वारा किया जाता है, उदाहरण के लिए अंतराल अंकगणितीय अधिक स्पष्ट रूप से कोई गणना को प्राथमिक संचालन के अनुक्रम में कम कर देता है, जिसे $(+,-,\times ,/)$ कहते हैं एक कंप्यूटर में प्रत्येक प्रारंभिक ऑपरेशन का परिणाम कंप्यूटर परिशुद्धता द्वारा गोल किया जाता है। चूँकि एक प्रारंभिक ऑपरेशन के परिणाम पर ऊपरी और निचले सीमा द्वारा प्रदान किए गए अंतराल का निर्माण कर सकते हैं। इसके बाद संख्याओं को अंतरालों से प्रतिस्थापित करके और प्रस्तुत करने योग्य संख्याओं के ऐसे अंतरालों के बीच प्रारंभिक संक्रियाएँ करते हुए आगे बढ़ता है।

दार्शनिक आपत्तियाँ

कंप्यूटर-सहायता प्राप्त प्रमाण गणितीय दुनिया में कुछ विवाद का विषय हैं आपत्तियों को स्पष्ट करने के लिए सबसे पहले थॉमस टिमोच्ज़को के साथ जो लोग टिमोच्ज़को के तर्कों का पालन करते हैं उनका यह मानना है कि लंबे कंप्यूटर-सहायता वाले प्रमाण कुछ अर्थों में, 'वास्तविक' गणितीय प्रमाण नहीं हैं क्योंकि उनमें इतने तार्किक कदम सम्मिलित हैं कि वे व्यावहारिक रूप से मनुष्यों द्वारा सत्यापन और सत्यापन नहीं कर रहे हैं और गणितज्ञ प्रभावी रूप से एक अनुभवजन्य कम्प्यूटेशनल प्रक्रिया में विश्वास के साथ अनुमानित सिद्धांतों से तार्किक कमी को बदलने के लिए कहा गया जो कंप्यूटर प्रोग्राम में त्रुटियों के साथ-साथ रनटाइम पर्यावरण और हार्डवेयर में दोषों से संभावित रूप से प्रभावित होता है।^[1]

अन्य गणितज्ञों का मानना है कि लंबे कंप्यूटर-सहायता वाले प्रमाणों को प्रमाणों के अतिरिक्त गणनाओं के रूप में माना जाना चाहिए: प्रमाण एल्गोरिथ्म को ही वैध सिद्ध होना चाहिए जिससे इसके उपयोग को केवल सत्यापन के रूप में माना जा सकता है । तर्क है कि कंप्यूटर-सहायता प्राप्त प्रमाण उनके स्रोत प्रोग्राम कंपाइलर और हार्डवेयर में त्रुटियों के अधीन हैं कंप्यूटर प्रोग्राम के लिए शुद्धता का एक औपचारिक प्रमाण प्रदान करके हल किया जा सकता है (एक दृष्टिकोण जिसे 2005 में चार-रंग प्रमेय पर सफलतापूर्वक प्रयुक्त किया गया था) साथ ही विभिन्न प्रोग्रामिंग भाषाओं विभिन्न कंपाइलरों और विभिन्न कंप्यूटर हार्डवेयर का उपयोग करके परिणाम की प्रतिलिपी करना है।

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

कंप्यूटर-सहायक प्रमाण के विपरीत एक और तर्क यह है कि उनमें गणितीय लालित्य की कमी है - कि वे कोई अंतर्दृष्टि या नई और उपयोगी अवधारणा प्रदान नहीं करते हैं। वास्तव में यह एक ऐसा तर्क है जिसे किसी भी लंबे प्रमाण के विरुद्ध थकावट द्वारा आगे बढ़ाया जा सकता है।

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

प्रायोगिक गणित का उभरता हुआ क्षेत्र गणितीय अन्वेषण के लिए अपने मुख्य उपकरण के रूप में संख्यात्मक प्रयोगों पर ध्यान केंद्रित करके इस बहस का सामना कर रहा है।

अनुप्रयोग

कंप्यूटर प्रोग्राम की सहायता से प्रमेयों को सिद्ध किया

इस सूची में सम्मिलित करने का अर्थ यह नहीं है कि एक औपचारिक कंप्यूटर-जाँच प्रमाण उपस्थित है चूँकि यह कि एक कंप्यूटर प्रोग्राम किसी तरह से सम्मिलित किया गया है। विवरण के लिए मुख्य लेख देखें।

Four color theorem, 1976
Mitchell Feigenbaum's universality conjecture in non-linear dynamics. Proven by O. E. Lanford using rigorous computer arithmetic, 1982
Connect Four, 1988 – a solved game
Non-existence of a finite projective plane of order 10, 1989
Double bubble conjecture, 1995^[2]
Robbins conjecture, 1996
Kepler conjecture, 1998 – the problem of optimal sphere packing in a box
Lorenz attractor, 2002 – 14th of Smale's problems proved by Warwick Tucker using interval arithmetic
17-point case of the Happy Ending problem, 2006
Kouril^[3]^[4]^[5] (between 2006 and 2016) computed several van der Waerden numbers using FPGA-based SAT-solver.
NP-hardness of minimum-weight triangulation, 2008
Ahmed^[6]^[7]^[8]^[9]^[10] (between 2009 and 2014) computed several van der Waerden numbers using DPLL algorithm-based stand-alone and distributed SAT-solvers. Ahmed first used cluster-distributed SAT-solvers to prove w(2; 3, 17) = 279 and w(2; 3, 18) = 312 in 2010.^[7]
Optimal solutions for Rubik's Cube can be obtained in at most 20 face moves, 2010
Minimum number of clues for a solvable Sudoku puzzle is 17, 2012
In 2014 a special case of the Erdős discrepancy problem was solved using a SAT-solver. The full conjecture was later solved by Terence Tao without computer assistance.^[11]
Boolean Pythagorean triples problem solved using 200 terabytes of data in May 2016.^[12]
Applications to the Kolmogorov-Arnold-Moser theory^[13]^[14]
Kazhdan's property (T) for the automorphism group of a free group of rank at least five
Schur number five, the proof that S(5) = 161 was announced in 2017 by Marijn Heule and took up 2 petabytes of space^[15]^[16]
Keller's conjecture in dimension 7 the only remaining case in 2020 with a 200 gigabyte proof^[17]^[18]
The packing chromatic number of the infinite square grid is 15, by Subercaseaux and Heule in 2023^[19]^[20] (See also: Hadwiger–Nelson problem for the chromatic number of the plane)

बिक्री के लिए प्रमेय

2010 में एडिनबर्ग विश्वविद्यालय के शिक्षाविदों ने लोगों को कंप्यूटर-सहायता प्रमाण के माध्यम से बनाए गए अपने स्वयं के प्रमेय को खरीदने का अवसर दिया। इस नए प्रमेय को क्रेता के नाम पर रखा जाएगा।^[21]^[22] ऐसा लगता है कि यह सेवा अब उपलब्ध नहीं है।

यह भी देखें

संदर्भ

↑ Tymoczko, Thomas (1979), "The Four-Color Problem and its Mathematical Significance", The Journal of Philosophy, 76 (2): 57–83, doi:10.2307/2025976, JSTOR 2025976.
↑ Hass, J.; Hutchings, M.; Schlafly, R. (1995). "The double bubble conjecture". Electronic Research Announcements of the American Mathematical Society. 1 (3): 98–102. CiteSeerX 10.1.1.527.8616. doi:10.1090/S1079-6762-95-03001-0.
↑ Kouril, Michal (2006). A Backtracking Framework for Beowulf Clusters with an Extension to Multi-Cluster Computation and Sat Benchmark Problem Implementation (Ph.D. thesis). University of Cincinnati.
↑ Kouril, Michal (2012). "Computing the van der Waerden number W(3,4)=293". Integers. 12: A46. MR 3083419.
↑ Kouril, Michal (2015). "Leveraging FPGA clusters for SAT computations". Parallel Computing: On the Road to Exascale: 525–532.
↑ Ahmed, Tanbir (2009). "Some new van der Waerden numbers and some van der Waerden-type numbers". Integers. 9: A6. doi:10.1515/integ.2009.007. MR 2506138. S2CID 122129059.
↑ ^7.0 ^7.1 Ahmed, Tanbir (2010). "Two new van der Waerden numbers w(2;3,17) and w(2;3,18)". Integers. 10 (4): 369–377. doi:10.1515/integ.2010.032. MR 2684128. S2CID 124272560.
↑ Ahmed, Tanbir (2012). "On computation of exact van der Waerden numbers". Integers. 12 (3): 417–425. doi:10.1515/integ.2011.112. MR 2955523. S2CID 11811448.
↑ Ahmed, Tanbir (2013). "Some More Van der Waerden numbers". Journal of Integer Sequences. 16 (4): 13.4.4. MR 3056628.
↑ Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter (2014). "On the van der Waerden numbers w(2;3,t)". Discrete Applied Mathematics. 174 (2014): 27–51. arXiv:1102.5433. doi:10.1016/j.dam.2014.05.007. MR 3215454.
↑ Cesare, Chris (1 October 2015). "Maths whizz solves a master's riddle". Nature. 526 (7571): 19–20. Bibcode:2015Natur.526...19C. doi:10.1038/nature.2015.18441. PMID 26432222.
↑ Lamb, Evelyn (26 May 2016). "Two-hundred-terabyte maths proof is largest ever". Nature. 534 (7605): 17–18. Bibcode:2016Natur.534...17L. doi:10.1038/nature.2016.19990. PMID 27251254.
↑ Celletti, A.; Chierchia, L. (1987). "Rigorous estimates for a computer‐assisted KAM theory". Journal of Mathematical Physics. 28 (9): 2078–86. Bibcode:1987JMP....28.2078C. doi:10.1063/1.527418.
↑ Figueras, J.L.; Haro, A.; Luque, A. (2017). "Rigorous computer-assisted application of KAM theory: a modern approach". Foundations of Computational Mathematics. 17 (5): 1123–93. arXiv:1601.00084. doi:10.1007/s10208-016-9339-3. hdl:2445/192693. S2CID 28258285.
↑ Heule, Marijn J. H. (2017). "Schur Number Five". arXiv:1711.08076 [cs.LO].
↑ "Schur Number Five". www.cs.utexas.edu. Retrieved 2021-10-06.
↑ Brakensiek, Joshua; Heule, Marijn; Mackey, John; Narváez, David (2020). Peltier, Nicolas; Sofronie-Stokkermans, Viorica (eds.). "The Resolution of Keller's Conjecture". Automated Reasoning. Lecture Notes in Computer Science. Springer. 12166: 48–65. doi:10.1007/978-3-030-51074-9_4. ISBN 978-3-030-51074-9. PMC 7324133.
↑ Hartnett, Kevin (2020-08-19). "Computer Search Settles 90-Year-Old Math Problem". Quanta Magazine (in English). Retrieved 2021-10-08.
↑ Subercaseaux, Bernardo; Heule, Marijn J. H. (2023-01-23). "The Packing Chromatic Number of the Infinite Square Grid is 15". arXiv:2301.09757 [cs.DM].
↑ Hartnett, Kevin (2023-04-20). "The Number 15 Describes the Secret Limit of an Infinite Grid". Quanta Magazine (in English). Retrieved 2023-04-20.
↑ "अपनी स्वयं की प्रमेय खरीदने पर हेराल्ड राजपत्र लेख". Herald Gazette Scotland. November 2010. Archived from the original on 2010-11-21.
↑ "स्कूल ऑफ इंफॉर्मेटिक्स, यूनिवर्सिटी.ऑफ़ एडिनबर्ग वेबसाइट". School of Informatics, Univ.of Edinburgh. April 2015.^{[permanent dead link]}

अग्रिम पठन

Lenat, D.B. (1976). AM: An artificial intelligence approach to discovery in mathematics as heuristic search (PDF) (PhD). AI Lab., Stanford University. STAN-CS-76-570, Heuristic Programming Project Report HPP-76-8.
Meyer, K.R.; Schmidt, D.S., eds. (2012). Computer aided proofs in analysis. IMA volumes in mathematics and it's applications. Vol. 28. Springer. ISBN 978-1-4613-9092-3.
Nakao, M.; Plum, M.; Watanabe, Y. (2019). Numerical Verification Methods and Computer-Assisted Proofs for Partial Differential Equations. Springer Series in Computational Mathematics. Springer. ISBN 9789811376696.

बाहरी संबंध

Lanford, Oscar E. (1982). "A computer-assisted proof of the Feigenbaum conjectures" (PDF). Bull. Amer. Math. Soc. 6 (3): 427–434. CiteSeerX 10.1.1.434.8389. doi:10.1090/S0273-0979-1982-15008-X.
Furse, Edmund (1990). Why did AM run out of steam? (Technical report). Department of Computer Studies, University of Glamorgan. CS-90-4. Archived from the original on 2012-07-17. Retrieved 2016-09-06.{{cite tech report}}: CS1 maint: bot: original URL status unknown (link)
Begley, S. (April 16, 2018). "Number proofs done by computer might err". Pittsburgh Post-Gazette. Archived from the original on 2018-04-16.
"A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008.

[tymoczko-1] Tymoczko, Thomas (1979), "The Four-Color Problem and its Mathematical Significance", The Journal of Philosophy, 76 (2): 57–83, doi:10.2307/2025976, JSTOR 2025976.

[2] Hass, J.; Hutchings, M.; Schlafly, R. (1995). "The double bubble conjecture". Electronic Research Announcements of the American Mathematical Society. 1 (3): 98–102. CiteSeerX 10.1.1.527.8616. doi:10.1090/S1079-6762-95-03001-0.

[kouril2006-3] Kouril, Michal (2006). A Backtracking Framework for Beowulf Clusters with an Extension to Multi-Cluster Computation and Sat Benchmark Problem Implementation (Ph.D. thesis). University of Cincinnati.

[kouril2012-4] Kouril, Michal (2012). "Computing the van der Waerden number W(3,4)=293". Integers. 12: A46. MR 3083419.

[kouril2016-5] Kouril, Michal (2015). "Leveraging FPGA clusters for SAT computations". Parallel Computing: On the Road to Exascale: 525–532.

[ahmed2009-6] Ahmed, Tanbir (2009). "Some new van der Waerden numbers and some van der Waerden-type numbers". Integers. 9: A6. doi:10.1515/integ.2009.007. MR 2506138. S2CID 122129059.

[ahmed2010-7] 7.0 ^7.1 Ahmed, Tanbir (2010). "Two new van der Waerden numbers w(2;3,17) and w(2;3,18)". Integers. 10 (4): 369–377. doi:10.1515/integ.2010.032. MR 2684128. S2CID 124272560.

[ahmed2011-8] Ahmed, Tanbir (2012). "On computation of exact van der Waerden numbers". Integers. 12 (3): 417–425. doi:10.1515/integ.2011.112. MR 2955523. S2CID 11811448.

[ahmedJIS-9] Ahmed, Tanbir (2013). "Some More Van der Waerden numbers". Journal of Integer Sequences. 16 (4): 13.4.4. MR 3056628.

[aks2011-10] Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter (2014). "On the van der Waerden numbers w(2;3,t)". Discrete Applied Mathematics. 174 (2014): 27–51. arXiv:1102.5433. doi:10.1016/j.dam.2014.05.007. MR 3215454.

[11] Cesare, Chris (1 October 2015). "Maths whizz solves a master's riddle". Nature. 526 (7571): 19–20. Bibcode:2015Natur.526...19C. doi:10.1038/nature.2015.18441. PMID 26432222.

[12] Lamb, Evelyn (26 May 2016). "Two-hundred-terabyte maths proof is largest ever". Nature. 534 (7605): 17–18. Bibcode:2016Natur.534...17L. doi:10.1038/nature.2016.19990. PMID 27251254.

[13] Celletti, A.; Chierchia, L. (1987). "Rigorous estimates for a computer‐assisted KAM theory". Journal of Mathematical Physics. 28 (9): 2078–86. Bibcode:1987JMP....28.2078C. doi:10.1063/1.527418.

[14] Figueras, J.L.; Haro, A.; Luque, A. (2017). "Rigorous computer-assisted application of KAM theory: a modern approach". Foundations of Computational Mathematics. 17 (5): 1123–93. arXiv:1601.00084. doi:10.1007/s10208-016-9339-3. hdl:2445/192693. S2CID 28258285.

[15] Heule, Marijn J. H. (2017). "Schur Number Five". arXiv:1711.08076 [cs.LO].

[16] "Schur Number Five". www.cs.utexas.edu. Retrieved 2021-10-06.

[17] Brakensiek, Joshua; Heule, Marijn; Mackey, John; Narváez, David (2020). Peltier, Nicolas; Sofronie-Stokkermans, Viorica (eds.). "The Resolution of Keller's Conjecture". Automated Reasoning. Lecture Notes in Computer Science. Springer. 12166: 48–65. doi:10.1007/978-3-030-51074-9_4. ISBN 978-3-030-51074-9. PMC 7324133.

[18] Hartnett, Kevin (2020-08-19). "Computer Search Settles 90-Year-Old Math Problem". Quanta Magazine (in English). Retrieved 2021-10-08.

[19] Subercaseaux, Bernardo; Heule, Marijn J. H. (2023-01-23). "The Packing Chromatic Number of the Infinite Square Grid is 15". arXiv:2301.09757 [cs.DM].

[20] Hartnett, Kevin (2023-04-20). "The Number 15 Describes the Secret Limit of an Infinite Grid". Quanta Magazine (in English). Retrieved 2023-04-20.

[21] "अपनी स्वयं की प्रमेय खरीदने पर हेराल्ड राजपत्र लेख". Herald Gazette Scotland. November 2010. Archived from the original on 2010-11-21.

[22] "स्कूल ऑफ इंफॉर्मेटिक्स, यूनिवर्सिटी.ऑफ़ एडिनबर्ग वेबसाइट". School of Informatics, Univ.of Edinburgh. April 2015.^{[permanent dead link]}

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

@@ Line 5: / Line 5: @@
 आज तक के अधिकांश कंप्यूटर-सहायक प्रमाण एक गणितीय [[प्रमेय]] के बड़े प्रमाण बाय एग्जॉशन के कार्यान्वयन हैं। यह विचार एक [[कंप्यूटर प्रोग्राम]] का उपयोग लंबी संगणना करने के लिए है, और एक प्रमाण प्रदान करने के लिए है कि इन संगणनाओं का परिणाम दिए गए प्रमेय का तात्पर्य है। 1976 में [[चार रंग प्रमेय]] एक कंप्यूटर प्रोग्राम का उपयोग करके सत्यापित किया जाने वाला पहला प्रमुख प्रमेय था।
-स्वचालित तर्क विधियों जैसे अनुमानी खोज का उपयोग करके नीचे से ऊपर तक गणितीय प्रमेय के छोटे स्पष्ट नए प्रमाण बनाने के लिए कृत्रिम बुद्धि अनुसंधान के क्षेत्र में भी प्रयास किए गए हैं। इस तरह के स्वचालित प्रमेय सिद्ध करने वालों ने कई नए परिणामों को सिद्ध किया है और ज्ञात प्रमेयों के लिए नए प्रमाण खोजे हैं। इसके अतिरिक्त इंटरैक्टिव प्रमाण  सहायक गणितज्ञों को मानव-पठनीय प्रमाण  विकसित करने की अनुमति देते हैं जो अभी भी शुद्धता के लिए औपचारिक रूप से सत्यापित हैं। चूँकि ये प्रमाण सामान्यतः मानव-सर्वे योग्य हैं (यद्यपि रॉबिन्स अनुमान के प्रमाण के साथ कठिनाई के साथ) वे कंप्यूटर-एडेड प्रमाण-बाय-एग्जॉशन के विवादास्पद निहितार्थों को साझा नहीं करते हैं।
+स्वचालित तर्क विधियों जैसे अनुमानी खोज का उपयोग करके नीचे से ऊपर तक गणितीय प्रमेय के छोटे स्पष्ट नए प्रमाण बनाने के लिए कृत्रिम बुद्धि अनुसंधान के क्षेत्र में भी प्रयास किए गए हैं। इस तरह के स्वचालित प्रमेय सिद्ध करने वालों ने कई नए परिणामों को सिद्ध किया है और ज्ञात प्रमेयों के लिए नए प्रमाण खोजे हैं। इसके अतिरिक्त इंटरैक्टिव प्रमाण सहायक गणितज्ञों को मानव-पठनीय प्रमाण विकसित करने की अनुमति देते हैं जो अभी भी शुद्धता के लिए औपचारिक रूप से सत्यापित हैं। चूँकि ये प्रमाण सामान्यतः मानव-सर्वे योग्य हैं (यद्यपि रॉबिन्स अनुमान के प्रमाण के साथ कठिनाई के साथ) वे कंप्यूटर-एडेड प्रमाण-बाय-एग्जॉशन के विवादास्पद निहितार्थों को साझा नहीं करते हैं।
 == विधि ==
-गणितीय प्रमाणों में कंप्यूटरों का उपयोग करने का एक विधि तथाकथित मान्य संख्यात्मक या कठोर संख्यात्मक के माध्यम से है। इसका अर्थ है संख्यात्मक रूप से फिर भी गणितीय कठोरता के साथ गणना करना एक निर्धारित मान  अंकगणित का उपयोग करता है और {{clarify span|inclusion principle|reason=What is this supposed to mean?|date=October 2020}} यह सुनिश्चित करने के लिए कि संख्यात्मक प्रोग्राम का निर्धारित मान  आउटपुट मूल गणितीय समस्या के समाधान को संलग्न करता है। यह राउंड-ऑफ और ट्रंकेशन त्रुटियों को नियंत्रित करने, घेरने और प्रचारित करने के द्वारा किया जाता है, उदाहरण के लिए [[अंतराल अंकगणित|अंतराल अंकगणितीय]] अधिक स्पष्ट रूप से कोई गणना को प्राथमिक संचालन के अनुक्रम में कम कर देता है, <math>(+, -, \times, /)</math> कहते हैं एक कंप्यूटर में प्रत्येक प्रारंभिक ऑपरेशन का परिणाम कंप्यूटर परिशुद्धता द्वारा गोल किया जाता है। चूँकि एक प्रारंभिक ऑपरेशन के परिणाम पर ऊपरी और निचले सीमा द्वारा प्रदान किए गए अंतराल का निर्माण कर सकते हैं। इसके बाद संख्याओं को अंतरालों से प्रतिस्थापित करके और प्रस्तुत करने योग्य संख्याओं के ऐसे अंतरालों के बीच प्रारंभिक संक्रियाएँ करते हुए आगे बढ़ता है।
+गणितीय प्रमाणों में कंप्यूटरों का उपयोग करने का एक विधि तथाकथित मान्य संख्यात्मक या कठोर संख्यात्मक के माध्यम से है। इसका अर्थ है संख्यात्मक रूप से फिर भी गणितीय कठोरता के साथ गणना करना एक निर्धारित मान अंकगणित का उपयोग करता है और {{clarify span|inclusion principle|reason=What is this supposed to mean?|date=October 2020}} यह सुनिश्चित करने के लिए कि संख्यात्मक प्रोग्राम का निर्धारित मान आउटपुट मूल गणितीय समस्या के समाधान को संलग्न करता है। यह राउंड-ऑफ और ट्रंकेशन त्रुटियों को नियंत्रित करने, घेरने और प्रचारित करने के द्वारा किया जाता है, उदाहरण के लिए [[अंतराल अंकगणित|अंतराल अंकगणितीय]] अधिक स्पष्ट रूप से कोई गणना को प्राथमिक संचालन के अनुक्रम में कम कर देता है, जिसे <math>(+, -, \times, /)</math> कहते हैं एक कंप्यूटर में प्रत्येक प्रारंभिक ऑपरेशन का परिणाम कंप्यूटर परिशुद्धता द्वारा गोल किया जाता है। चूँकि एक प्रारंभिक ऑपरेशन के परिणाम पर ऊपरी और निचले सीमा द्वारा प्रदान किए गए अंतराल का निर्माण कर सकते हैं। इसके बाद संख्याओं को अंतरालों से प्रतिस्थापित करके और प्रस्तुत करने योग्य संख्याओं के ऐसे अंतरालों के बीच प्रारंभिक संक्रियाएँ करते हुए आगे बढ़ता है।
 == दार्शनिक आपत्तियाँ ==
-{{main|गैर-सर्वे योग्य प्रमाण}}
+{{main|गैर-सर्वे योग्य प्रमाण}}कंप्यूटर-सहायता प्राप्त प्रमाण गणितीय दुनिया में कुछ विवाद का विषय हैं आपत्तियों को स्पष्ट करने के लिए सबसे पहले [[थॉमस टिमोच्ज़को]] के साथ जो लोग टिमोच्ज़को के तर्कों का पालन करते हैं उनका यह मानना है कि लंबे कंप्यूटर-सहायता वाले प्रमाण कुछ अर्थों में, 'वास्तविक' गणितीय प्रमाण नहीं हैं क्योंकि उनमें इतने तार्किक कदम सम्मिलित हैं कि वे व्यावहारिक रूप से मनुष्यों द्वारा [[सत्यापन और सत्यापन]] नहीं कर रहे हैं और गणितज्ञ प्रभावी रूप से एक अनुभवजन्य कम्प्यूटेशनल प्रक्रिया में विश्वास के साथ अनुमानित सिद्धांतों से तार्किक कमी को बदलने के लिए कहा गया जो कंप्यूटर प्रोग्राम में त्रुटियों के साथ-साथ रनटाइम पर्यावरण और हार्डवेयर में दोषों से संभावित रूप से प्रभावित होता है।<ref name="tymoczko">{{Citation|last = Tymoczko|first = Thomas|author-link = Thomas Tymoczko|title = The Four-Color Problem and its Mathematical Significance|year = 1979|journal = [[The Journal of Philosophy]]|volume = 76|issue = 2|pages = 57–83|doi=10.2307/2025976|jstor = 2025976}}.</ref>
-{{More citations needed section|date=October 2020}}
+अन्य गणितज्ञों का मानना है कि लंबे कंप्यूटर-सहायता वाले प्रमाणों को प्रमाणों के अतिरिक्त गणनाओं के रूप में माना जाना चाहिए: प्रमाण एल्गोरिथ्म को ही वैध सिद्ध होना चाहिए जिससे इसके उपयोग को केवल सत्यापन के रूप में माना जा सकता है । तर्क है कि कंप्यूटर-सहायता प्राप्त प्रमाण उनके स्रोत प्रोग्राम कंपाइलर और हार्डवेयर में त्रुटियों के अधीन हैं कंप्यूटर प्रोग्राम के लिए शुद्धता का एक औपचारिक प्रमाण प्रदान करके हल किया जा सकता है (एक दृष्टिकोण जिसे 2005 में चार-रंग प्रमेय पर सफलतापूर्वक प्रयुक्त किया गया था) साथ ही विभिन्न प्रोग्रामिंग भाषाओं विभिन्न कंपाइलरों और विभिन्न कंप्यूटर हार्डवेयर का उपयोग करके परिणाम की प्रतिलिपी करना है।
-कंप्यूटर-सहायता प्राप्त प्रमाण गणितीय दुनिया में कुछ विवाद का विषय हैं, आपत्तियों को स्पष्ट करने के लिए सबसे पहले [[थॉमस टिमोच्ज़को]] के साथ। जो लोग Tymoczko के तर्कों का पालन करते हैं, उनका मानना है कि लंबे कंप्यूटर-सहायता वाले प्रमाण, कुछ अर्थों में, 'वास्तविक' गणितीय प्रमाण नहीं हैं, क्योंकि उनमें इतने तार्किक कदम सम्मिलित हैं कि वे व्यावहारिक रूप से मनुष्यों द्वारा [[सत्यापन और सत्यापन]] नहीं कर रहे हैं, और गणितज्ञ प्रभावी रूप से एक अनुभवजन्य कम्प्यूटेशनल प्रक्रिया में विश्वास के साथ अनुमानित सिद्धांतों से तार्किक कटौती को बदलने के लिए कहा गया, जो कंप्यूटर प्रोग्राम में त्रुटियों के साथ-साथ रनटाइम पर्यावरण और हार्डवेयर में दोषों से संभावित रूप से प्रभावित होता है।<ref name="tymoczko">{{Citation|last = Tymoczko|first = Thomas|author-link = Thomas Tymoczko|title = The Four-Color Problem and its Mathematical Significance|year = 1979|journal = [[The Journal of Philosophy]]|volume = 76|issue = 2|pages = 57–83|doi=10.2307/2025976|jstor = 2025976}}.</ref>
+कंप्यूटर-सहायक प्रमाण को सत्यापित करने का एक अन्य संभावित विधि मशीन-पठनीय रूप में उनके तर्कपूर्ण चरणों को उत्पन्न करना है और फिर उनकी शुद्धता को प्रदर्शित करने के लिए [[ सबूत चेकर |प्रमाण चेकर]] प्रोग्राम का उपयोग करना है। चूँकि दिए गए प्रमाण को सत्यापित करना प्रमाण खोजने की तुलना में बहुत आसान है चेकर कार्यक्रम मूल सहायक कार्यक्रम की तुलना में सरल है और इसकी शुद्धता में विश्वास प्राप्त करना इसलिए आसान है। चूँकि दूसरे प्रोग्राम के आउटपुट को सही सिद्ध करने के लिए एक कंप्यूटर प्रोग्राम का उपयोग करने का यह विधि कंप्यूटर प्रमाण संशयवादियों को पसंद नहीं आता है जो इसे मानव समझ की कथित आवश्यकता को संबोधित किए बिना जटिलता की एक और परत जोड़ने के रूप में देखते हैं।
-अन्य गणितज्ञों का मानना है कि लंबे कंप्यूटर-सहायता वाले प्रमाणों को प्रमाणों के बजाय गणनाओं के रूप में माना जाना चाहिए: प्रमाण एल्गोरिथ्म को ही वैध साबित होना चाहिए, ताकि इसके उपयोग को केवल सत्यापन के रूप में माना जा सके। तर्क है कि कंप्यूटर-सहायता प्राप्त प्रमाण उनके स्रोत प्रोग्राम, कंपाइलर और हार्डवेयर में त्रुटियों के अधीन हैं, कंप्यूटर प्रोग्राम के लिए शुद्धता का एक औपचारिक प्रमाण प्रदान करके हल किया जा सकता है (एक दृष्टिकोण जिसे 2005 में चार-रंग प्रमेय पर सफलतापूर्वक लागू किया गया था) साथ ही विभिन्न प्रोग्रामिंग भाषाओं, विभिन्न कंपाइलरों और विभिन्न कंप्यूटर हार्डवेयर का उपयोग करके परिणाम की नकल करना।
-कंप्यूटर-सहायक प्रमाण को सत्यापित करने का एक अन्य संभावित विधि मशीन-पठनीय रूप में उनके तर्कपूर्ण चरणों को उत्पन्न करना है, और फिर उनकी शुद्धता को प्रदर्शित करने के लिए [[ सबूत चेकर | प्रमाण चेकर]] प्रोग्राम का उपयोग करना है। चूँकि दिए गए प्रमाण को सत्यापित करना प्रमाण खोजने की तुलना में बहुत आसान है, चेकर कार्यक्रम मूल सहायक कार्यक्रम की तुलना में सरल है, और इसकी शुद्धता में विश्वास हासिल करना तदनुसार आसान है। चूँकि , दूसरे प्रोग्राम के आउटपुट को सही साबित करने के लिए एक कंप्यूटर प्रोग्राम का उपयोग करने का यह विधि कंप्यूटर प्रमाण संशयवादियों को पसंद नहीं आता है, जो इसे मानव समझ की कथित आवश्यकता को संबोधित किए बिना जटिलता की एक और परत जोड़ने के रूप में देखते हैं।
+कंप्यूटर-सहायक प्रमाण के विपरीत एक और तर्क यह है कि उनमें [[गणितीय लालित्य]] की कमी है - कि वे कोई अंतर्दृष्टि या नई और उपयोगी अवधारणा प्रदान नहीं करते हैं। वास्तव में यह एक ऐसा तर्क है जिसे किसी भी लंबे प्रमाण के विरुद्ध थकावट द्वारा आगे बढ़ाया जा सकता है।
-कंप्यूटर-सहायक प्रमाण के खिलाफ एक और तर्क यह है कि उनमें [[गणितीय लालित्य]] की कमी है - कि वे कोई अंतर्दृष्टि या नई और उपयोगी अवधारणा प्रदान नहीं करते हैं। वास्तव में, यह एक ऐसा तर्क है जिसे किसी भी लंबे प्रमाण के विरुद्ध थकावट द्वारा आगे बढ़ाया जा सकता है।
+कंप्यूटर-सहायता प्राप्त प्रमाणों द्वारा उठाया गया एक अतिरिक्त दार्शनिक उद्देश्य यह है कि क्या वे गणित को [[गणित में अर्ध-अनुभववाद]] में बनाते हैं अर्ध-अनुभवजन्य विज्ञान जहां अमूर्त गणितीय अवधारणाओं के क्षेत्र में वैज्ञानिक पद्धति शुद्ध कारण के अनुप्रयोग से अधिक महत्वपूर्ण हो जाती है। यह सीधे गणित के अंदर तर्क से संबंधित है कि क्या गणित विचारों पर आधारित है या औपचारिक प्रतीक हेरफेर में केवल एक अभ्यास (गणित) यह सवाल भी उठाता है कि क्या यदि [[गणितीय प्लैटोनिज्म]] दृष्टिकोण के अनुसार किसी अर्थ में सभी संभावित गणितीय वस्तुएं पहले से उपस्थित हैं तो क्या कंप्यूटर-समर्थित गणित खगोल विज्ञान की तरह एक अवलोकन संबंधी अध्ययन विज्ञान है न कि भौतिकी या रसायन विज्ञान की तरह एक प्रयोगात्मक अध्ययन गणित के अंदर यह विवाद उसी समय उत्पन्न हो रहा है जब भौतिकी समुदाय में इस बारे में प्रश्न पूछे जा रहे हैं कि क्या इक्कीसवीं सदी का [[सैद्धांतिक भौतिकी]] बहुत अधिक गणितीय होता जा रहा है और अपनी प्रायोगिक जड़ों को पीछे छोड़ रहा है।
-कंप्यूटर-सहायता प्राप्त प्रमाणों द्वारा उठाया गया एक अतिरिक्त दार्शनिक मुद्दा यह है कि क्या वे गणित को [[गणित में अर्ध-अनुभववाद]] में बनाते हैं|अर्ध-अनुभवजन्य विज्ञान, जहां अमूर्त गणितीय अवधारणाओं के क्षेत्र में वैज्ञानिक पद्धति शुद्ध कारण के अनुप्रयोग से अधिक महत्वपूर्ण हो जाती है। यह सीधे गणित के भीतर तर्क से संबंधित है कि क्या गणित विचारों पर आधारित है, या औपचारिक प्रतीक हेरफेर में केवल एक अभ्यास (गणित)। यह सवाल भी उठाता है कि क्या, यदि [[गणितीय प्लैटोनिज्म]] दृष्टिकोण के अनुसार, किसी अर्थ में सभी संभावित गणितीय वस्तुएं पहले से मौजूद हैं, तो क्या कंप्यूटर-समर्थित गणित खगोल विज्ञान की तरह एक अवलोकन संबंधी अध्ययन विज्ञान है, न कि भौतिकी या रसायन विज्ञान की तरह एक प्रयोगात्मक अध्ययन। गणित के भीतर यह विवाद उसी समय उत्पन्न हो रहा है जब भौतिकी समुदाय में इस बारे में प्रश्न पूछे जा रहे हैं कि क्या इक्कीसवीं सदी का [[सैद्धांतिक भौतिकी]] बहुत अधिक गणितीय होता जा रहा है, और अपनी प्रायोगिक जड़ों को पीछे छोड़ रहा है।
 प्रायोगिक गणित का उभरता हुआ क्षेत्र गणितीय अन्वेषण के लिए अपने मुख्य उपकरण के रूप में संख्यात्मक प्रयोगों पर ध्यान केंद्रित करके इस बहस का सामना कर रहा है।
+== अनुप्रयोग                                                                         ==
-'''सी अर्थ में सभी संभावित गणितीय वस्तुएं पहले से मौजूद हैं, तो क्या कंप्यूटर-समर्थित गणित खगोल विज्ञान की तरह एक अवलोकन संबंधी अध्ययन विज्ञान है, न कि भौतिकी या रसायन विज्ञान की तरह एक प्रयोगात्मक अध्यय'''
+===कंप्यूटर प्रोग्राम की सहायता से प्रमेयों को सिद्ध किया ===
+इस सूची में सम्मिलित करने का अर्थ यह नहीं है कि एक औपचारिक कंप्यूटर-जाँच प्रमाण उपस्थित है चूँकि यह कि एक कंप्यूटर प्रोग्राम किसी तरह से सम्मिलित किया गया है। विवरण के लिए मुख्य लेख देखें।
-== अनुप्रयोग       ==
-===कंप्यूटर प्रोग्राम की मदद से प्रमेयों को सिद्ध किया ===
-इस सूची में सम्मिलित करने का अर्थ यह नहीं है कि एक औपचारिक कंप्यूटर-जाँच प्रमाण मौजूद है, बल्कि यह कि एक कंप्यूटर प्रोग्राम किसी तरह से सम्मिलित किया गया है। विवरण के लिए मुख्य लेख देखें।
 {{columns-list|colwidth=22em|1=* [[Four color theorem]], 1976
@@ Line 165: / Line 159: @@
 === बिक्री के लिए प्रमेय ===
-में, [[एडिनबर्ग विश्वविद्यालय]] के शिक्षाविदों ने लोगों को कंप्यूटर-सहायता प्रमाण के माध्यम से बनाए गए अपने स्वयं के प्रमेय को खरीदने का मौका दिया। इस नए प्रमेय को क्रेता के नाम पर रखा जाएगा।<ref>{{cite web|title=अपनी स्वयं की प्रमेय खरीदने पर हेराल्ड राजपत्र लेख|url=http://www.heraldscotland.com/news/education/your-own-maths-theorem-for-15-1.1068654|work=Herald Gazette Scotland|date=November 2010|url-status=dead|archive-url=https://web.archive.org/web/20101121000707/http://www.heraldscotland.com/news/education/your-own-maths-theorem-for-15-1.1068654|archive-date=2010-11-21}}</ref><ref>{{cite web|title=स्कूल ऑफ इंफॉर्मेटिक्स, यूनिवर्सिटी.ऑफ़ एडिनबर्ग वेबसाइट|url=http://www.ed.ac.uk/informatics/news-events/recentnews/theorem|work=School of Informatics, Univ.of Edinburgh|date=April 2015}}{{Dead link|date=July 2019 |bot=InternetArchiveBot |fix-attempted=yes }}</ref> ऐसा लगता है कि यह सेवा अब उपलब्ध नहीं है।
+में [[एडिनबर्ग विश्वविद्यालय]] के शिक्षाविदों ने लोगों को कंप्यूटर-सहायता प्रमाण के माध्यम से बनाए गए अपने स्वयं के प्रमेय को खरीदने का अवसर दिया। इस नए प्रमेय को क्रेता के नाम पर रखा जाएगा।<ref>{{cite web|title=अपनी स्वयं की प्रमेय खरीदने पर हेराल्ड राजपत्र लेख|url=http://www.heraldscotland.com/news/education/your-own-maths-theorem-for-15-1.1068654|work=Herald Gazette Scotland|date=November 2010|url-status=dead|archive-url=https://web.archive.org/web/20101121000707/http://www.heraldscotland.com/news/education/your-own-maths-theorem-for-15-1.1068654|archive-date=2010-11-21}}</ref><ref>{{cite web|title=स्कूल ऑफ इंफॉर्मेटिक्स, यूनिवर्सिटी.ऑफ़ एडिनबर्ग वेबसाइट|url=http://www.ed.ac.uk/informatics/news-events/recentnews/theorem|work=School of Informatics, Univ.of Edinburgh|date=April 2015}}{{Dead link|date=July 2019 |bot=InternetArchiveBot |fix-attempted=yes }}</ref> ऐसा लगता है कि यह सेवा अब उपलब्ध नहीं है।
 == यह भी देखें ==
-{{columns-list|colwidth=22em|
+{{columns-list|colwidth=22em|* [[औपचारिक सत्यापन]]
-* [[Formal verification]]
+* [[तर्क सिद्धांतकार]]
-* [[Logic Theorist]]
+* [[गणितीय प्रमाण]]
-* [[Mathematical proof]]
+* [[मेटामैथ]]
-* [[Metamath]]
+* [[मॉडल जाँच]]
-* [[Model checking]]
+* [[सत्रह या बस्ट]]
-* [[Seventeen or Bust]]
+* [[प्रतीकात्मक गणना]]
-* [[Symbolic computation]]
+* [[मान्य संख्याएँ]]}}
-* [[Validated numerics]]
-}}
 ==संदर्भ==
@@ Line 195: / Line 187: @@
 * {{cite web|title=A Special Issue on Formal Proof|url=https://www.ams.org/notices/200811/|work=Notices of the [[American Mathematical Society]]|date=December 2008}}
-{{Mathematical logic}}
+[[Category:All Wikipedia articles needing clarification]]
-{{Numerical PDE}}
+[[Category:All articles with dead external links]]
-[[Category: तर्क तकनीक]] [[Category: स्वचालित प्रमेय साबित करना]] [[Category: कंप्यूटर-सहायता प्राप्त प्रमाण]] [[Category: औपचारिक तरीके]] [[Category: संख्यात्मक विश्लेषण]] [[Category: गणित का दर्शन]]
+[[Category:Articles with dead external links from July 2019]]
+[[Category:Articles with hatnote templates targeting a nonexistent page]]
+[[Category:Articles with permanently dead external links]]
+[[Category:CS1 English-language sources (en)]]
-[[Category: Machine Translated Page]]
+[[Category:CS1 maint]]
 [[Category:Created On 30/05/2023]]
+[[Category:Lua-based templates]]
+[[Category:Machine Translated Page]]
+[[Category:Multi-column templates]]
+[[Category:Pages using div col with small parameter]]
+[[Category:Pages with script errors]]
+[[Category:Templates Vigyan Ready]]
+[[Category:Templates that add a tracking category]]
+[[Category:Templates that generate short descriptions]]
+[[Category:Templates using TemplateData]]
+[[Category:Templates using under-protected Lua modules]]
+[[Category:Wikipedia articles needing clarification from October 2020]]
+[[Category:Wikipedia fully protected templates|Div col]]
+[[Category:औपचारिक तरीके]]
+[[Category:कंप्यूटर-सहायता प्राप्त प्रमाण]]
+[[Category:गणित का दर्शन]]
+[[Category:तर्क तकनीक]]
+[[Category:संख्यात्मक विश्लेषण]]
+[[Category:स्वचालित प्रमेय साबित करना]]

Anonymous

Search

कंप्यूटर-सहायता प्रमाण: Difference between revisions

Namespaces

More

Page actions

Latest revision as of 11:50, 28 June 2023

Contents

विधि

दार्शनिक आपत्तियाँ

अनुप्रयोग

कंप्यूटर प्रोग्राम की सहायता से प्रमेयों को सिद्ध किया

बिक्री के लिए प्रमेय

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

कंप्यूटर-सहायता प्रमाण: Difference between revisions

Latest revision as of 11:50, 28 June 2023

विधि

दार्शनिक आपत्तियाँ

अनुप्रयोग

कंप्यूटर प्रोग्राम की सहायता से प्रमेयों को सिद्ध किया

बिक्री के लिए प्रमेय

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories