🤖 AI

Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization

यह शोध पत्र लीन एटलस (Lean Atlas) का परिचय देता है, जो एक ओपन-सोर्स इंटरैक्टिव वेब टूल है जिसमें लीन कम्पास (Lean Compass) एल्गोरिदम है जो प्रोजेक्ट निर्भरताओं को विज़ुअलाइज़ करने और उन विशिष्ट परिभाषाओं और प्रमेयों की स्वचालित रूप से पहचान करने में सक्षम बनाता है जिन्हें मानव अर्थ संबंधी सत्यापन (semantic verification) की आवश्यकता होती है ताकि AI-जनित प्रमाणों में अर्थ संबंधी मतिभ्रम (semantic hallucinations) प्रदर्शित होने से रोका जा सके, जिससे गणित को औपचारिक बनाने में स्केलेबल मानव-AI सहयोग संभव हो सके।

मूल लेखक: Banri Yanahama, Akiyoshi Sannai

प्रकाशित 2026-04-21

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Banri Yanahama, Akiyoshi Sannai

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

यहाँ "Lean Atlas" पेपर का सरल भाषा और रचनात्मक उपमाओं (analogies) का उपयोग करके विवरण दिया गया है।

समस्या: "पूरी तरह से गलत" प्रमाण (The "Perfectly Wrong" Proof)

कल्पना कीजिए कि आपने अपने लिए एक कानूनी अनुबंध (legal contract) लिखने के लिए एक सुपर-फास्ट, सुपर-स्मार्ट रोबोट को काम पर रखा है। रोबोट एक ऐसा दस्तावेज़ टाइप करता है जो व्याकरण की दृष्टि से एकदम सटीक (grammatically perfect) है। हर वाक्य अंग्रेजी के नियमों का पालन करता है, विराम चिह्न सही हैं, और फॉर्मेटिंग त्रुटिहीन है। एक स्पेल-चेकर इसे 100% स्कोर देगा।

हालाँकि, रोबोट ने एक सूक्ष्म गलती की है: उसने सबसे महत्वपूर्ण क्लॉज में "खरीदार" (buyer) शब्द को "विक्रेता" (seller) से बदल दिया है। दस्तावेज़ अभी भी "व्याकरणिक रूप से सही" है, लेकिन इसका अर्थ वही है जो आप चाहते थे उसका ठीक उल्टा। गणित और कंप्यूटर विज्ञान की दुनिया में, इसे सिमेंटिक हैलुसिनेशन (Semantic Hallucination) कहा जाता है।

पेपर में, लेखक बताते हैं कि AI औपचारिक गणितीय प्रमाण (एक टूल जिसे Lean कहा जाता है) लिखने में बहुत अच्छा हो रहा है। कंप्यूटर का "स्पेल-चेकर" (जिसे Type Checker कहा जाता है) यह बता सकता है कि तर्क (logic) सही ढंग से जुड़ा हुआ है या नहीं। लेकिन यह यह नहीं बता सकता कि गणित वास्तव में वह मतलब निकाल रहा है जो इंसान चाहता था। AI एक ऐसा कथन सिद्ध कर सकता है जो तार्किक रूप से तो सत्य है, लेकिन गणितीय रूप से निरर्थक (nonsense) है।

समाधान: मानव-इन-द-लूप (The Human-in-the-Loop)

लेखक काम करने का एक नया तरीका प्रस्तावित करते हैं: इंसान और AI एक टीम के रूप में।

AI भारी काम करता है: कोड लिखना, तर्क की जाँच करना और संरचना बनाना।
इंसान एक "मीनिंग इंस्पेक्टर" (अर्थ निरीक्षक) के रूप में कार्य करता है। वे कोड की हर एक लाइन की जाँच नहीं करते (जिसमें बहुत समय लगेगा); वे केवल उन हिस्सों की जाँच करते हैं जो यह निर्धारित करते हैं कि गणित वास्तव में क्या कहता है।

लेकिन हजारों लाइनों के कोड वाले एक विशाल प्रोजेक्ट में आप कैसे जानेंगे कि किन हिस्सों की जाँच करनी है? यहीं Lean Atlas काम आता है।

टूल: Lean Atlas (द "मैप")

एक बड़े गणितीय प्रोजेक्ट को ऊन के एक विशाल, उलझे हुए गोले की तरह समझें। हर धागा (एक परिभाषा या प्रमेय/theorem) कई अन्य धागों से जुड़ा होता है। यदि आप एक धागा खींचते हैं, तो वह दर्जनों अन्य धागों को भी खींच सकता है।

