संगणक आपसूक तपासू शकेल अशा पद्धतीने गणिती ज्ञानाची निर्मिती, चाळणी आणि मांडणी करणे हा त्याचा मुख्य उद्देश होता.
ग्रंथ आणि शोधलेख या गणित साहित्याचे सखोल वर्गीकरण, अंकीय माहितीसाठानिर्मिती आणि सुलभतेने शोध घेण्याच्या पद्धती विकसित करणे हा गणित ज्ञान व्यवस्थापनाचा एक उद्देश बहुतांशी साध्य झाला आहे. त्याच्या जोडीला अशा साहित्यात मांडलेल्या गणिती ज्ञानाच्या संवर्धनासाठी काही प्राथमिक संगणकीय प्रणालीही विकसित झाल्या; पण कालांतराने त्य मागे पडल्या. यासंदर्भात १९७३ मध्ये ‘मायझर’ (टकेअफ) नावाचा प्रकल्प पोलंडमधील गणितज्ञ व संगणकशास्त्रज्ञ अ‍ॅण्डेज त्रिब्युलेक (१९४१-२०१३) यांनी हाती घेतला, जो आजही सुरू आहे. संगणक आपसूक तपासू शकेल अशा पद्धतीने गणिती ज्ञानाची निर्मिती, चाळणी आणि मांडणी करणे हा त्याचा मुख्य उद्देश होता. यासाठी ‘मायझर’ ही एक खास संगणकीय भाषा विकसित केली गेली. त्या भाषेत लिहिलेला शोधलेख तपासून संगणक गणिती त्रुटी दाखवू शकतो, नवी सिद्धता देण्यास मदत करू शकतो. या कार्याकरता ‘मायझर प्रूफचेकर’ नावाची खास आज्ञावली निर्माण केली गेली. अर्थातच मायझर भाषेत मांडलेल्या लेखांची लांबी वाढते, कारण आपल्यासाठी अगदी क्षुल्लक असलेली बाबदेखील संगणकाला तार्किकदृष्टय़ा स्पष्ट असावी लागते. ही भाषा केवळ मूलभूत संच सिद्धांत आणि विधेय (प्रेडिकेट) तर्कशास्त्रावर आधारलेली असल्याने ती सरावाने आत्मसात करणे फारसे कठीण नाही. या प्रकल्पात संगणकाच्या संदर्भासाठी गणिती व्याख्या, पायाभूत संरचना, पद्धती व सिद्धता यांचा समावेश असलेले अंकीय ग्रंथालय उभारले गेले आहे.
अनेक गणितज्ञांच्या सहकार्याने उभारलेले ‘मायझर गणिती ग्रंथालय’ हे सर्वात मोठे, विशुद्ध, काटेकोर औपचारिक गणित ज्ञानाचे अंकीय ग्रंथालय म्हणून ख्यातनाम आहे. त्यात ९,४०० संकल्पनांच्या व्याख्या आणि ४९,०००हून अधिक प्रमेये संग्रहित आहेत. या अंकीय ग्रंथालयाचा वापर विनाशुल्क करता येतो. (http://mizar.org/). सध्या हा प्रकल्प पोलंडचे बायस्टोक विद्यापीठ, कॅनडाचे अल्बर्टा विद्यापीठ आणि जपानचे शिन्षु विद्यापीठ येथील गणिती गट संयुक्तपणे संचालित करीत आहेत. गणिती प्रमेयांच्या सिद्धतांची तपासणी संगणक आपसूक करू शकेल अशा पंधराहून अधिक ‘सिद्धता साहाय्यक’ (प्रूफ असिस्टंट) प्रणाली सध्या कार्यरत आहेत. उदा. सीओक्यू, एचओएल, पीव्हीएस. या प्रणालींची कार्यपद्धती, विस्तार आणि मर्यादा याबाबतही संशोधन होत असून, त्या अधिक सक्षम केल्या जात आहेत. एकूण संगणकाधारित औपचारिक सिद्धता देणे वा तपासणे मोठय़ा प्रमाणात वाढण्याचे संकेत आहेत. मागील ५० वर्षांतील अशा आज्ञावलींची मूलभूत माहिती जतन करणारी ‘प्रमेय सिद्धता संग्रहालय’ नावाची एक अंकीय संचयिका (रिपॉझिटरी) स्थापित केली गेली आहे. (https://theoremprover-museum.github.io/). गणिती ज्ञानाच्या या एका नव्या दालनाचा लाभ संशोधकांना होत आहे.
– डॉ. विवेक पाटकर
मराठी विज्ञान परिषद
संकेतस्थळ : www.mavipa.org
ईमेल : office@mavipamumbai.org
Ref : Loksatta
