गणित हमेशा से दो अलग-अलग भाषाओं पर निर्भर रहा है। एक वह प्राकृतिक भाषा है जिसका उपयोग हम विचारों को समझाने, कहानियाँ सुनाने और अंतर्दृष्टि साझा करने के लिए करते हैं; यह लचीली है, संदर्भ से समृद्ध है, और अक्सर उन चरणों को छोड़ देती है जो एक मानव पाठक के लिए स्पष्ट लगते हैं। दूसरी भाषा 'प्रूफ असिस्टेंट्स' (proof assistants) की औपचारिक भाषा है, जो कठोर कंप्यूटर सिस्टम हैं जो किसी निष्कर्ष को निर्विवाद रूप से सत्य सुनिश्चित करने के लिए हर एक तार्किक कदम की जाँच करते हैं। दशकों से, शोधकर्ता पहली भाषा को दूसरी में अनुवाद करने पर काम कर रहे हैं, जिसे 'ऑटोफॉर्मलाइजेशन' (autoformalization) कहा जाता है। लक्ष्य सरल था: एक मानव-लिखित प्रमाण को लें और उसे ऐसे कोड में बदल दें जिसे कंप्यूटर सत्यापित कर सके। लेकिन एक महत्वपूर्ण समस्या बनी हुई थी। कंप्यूटर अक्सर एक ऐसा प्रमाण उत्पन्न कर सकता था जो तकनीकी रूप से सही तो था, लेकिन उसका मूल मानवीय तर्क से कोई मेल नहीं था। कंप्यूटर समस्या को पूरी तरह से अलग पथ का उपयोग करके हल कर सकता था, जिससे मूल तर्क को स्वचालित शॉर्टकट की दीवार के पीछे छिपा दिया जाता था। इसने सत्य और समझ के बीच एक अंतर पैदा कर दिया। यदि कंप्यूटर का प्रमाण मानव के चरणों का पालन नहीं करता है, तो हम यह जाँचने के लिए इसका उपयोग नहीं कर सकते कि क्या मानव का तर्क वास्तव में सुदृढ़ था, और न ही हम इस पर भरोसा कर सकते हैं कि वह हमें सिखाता है कि तर्क कैसे काम करता है।

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

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

इसे प्राप्त करने के लिए, शोधकर्ताओं ने एक विधि विकसित की जो अनुवाद प्रक्रिया को दो अलग-अलग चरणों में विभाजित करती है। पहले, एक 'मैपिंग चरण' (mapping phase) प्राकृतिक भाषा के पाठ का विश्लेषण करता है और इसे छोटे, परमाणु चरणों के अनुक्रम में विभाजित करता है। यह पहचानता है कि प्रत्येक वाक्य क्या दावा करता है और वह किन धारणाओं पर निर्भर है। यह एक सख्त टेम्पलेट बनाता है जिसका पालन कंप्यूटर को करना ही होता है। दूसरा, एक 'फिलिंग चरण' (filling phase) प्रत्येक इन छोटे चरणों को व्यक्तिगत रूप से सिद्ध करने का प्रयास करता है। सिस्टम एक विशेष खोज रणनीति का उपयोग करता है जो कंप्यूटर को शॉर्टकट लेने या आगे बढ़ने से रोकता है। यदि कंप्यूटर मानव पाठ में वर्णित सटीक उपकरणों और संदर्भों का उपयोग करके एक विशिष्ट चरण को सिद्ध नहीं कर पाता है, तो वह समस्या को हल करने का कोई अन्य तरीका खोजने के बजाय, समस्या को फ्लैग (flag) करता है, जिससे पता चलता है कि मूल मानव तर्क में कोई छेद या अधूरा हिस्सा हो सकता है।

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

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

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

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

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