Lean Atlas इस ऊन को सुलझाता है और कनेक्शन का एक नक्शा (map) बनाता है।

यह प्रोजेक्ट को एक इंटरैक्टिव वेब के रूप में विज़ुअलाइज़ करता है।
यह दो प्रकार के कनेक्शनों के बीच अंतर करता है:
1. "क्या" (Type Dependencies): ये वे परिभाषाएँ और अवधारणाएँ हैं जो गणित को उसका अर्थ देती हैं। (जैसे, "'अभाज्य संख्या' (prime number) क्या है?")
2. "कैसे" (Value Dependencies): ये कुछ सच होने को सिद्ध करने के लिए उठाए गए विशिष्ट चरण हैं। (जैसे, "यहाँ 2 अभाज्य है, इसे सिद्ध करने के लिए चरण-दर-चरण गणना दी गई है।")

जादुई ट्रिक: Lean Compass (द "फिल्टर")

यह इस पेपर का सबसे चतुर विचार है।

कल्पना कीजिए कि आप उस ऊन के विशाल गोले के बीच में एक विशिष्ट प्रमेय (एक विशिष्ट दावा) को देख रहे हैं। आप जानना चाहते हैं: "यदि मैं इस परिभाषा को बदल दूँ, तो क्या यह मेरे प्रमेय के अर्थ को बिगाड़ देगा?"

आमतौर पर, आपको उससे जुड़े हर एक धागे को देखना होगा। लेकिन Lean Compass एक स्मार्ट फिल्टर है। यह एक सरल नियम का उपयोग करता है:

"यदि कोई कनेक्शन एक प्रमाण (the 'How') से आता है, तो हम अभी के लिए उसे अनदेखा कर सकते हैं। कंप्यूटर पहले ही जाँच चुका है कि प्रमाण तार्किक है। हमें केवल उन कनेक्शनों की चिंता करने की आवश्यकता है जो परिभाषाओं (the 'What') से आते हैं।"

उपमा (Analogy):
कल्पना कीजिए कि आप सुरक्षा के लिए एक घर का निरीक्षण कर रहे हैं।

"प्रमाण" (Proofs) वे मजदूर हैं जिन्होंने दीवारें बनाई हैं। यदि मजदूरों ने खराब काम किया, तो दीवार गिर सकती है, लेकिन ब्लूप्रिंट (डिज़ाइन) अभी भी सही है। कंप्यूटर मजदूरों की जाँच करता है।
"परिभाषाएँ" (Definitions) ब्लूप्रिंट हैं। यदि ब्लूप्रिंट कहता है "यह एक खिड़की है" लेकिन वास्तुकार का मतलब "यह एक दरवाजा है" था, तो घर गलत बना है, भले ही मजदूरों ने ब्लूप्रिंट का पूरी तरह से पालन किया हो।

Lean Compass आपको बताता है: "मजदूरों के चरणों की जाँच करने में समय बर्बाद न करें। बस ब्लूप्रिंट और दरवाजों की जाँच करें।"

इन "प्रमाण चरणों" (proof steps) को फ़िल्टर करके, Lean Compass कई मामलों में एक इंसान द्वारा जाँच किए जाने वाले चीजों की सूची को 90% या उससे अधिक कम कर देता है।

परिणाम: यह कितना अच्छा काम करता है?

लेखकों ने छह अलग-अलग प्रोजेक्ट्स पर इसका परीक्षण किया, जिनमें शुद्ध गणित से लेकर भौतिकी और क्रिप्टोग्राफी तक शामिल हैं।

