5
अधिकांश सबूत सहायक आश्रित प्रकार के साथ कार्यात्मक प्रोग्रामिंग भाषाएं हैं। वे कार्यक्रम/एल्गोरिदम प्रमाणित कर सकते हैं। मुझे दिलचस्पी है, इसके बजाय, सबूत सहायक में गणित के लिए सर्वश्रेष्ठ उपयुक्त है और केवल (उदाहरण के लिए कैलकुस)। क्या आप एक की सिफारिश कर सकते हैं? मैंने मिजर के बारे में सुना लेकिन मुझे यह पसंद नहीं है कि स्रोत कोड बंद है, लेकिन अगर यह गणित के लिए सबसे अच्छा है तो मैं इसका इस्तेमाल करूंगा। Agda और Idris जैसे नई भाषा गणितीय सबूत के लिए कितनी अच्छी तरह उपयुक्त हैं?गणित के लिए सबूत सहायक केवल
में शामिल किया गया था मैं अपने जवाब से मान सकते हैं कि AGDA गणितीय प्रमाणों लिए उपयुक्त नहीं है? –
पिछले 4 वर्षों से मेरे सभी काम (प्रोग्रामिंग और साबित करने के इंटरफ़ेस पर) Agda में किया गया है। और एजदा में पूरी तरह से बड़ी औपचारिकता परियोजनाएं पूरी की जाती हैं। लेकिन कोक को कुछ कष्टप्रद सबूतों को स्वचालित करने के उद्देश्य से बहुत सारे कामों से लाभ होता है (उदाहरण के लिए अंगूठियां, खेतों, आदि से निपटने के दौरान सभी (इन) समानताएं)। अंत में, उत्तर इस बात पर निर्भर करेगा कि आप किस तरह के गणित करना चाहते हैं। – gallais