Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem

तकनीकी सारांश: अरस्तू (Aristotle) API का उपयोग करके ग्रासहॉपर समस्या का एक औपचारिकीकरण केस स्टडी

समस्या विवरण
यह शोध पत्र "ग्रासहॉपर समस्या" (Grasshopper problem) के एक औपचारिकीकरण केस स्टडी को प्रस्तुत करता है, जिसे मूल रूप से 50वें अंतर्राष्ट्रीय गणितीय ओलंपियाड (IMO 2009) की समस्या 6 के रूप में प्रस्तुत किया गया था। यह प्रमेय बताता है कि $n$ अलग-अलग धनात्मक पूर्णांकों $\{a_1, \dots, a_n\}$ के किसी भी सेट और $n-1$ धनात्मक पूर्णांकों के एक सेट $M$ के लिए (जहाँ कुल योग $\sum a_i \notin M$), जंप्स (jumps) के एक क्रम (permutation) $\sigma$ का अस्तित्व होता है, जिससे कोई भी मध्यवर्ती आंशिक योग (intermediate partial sum) $S_k = \sum_{i=1}^k a_{\sigma(i)}$, $M$ में नहीं आता है। इस समस्या को इसके ऐतिहासिक कठिन स्तर के लिए नोट किया गया है, जिसका औसत स्कोर 2009 के सभी IMO प्रश्नों में सबसे कम था, और इसमें क्रमपरिवर्तन (permutations) और वर्जित सेट्स (forbidden sets) से संबंधित गैर-तुच्छ कॉम्बिनेटोरियल तर्क की आवश्यकता होती है।

कार्यप्रणाली
यह अध्ययन अरस्तू API (Aristotle API) का उपयोग करता है, जो एक स्वचालित प्रमेय-सिद्ध करने वाली प्रणाली है जो भाषा-मॉडल-निर्देशित खोज, अनौपचारिक लेम्मा जनरेशन, और Lean 4 प्रूफ़ असिस्टेंट (Mathlib का उपयोग करते हुए) के भीतर औपचारिकीकरण को जोड़ती है। लेखकों ने अरस्तू API को ग्रासहॉपर समस्या के एक कठोर, पूर्ण प्रमाण के लिए एक विशिष्ट प्रॉम्प्ट प्रदान किया, जिसमें समस्या को एक ज्ञात प्रमेय के रूप में उद्धृत करने को स्पष्ट रूप से वर्जित किया गया था और एक वैध क्रम (permutation) के निर्माण की मांग की गई थी।

परिणामस्वरूप प्राप्त आर्टिफैक्ट (artefact) एक Lean 4 प्रोजेक्ट है जिसमें प्रमेय का एक सामान्यीकृत संस्करण (जो $|M| < n$ की अनुमति देता है, न कि सख्ती से $n-1$, और $0 \in M$ की अनुमति देता है) शामिल है। लेखकों ने पूरी तरह से मशीन-सत्यापित घोषणाओं और अनसुलझे प्रमाण प्लेसहोल्डर्स (sorry) वाले घोषणाओं के बीच अंतर करने के लिए उत्पन्न कोड का सूक्ष्म निरीक्षण किया।

मुख्य परिणाम और सत्यापित घटक
जेनरेट किए गए Lean विकास ने मुख्य प्रमेय का पूर्ण प्रमाण उत्पन्न नहीं किया। इसके बजाय, यह चार पूरी तरह से सत्यापित सहायक लेम्मा और एक अनसुलझे मुख्य प्रमेय से युक्त एक हाइब्रिड आर्टिफैक्ट के रूप में सामने आया:

1. सत्यापित स्थानीय घटक:

   • PS last: यह सत्यापित किया गया कि अंतिम आंशिक योग जंप्स का कुल योग है।
   • PS swap: यह सत्यापित किया गया कि जंप्स का एक आसन्न ट्रांसपोज़िशन (adjacent transposition) केवल उस विशिष्ट स्थिति पर प्रभाव डालता है, और अन्य सभी को अपरिवर्तित छोड़ देता है।
   • PS swap eq: स्वैप के बाद बदले हुए आंशिक योग के बीजगणितीय रूप को सत्यापित किया गया ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$)।
   • maximizer swap in M: एक स्थानीय व्यापकता (local maximality) तर्क को सत्यापित किया गया। यह स्थापित करता है कि यदि एक क्रम $\sigma$ एक विशिष्ट स्कोर फंक्शन $G(\sigma)$ को अधिकतम करता है, और एक स्वैपेबल स्थिति पर एक आंशिक योग $M$ में है, तो स्वैप से प्राप्त मान भी $M$ में होगा।

2. अनसुलझा वैश्विक घटक:

   • मुख्य प्रमेय, grasshopper, सीधे एक एकल sorry द्वारा बंद किया गया है।
   • अरस्तू आउटपुट सारांश लुप्त चरण के रूप में एक वैश्विक गणना तर्क (global counting argument) की पहचान करता है। जबकि स्थानीय लेम्मा यह स्थापित करते हैं कि विशिष्ट स्वैप $M$ में सदस्यता को मजबूर करते हैं, सिस्टम इन तथ्यों को समन्वयित करने में विफल रहा कि वे कम से कम $n$ विशिष्ट वर्जित मान उत्पन्न करते हैं, जो इस धारणा का खंडन करेगा कि $|M| < n$। Lean स्रोत मुख्य प्रमेय को एक अलग, एन्कोडेड काउंटिंग लेम्मा तक कम नहीं करता है; अंतराल (gap) एक अप्राप्त दायित्व के रूप में बना हुआ है।

योगदान
यह शोध पत्र दो प्राथमिक योगदान देता है:

1. एक पुनरुत्पादक आर्टिफैक्ट (A Reproducible Artefact): यह एक निरीक्षण योग्य, पुनरुत्पादक Lean 4 औपचारिकीकरण प्रयास प्रदान करता है, जिसमें अरस्तू API का उपयोग करके एक कठिन ओलंपियाड कॉम्बिनेटोरिक्स समस्या को हल करने का प्रयास किया गया है, जिसमें पूर्ण सोर्स कोड और रन लॉग शामिल हैं।
2. AI सीमाओं का सटीक विश्लेषण: यह AI-जनित प्रमाणों के "साक्ष्य संबंधी स्थिति" (evidential status) का विस्तृत विच्छेदन करता है। अध्ययन दर्शाता है कि AI सिस्टम सफलतापूर्वक स्थानीय, बीजगणितीय और एक्सचेंज-आधारित तर्क चरणों को सत्यापित कर सकते हैं, लेकिन मुख्य प्रमेय को बंद करने के लिए आवश्यक वैश्विक कॉम्बिनेटोरियल बुककीपिंग (bookkeeping) को निष्पादित करने में विफल रहते हैं।

महत्व और दावे
यह शोध पत्र तर्क देता है कि "सत्यापित घोषणाओं" और "sorry द्वारा बंद घोषणाओं" के बीच का अंतर AI-सहायता प्राप्त प्रमेय सिद्ध करने की व्याख्या के लिए महत्वपूर्ण है। इस केस स्टडी का महत्व यह प्रदर्शित करने में निहित है कि स्थानीय प्रमाण खोज सफल हो सकती है जबकि वैश्विक तर्क अनसुलझा रहता है।

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