"प्रमाण-भारी" (Proof-Heavy) प्रोजेक्ट्स: (जैसे कि प्राइम नंबर थ्योरम)। ये उन घरों की तरह हैं जिनमें हजारों मजदूर हैं लेकिन ब्लूप्रिंट सरल है। Lean Compass ने एक वैक्यूम क्लीनर की तरह काम किया, जिससे 94-99% कचरा साफ हो गया। इंसानों को केवल बचे हुए छोटे से हिस्से को देखना पड़ा।
"परिभाषा-भारी" (Definition-Heavy) प्रोजेक्ट्स: (जैसे कि एक जटिल क्रिप्टोग्राफिक सिग्नेचर)। ये उन घरों की तरह हैं जिनके ब्लूप्रिंट बहुत जटिल और बदलते रहते हैं। यहाँ, "ब्लूप्रिंट" (परिभाषाएँ) मुख्य घटना है, इसलिए फिल्टर उतना अधिक हिस्सा नहीं हटा सका (केवल लगभग 27% की कमी)। लेकिन इसने मदद भी की।
मिश्रित (Mixed) प्रोजेक्ट्स: (जैसे फर्मा का अंतिम प्रमेय/Fermat's Last Theorem)। कुछ हिस्से फ़िल्टर करने में आसान थे, कुछ कठिन। इससे सिद्ध हुआ कि टूल प्रोजेक्ट की संरचना के अनुसार खुद को ढाल लेता है।

बड़ा विचार: "Aligned Lean Code"

यह पेपर एक नया गुणवत्ता मानक पेश करता जिसे Aligned Lean Code कहा जाता है।

तार्किक शुद्धता (Logical Correctness): कंप्यूटर कहता है, "यह प्रमाण मान्य है।"
सिमेंटिक शुद्धता (Semantic Correctness): एक इंसान कहता है, "इस प्रमाण का वही अर्थ है जो हम चाहते थे।"

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

सारांश

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

यहाँ शोध पत्र "Lean Atlas: Scalable Human-AI Collaborative Formalization के लिए एक Integrated Proof Environment" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण: AI Formalization में Semantic Hallucination (अर्थ संबंधी भ्रम)

यद्यपि AI-संचालित ऑटोफॉर्मलाइजेशन (autoformalization) तेजी से आगे बढ़ रहा है, लेकिन तार्किक शुद्धता (logical correctness) और अर्थगत शुद्धता (semantic correctness) के बीच एक महत्वपूर्ण अंतर मौजूद है।

सीमा: प्रूफ़ असिस्टेंट (जैसे Lean 4) यह गारंटी देते हैं कि एक प्रूफ़ टर्म दिए गए प्रपोजिशन (proposition) के लिए तार्किक रूप से निर्मित है (type checking)। हालाँकि, वे यह सत्यापित नहीं कर सकते कि प्रपोजिशन या उसकी परिभाषाएँ इच्छित गणितीय अर्थ को निष्ठापूर्वक पकड़ती हैं या नहीं।
Semantic Hallucination: यह तब होता है जब AI-जनरेटेड फॉर्मलाइजेशन टाइप चेकर को पास कर देता है और सिद्ध करने योग्य होता है, फिर भी मूल गणितीय कथन का प्रतिनिधित्व करने में विफल रहता है। सामान्य पैटर्न में परिभाषाओं का बेमेल होना (definition mismatches), धारणाओं का छूटना (missing assumptions), लक्ष्य प्रतिस्थापन (goal substitution), और टाइप डिफॉल्ट शिफ्ट (type default shifts) शामिल हैं।
चुनौती: जैसे-जैसे AI बड़े पैमाने पर प्रूफ़ जनरेट करता है, यदि समीक्षकों को पूरे प्रोजेक्ट के डिपेंडेंसी ग्राफ (dependency graph) का निरीक्षण करना पड़े, तो मानव समीक्षा अव्यवहार्य हो जाती है। एक ऐसे वर्कफ़्लो की आवश्यकता है जो कुशलतापूर्वक उन विशिष्ट घोषणाओं (declarations) को अलग कर सके जिन्हें मानव अर्थगत सत्यापन (semantic verification) की आवश्यकता है।

2. कार्यप्रणाली: Lean Atlas और Lean Compass

लेखक एक human-in-the-loop दृष्टिकोण प्रस्तावित करते हैं जहाँ AI तार्किक निर्माण (logical construction) को संभालता है, और मानव वैज्ञानिक अर्थगत शुद्धता (semantic correctness) को सत्यापित करते हैं। इसे दो मुख्य घटकों के माध्यम through साकार किया गया है:

A. Lean Atlas (The Environment)

Lean Atlas, Lean 4 प्रोजेक्ट्स के लिए एक इंटरैक्टिव वेब व्यूअर और बैकएंड टूल है।

Dependency Graph Extraction: यह Lean 4 एनवायरनमेंट को ट्रैवर्स करता है ताकि कॉन्स्टेंट्स (theorems, definitions, inductive types, आदि) और उनकी निर्भरताओं (dependencies) को निकाला जा सके।
वर्गीकरण (Classification): यह निर्भरताओं को दो अलग-अलग श्रेणियों में वर्गीकृत करता है:
1. Type Dependencies: ऐसे संबंध जहाँ एक कॉन्स्टेंट दूसरे के 'टाइप सिग्नेचर' में दिखाई देता है (जैसे, एक प्रमेय के प्रपोजिशन में उपयोग की गई परिभाषा)। ये अर्थगत अर्थ के लिए महत्वपूर्ण हैं।
2. Value Dependencies: ऐसे संबंध जहाँ एक कॉन्स्टेंट केवल 'इम्प्लीमेंटेशन/वैल्यू' में दिखाई देता है (जैसे, एक प्रमेय का प्रूफ़ टर्म)।
विज़ुअलाइज़ेशन: यह डिपेंडेंसी ग्राफ को एक इंटरैक्टिव वेब व्यूअर के रूप में विज़ुअलाइज़ करता है, जिससे उपयोगकर्ताओं को एज के प्रकार (edge kind), कॉन्फिडेंस और प्रूफ़ स्टेटस के आधार पर फ़िल्टर करने की अनुमति मिलती है।

B. Lean Compass (The Algorithm)

Lean Compass एक कोर एल्गोरिदम है जिसे मानव समीक्षा के दायरे को कम करने के लिए डिज़ाइन किया गया है।

मुख्य अंतर्दृष्टि: यह वैल्यू डिपेंडेंसीज में एक विषमता (asymmetry) का लाभ उठाता है:
- Theorem के proof से उत्पन्न होने वाली Value dependencies: ये टाइप चेकर द्वारा गारंटीकृत होती हैं (तार्किक शुद्धता) और इन्हें अर्थगत समीक्षा के लिए प्रून (prune/हटाया) किया जा सकता है।
- Definition के implementation से उत्पन्न होने वाली Value dependencies: इनमें कम्प्यूटेशनल सामग्री हो सकती है जो टाइप सिग्नेचर में प्रतिबिंबित नहीं होती है, इसलिए इन्हें रखा (retain) जाना चाहिए।
एल्गोरिदम:
1. इनपुट: एक डिपेंडेंसी ग्राफ $G$ और एक लक्षित सेट $M$ ।
2. Pruning Rule: वे किनारे (edges) जहाँ स्रोत एक theorem है और डिपेंडेंसी साइट value है (अर्थात, प्रूफ़-स्तरीय निर्भरताएँ), उन्हें हटा दिया जाता है।
3. Reachability: प्रून किए गए ग्राफ पर $M$ से शुरू होकर एक Breadth-First Search (BFS) किया जाता है ताकि सभी सुलभ नोड्स (reachable nodes) को पाया जा सके।
4. आउटपुट: एक "Review Cone" जिसमें केवल प्रोजेक्ट-विशिष्ट नोड्स होते हैं जिनकी अर्थगत शुद्धता लक्षित प्रमेयों को प्रभावित कर सकती है।
Edge Classification: सिस्टम को Source Kind $\times$ Dependency Site $\times$ Target Kind के आधार पर 8 प्रकारों में वर्गीकृत किया गया है। केवल किनारे #3 और #4 (theorem $\to$ value $\to$ definition/theorem) को हटाया जाता है।

3. प्रमुख योगदान

"Aligned Lean Code" की अवधारणा: लेखकों ने उस फॉर्मलाइजेशन कोड को "एलाइंड" (aligned) के रूप में परिभाषित किया है जो मानव अर्थगत सत्यापन से गुजरा है। इस कोड में तार्किक शुद्धता (टाइप चेकर से) और अर्थगत शुद्धता (मानव समीक्षा से) दोनों होती है, जो AI-जनरेटेड फॉर्मलाइजेशन के लिए एक नया गुणवत्ता मानक है।
Lean Atlas टूल: एक अभिनव टूल जो विशेष रूप से टाइप बनाम वैल्यू डिपेंडेंसीज को अलग करने पर ध्यान केंद्रित करते हुए डिपेंडेंसी ग्राफ को विज़ुअलाइज़ करता है, जिससे कुशल मानव निरीक्षण सक्षम होता है।
Lean Compass एल्गोरिदम: बड़े पैमाने के प्रोजेक्ट्स में मानव समीक्षा के लिए आवश्यक नोड्स के न्यूनतम सेट को स्वचालित रूप से निकालने का एक स्केलेबल तरीका।

4. परिणाम और मूल्यांकन

टूल का मूल्यांकन विभिन्न संरचनात्मक विशेषताओं वाले छह विविध Lean 4 प्रोजेक्ट्स पर किया गया। प्राथमिक मीट्रिक नोड रिडक्शन रेट (node reduction rate) (डिपेंडेंसी ग्राफ का वह प्रतिशत जिसे हटाया गया) था।

प्रोजेक्ट प्रकार	प्रोजेक्ट का नाम	विशेषताएँ	औसत रिडक्शन (Average Reduction)
Proof-Heavy	PrimeNumberTheoremAnd	8 मुख्य प्रमेय	94–99%
Proof-Heavy	Carleson	9 मुख्य प्रमेय (बड़े पैमाने पर)	96.2%
Proof-Heavy	Brownian Motion	5 मुख्य प्रमेय	94.4%
Mixed	FLT (Fermat's Last Theorem)	6 मील का पत्थर प्रमेय	59.8%
Mixed	PhysLib	सैद्धांतिक भौतिकी (QM, GR, आदि)	69.0%
Definition-Heavy	XMSS	क्रिप्टोग्राफी (Hash-based signatures)	27.3%

मुख्य निष्कर्ष:

संरचनात्मक निर्धारक (Structural Determinant): रिडक्शन रेट "रिव्यू कोन" (review cone) के भीतर theorem-to-definition अनुपात द्वारा निर्धारित होता है, न कि प्रोजेक्ट के आकार या डोमेन द्वारा।
उच्च रिडक्शन: प्रूफ-हेवी प्रोजेक्ट्स में, एल्गोरिदम बड़ी मात्रा में प्रूफ़-स्तरीय निर्भरताओं को सफलतापूर्वक हटा देता है (उदाहरण के लिए, Brownian Motion में 227-नोड वाले कोन को 14 नोड्स तक कम करना)।
कम रिडक्शन: परिभाषा-प्रधान प्रोजेक्ट्स (जैसे XMSS) में, परिभाषाओं से उत्पन्न होने वाली वैल्यू डिपेंडेंसीज को रखना पड़ता है क्योंकि वे कम्प्यूटेशनल अर्थ (computational semantics) ले जाती हैं, जिसके परिणामस्वरूप कम रिडक्शन रेट मिलता है।
क्रॉस-डोमेन प्रयोज्यता: यह दृष्टिकोण गैर-गणितीय डोमेन, जैसे सैद्धांतिक भौतिकी (PhysLib) और क्रिप्टोग्राफी (XMSS) में भी प्रभावी साबित हुआ, जो दर्शाता है कि 'semantic hallucination' एक सामान्य समस्या है।

5. महत्व

स्केलेबिलिटी (Scalability): Lean Compass, तार्किक रूप से सत्यापित लेकिन अर्थगत रूप से अप्रासंगिक कोड को फ़िल्टर करके बड़े पैमाने के AI-जनरेटेड फॉर्मलाइजेशन के लिए मानव-इन-द-लूप सत्यापन को संभव बनाता है।
गुणवत्ता मानक: "Aligned Lean code" की अवधारणा AI-सहायता प्राप्त गणित के लिए एक ठोस लक्ष्य प्रदान करती है: ऐसा कोड जो न केवल सिद्ध करने योग्य है, बल्कि सार्थक भी है।
डोमेन एग्नोस्टिक (Domain Agnosticism): टाइप-चेकर वैधता और इच्छित अर्थशास्त्र के बीच के अंतर को संबोधित करके, यह फ्रेमवर्क किसी भी डोमेन पर लागू होता है जिसमें प्रूफ़ असिस्टेंट का उपयोग किया जाता है, जिसमें क्रिप्टोग्राफी और भौतिकी शामिल हैं, जहाँ डोमेन-विशिष्ट परिभाषाएँ सामान्य प्रूफ़ असिस्टेंट के लिए अपरिचित हो सकती हैं।
भविष्य का इंफ्रास्ट्रक्चर: यह शोध पत्र "एलाइंड" कोड के संग्रह के लिए आधार तैयार करता है, जो भविष्य के AI मॉडल के लिए उच्च-गुणवत्ता वाले प्रशिक्षण डेटा और गणितज्ञों के लिए एक विश्वसनीय संदर्भ के रूप में कार्य कर सकता है।

सीमाएँ और भविष्य का कार्य:
वर्तमान मूल्यांकन समय की बचत के प्रॉक्सी के रूप में नोड रिडक्शन पर निर्भर करता है; वास्तविक मानव सत्यापन समय में कमी को अभी तक मापा नहीं गया है। भविष्य के कार्यों में AI के माध्यम से कॉन्फिडेंस मेटाडेटा जनरेशन को स्वचालित करना और व्यापक वैज्ञानिक डोमेन में मूल्यांकन का विस्तार करना शामिल है।