Ethereum के को-फाउंडर Vitalik Buterin ने एक नया प्रोग्रामिंग लैंग्वेज प्रपोज किया है। यह डायरेक्टली Lean या HOL जैसे formal proof assistant में कंपाइल हो सकती है।
यह आइडिया खास तौर पर उस गैप को टारगेट करता है जो लोग AI आउटपुट को पढ़ते समय फेस करते हैं। आजकल आर्टिफिशियल इंटेलिजेंस बड़े-बड़े automated proofs बहुत तेजी से तैयार कर रही है, जो किसी भी इंसानी टीम से कई गुना तेज है। लेकिन बहुत कम रीडर्स तुरंत पता लगा सकते हैं कि ये proofs असल में क्या साबित कर रहे हैं।
AI Proof Readers के लिए बनाया गया एक लैंग्वेज
Lean एक proof assistant है — ऐसा सॉफ्टवेयर जिसे mathematicians और engineers use करते हैं ताकि proofs ऐसे लिखें जिन्हें कंप्यूटर एक-एक लाइन check कर सके। Ethereum के researchers भी इसका यूज़ cryptographic code और consensus logic verify करने के लिए करते हैं। Proof assistants पिछले लगभग 60 सालों से exist कर रहे हैं, फिर भी यह अभी भी niche community तक ही सीमित है।
अपने पोस्ट में, Buterin ने कहा कि proof के internal steps का सिर्फ एक ही रूल है – मैथेमैटिकल करेक्टनेस। इसके अलावा और कुछ खास मायने नहीं रखता। रीडर्स कभी भी उस मशीनरी को डायरेक्ट इंस्पेक्ट नहीं करते। Definitions और theorems अलग तरीके से वर्क करते हैं, क्योंकि इन्हें इंसान पढ़ते हैं ताकि पता चले कि वह सॉफ्टवेयर रियल में क्या गारंटी करता है।
Buterin ने इसी से जुड़ी बात अपने मई के ब्लॉग पोस्ट में भी एक्सप्लोर की थी। वहां मैथमेटिकल प्रूफ से दिखाया गया कि efficient low-level कोड एक readable specification से perfectly मैचे करता है, जिससे एक single ऑडिट दोनों versions को एकसाथ कवर कर लेता है।
Vitalik का ये कदम Ethereum के अपने नए rebuild प्रोजेक्ट के टाइमलाइन के साथ भी जुड़ा है, जिसे Lean Ethereum roadmap भी कहा जाता है। दूसरी तरफ researchers एक formally verified ZK-EVM बना रहे हैं — यानी Ethereum के EVM का zero-knowledge-provable वर्जन — जिसमें ये तकनीक इस्तेमाल हो रही है।
AI proofs लिखता है, इंसान क्लेम्स को चेक करते हैं
आज के बड़े language models पहले से ही काम के Lean proofs लिख सकते हैं। Buterin ने Claude और Deepseek 4 Pro को यूजफुल टूल बताया है, और Leanstral नाम के छोटे मॉडल को खास Lean के लिए ट्यून किया गया है। ऐसे ही एक प्रोजेक्ट का नाम है evm-asm, जिसमें EVM का इम्प्लीमेंटेशन एक readable reference के साथ verify किया गया है। यह capability वही रीजनिंग skills दिखाता है जो developers ने Buterin के AI चैलेंज में दिए थे — जिसे testers ने कुछ घंटों में ही solve कर लिया था।
यह सब सिर्फ आसानी के लिए नहीं है, बल्कि इससे आगे भी मायने हैं। सिक्योरिटी रिसर्चर्स ने देखा है कि इस साल AI-assisted exploit attempts में तेजी आई है। Formally verified code ऐसे ट्रेंड्स के खिलाफ एक डिफेंस है। अगर specification language यूजर-फ्रेंडली हो तो डेवेलपर्स बिना पूरे proof के क्लेम्स को आसानी से ऑडिट कर पाएंगे।
Ethereum के research सर्कल्स से आगे
Buterin लगातार इन आइडियाज को पब्लिक में टेस्ट करते रहते हैं। हाल ही में उन्होंने जीरो-नॉलेज प्रूफ्स का इस्तेमाल कर एक गुमनाम बिलबोर्ड डेमो किया। इस डेमो में दिखाया गया कि कैसे वेरीफाएबल दावे रिसर्च रिपॉजिटरी से निकलकर वर्किंग प्रोडक्ट्स में ट्रांसफर किए जा सकते हैं। रिसर्चर्स भी अब Lean में कंसेंसस क्लाइंट्स को फॉर्मली वेरीफाई करना शुरू कर चुके हैं ताकि जल्दी बग पकड़े जा सकें।
फिर भी, ये दिशा जाना-पहचाना पैटर्न दिखाती है: तेज कोड को पठनीय दावों से अलग करें, फिर सिद्ध करें कि दोनों मेल खाते हैं।
नई लैंग्वेज का कोई प्रोटोटाइप अभी मौजूद नहीं है, और Buterin ने इसका सटीक सिंटैक्स ओपन रखा है। डेवलपर्स एक साझा स्टैंडर्ड पर सहमत हो सकते हैं, या शायद कई अलग-अलग और इनकंपैटिबल डायलैक्ट्स अपना सकते हैं। यही विकल्प तय करेगा कि AI-वेरिफाइड कोड प्रोडक्शन सिस्टम्स तक कितनी जल्दी पहुंचेगा।
