Leanstral: भरोसेमंद कोड और formal proof इंजीनियरिंग के लिए ओपन सोर्स एजेंट

• Lean 4 के लिए डिज़ाइन किया गया पहला ओपन सोर्स code agent, जिसका लक्ष्य formal proof को ऑटोमेट करके इंसानी verification का बोझ कम करना है
• Apache 2.0 लाइसेंस के तहत model weights जारी किए गए हैं, और Mistral Vibe environment व मुफ्त API endpoint के जरिए तुरंत इस्तेमाल किया जा सकता है
• 6B active parameters वाली sparse architecture का उपयोग करके efficiency और cost reduction हासिल करता है, साथ ही lean-lsp-mcp जैसे MCP integration को सपोर्ट करता है
• FLTEval benchmark में Qwen3.5, GLM5, Kimi-K2.5 जैसे बड़े open source models से बेहतर स्कोर दर्ज किया, और Claude Sonnet के मुकाबले 15 गुना से अधिक कम लागत पर समान प्रदर्शन दिखाया
• formal proof automation और code reliability सुधार को जोड़ने वाले नए दृष्टिकोण के रूप में, यह research mathematics और mission-critical software development दोनों में उपयोग की संभावना दिखाता है

---

Leanstral का अवलोकन

• Leanstral, Lean 4 के लिए पहला ओपन सोर्स code agent है, जो proof assistant environment में काम करता है
  • Lean 4 जटिल गणितीय objects (जैसे perfectoid spaces) और software specifications को व्यक्त कर सकता है
  • जहाँ मौजूदा proof systems सामान्य model wrappers या एकल समस्याओं पर केंद्रित हैं, वहीं Leanstral को वास्तविक formal repositories में कुशलता से काम करने के लिए प्रशिक्षित किया गया है
• 6B active parameters वाली sparse architecture अपनाकर यह parallel inference और Lean की verification क्षमताओं को जोड़ता है
• MCP integration support के माध्यम से यह lean-lsp-mcp जैसे आम तौर पर उपयोग किए जाने वाले protocols के साथ compatible है

रिलीज़ और उपलब्धता

• Apache 2.0 लाइसेंस के तहत model weights जारी किए गए हैं, और Mistral Vibe के agent mode में उपलब्ध है
• मुफ्त API endpoint(labs-leanstral-2603) के जरिए कोई भी इसे एक्सेस कर सकता है, और user feedback इकट्ठा करके अगली model release को बेहतर बनाने की योजना है
• technical report और evaluation tool FLTEval भी साथ जारी किए गए हैं, ताकि केवल गणित-केंद्रित आकलन से आगे बढ़कर वास्तविक proof engineering performance को मापा जा सके

प्रदर्शन मूल्यांकन (Evaluation)

• मूल्यांकन का आधार FLT project के Pull Request unit पर सभी formal proofs और नई गणितीय concepts की definitions को पूरा करने की क्षमता है
• तुलना के मॉडल: Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B

Leanstral vs. open source models

• Leanstral-120B-A6B ने GLM5 (16.6 अंक) और Kimi-K2.5 (20.1 अंक) से बेहतर 26.3 अंक(pass@2) दर्ज किए
• जहाँ Qwen3.5 ने 4 runs (pass@4) में 25.4 अंक हासिल किए, वहीं Leanstral ने आधे runs में इससे अधिक स्कोर प्राप्त किया
• समान cost level पर यह रैखिक रूप से बढ़कर 29.3 अंक(pass@4) तक पहुँचता है

Leanstral vs. Claude product family

• Sonnet की तुलना में 2.6 अंक की बढ़त (26.3 बनाम 23.7) दिखाता है, जबकि execution cost $36 बनाम $549 है, यानी 15 गुना से अधिक सस्ता
• pass@16 के आधार पर 31.9 अंक दर्ज किए, जो Sonnet से 8 अंक अधिक है
• सबसे उच्च प्रदर्शन वाला Claude Opus 4.6 39.6 अंक तक पहुँचा, लेकिन इसकी लागत $1,650 रही, जो Leanstral की तुलना में 92 गुना अधिक है
• सभी benchmarks Mistral Vibe environment में बिना किसी modification के चलाए गए

मॉडल	लागत($)	स्कोर
Haiku	184	23.0
Sonnet	549	23.7
Opus	1,650	39.6
Leanstral	18	21.9
Leanstral pass@2	36	26.3
Leanstral pass@4	72	29.3
Leanstral pass@8	145	31.0
Leanstral pass@16	290	31.9

केस स्टडी

Lean version change के प्रति प्रतिक्रिया

• Lean 4.29.0-rc6 में आए type alias से जुड़े error पर आधारित StackExchange प्रश्न इनपुट किया गया
• Leanstral ने problem environment को reproduce किया और definitional equality समस्या का सटीक निदान किया
• def की जगह abbrev उपयोग करने का सुझाव दिया, जिससे rw tactic फिर से सही तरह काम करने लगी
• समस्या के कारण और समाधान के पीछे की वजह को user को स्पष्ट रूप से समझाया

program reasoning और transformation

• Rocq की program definition को Lean में बदला गया और user-defined notation तक implement की गई
• उदाहरण के तौर पर plus2 command के लिए यह सिद्ध किया गया कि वह variable X में 2 जोड़ने का कार्य करती है
• दी गई Rocq specification के आधार पर Lean में theorem को पूरा किया गया और proof भी किया गया

उपयोग का तरीका

• Mistral Vibe integration: /leanstall command से तुरंत इस्तेमाल संभव
• Labs API: मुफ्त या कम लागत पर उपलब्ध
• model download: Apache 2.0 लाइसेंस के तहत सीधे चलाया जा सकता है

महत्व

• Leanstral, code generation और formal proof automation को जोड़ने वाला पहला ओपन सोर्स प्रयास है
• research mathematics, verifiable software development, high-reliability system design जैसे क्षेत्रों में उपयोग की संभावना दिखाता है
• इसे cost efficiency और openness दोनों को साथ लाने वाली नई code verification infrastructure के रूप में देखा जा रहा है

[GN⁺]

Hacker News की टिप्पणियाँ

• यह दिलचस्प है कि लोग अब इस पैटर्न को पहचानने लगे हैं कि एजेंट के लिए इच्छित व्यवहार को specify करना, और उसी specification के मुताबिक कोड लिखवाना संभव है
  TDD हो, verification tools हों या कोई और तरीका, समय के साथ ऐसे verification suites इस बात को दिखाने वाले executable documentation repository के रूप में जमा होते जाते हैं कि “इसे कैसे काम करना चाहिए”
  यह तरीका साधारण Markdown spec की तुलना में कहीं ज़्यादा ताकतवर है। क्योंकि यह इरादे नहीं, बल्कि विस्तृत व्यवहार को कोड में दर्ज करता है
  जैसे-जैसे software जटिल होता जाता है, “उसके लिए Jim से पूछ लो” जैसी मौखिक परंपरा की सीमाएँ सामने आती हैं

  • मुझे बहुत बड़ा फर्क नहीं लगता। आखिरकार कोड भी बस उस जानकारी की एक अलग अभिव्यक्ति है जो .md फ़ाइल में लिखी जा सकती है
    बारीकी और संदर्भ resolution बदलने की प्रक्रिया में खो जाते हैं
    मैं TDD या verification-first development से सहमत हूँ, लेकिन उसे कोड में लिखना अंतिम लक्ष्य नहीं है
    पहले से ही लाखों लाइनों के tests मौजूद हैं, इसलिए उन्हीं के आधार पर आगे बढ़ना ज़्यादा व्यावहारिक है
  • मुझे लगता है कि AI के आने के बाद ही वह वास्तविकता संभव हुई है जिसका TDD सपना देखता था
  • यह तरीका दिलचस्प है, लेकिन blog post थोड़ी उलझाने वाली थी
    जानना चाहता हूँ कि Lean वास्तव में किस तरह मदद करता है।
    उदाहरण के लिए, क्या Lean में state machine को prove करके फिर उसे Dart में port किया जाता है?
    मुझे Lean की अच्छी समझ नहीं है, इसलिए अंदाज़ा नहीं लग पा रहा कि यह व्यावहारिक तरीका है या नहीं

• जैसा कि हाल में Jack Clark (Anthropic के सह-संस्थापक) और Ezra Klein के podcast में भी कहा गया था, model alignment सापेक्ष है और विविधता महत्वपूर्ण है — इस पर काफी चर्चा हो रही है
  कुछ लोगों का मानना है कि Mistral के models दूसरे frontier models से पीछे हैं, लेकिन ecosystem के लिए अलग-अलग alignment techniques और कंपनियों के साथ प्रयोग करना महत्वपूर्ण है

  • आखिर में समय ही इसका फैसला करेगा

• यह वास्तविक सफलता का मामला Simon Willison के Red Green TDD की याद दिलाता है
  Leanstral ने failure environment को reproduce करने वाला test code बनाया और definitional equality की समस्या पकड़ ली — यह हिस्सा प्रभावशाली था

  • अगर एजेंट खुद tests लिखता है, तो क्या कोड और tests अलग-अलग लिखने की तुलना में correctness की गारंटी ज़्यादा मजबूत होगी?
  • मुझे लगता है TDD आखिरकार prompt engineering जैसा ही है। यानी एजेंट को साफ़ लक्ष्य देना

• यह model खास tasks के लिए train किया गया है, लेकिन Opus से इसकी performance कम है
  Opus 6 गुना महंगा है, लेकिन शायद उतना देना वाजिब लगता है

  • विचार अच्छा है, लेकिन आखिरकार गुणवत्ता, भरोसे से पहले आती है
    कम पूंजी वाला कोई यूरोपीय startup इस niche को target करे, यह समझ आता है, लेकिन इससे बड़ा मुनाफा निकलना मुश्किल लगता है
  • benchmark की विश्वसनीयता थोड़ी अस्पष्ट है, लेकिन pass@2 या pass@3 के नतीजे देखें तो प्रभाव बदलता है
    Codex जैसे models से तुलना करना शायद ज़्यादा दिलचस्प होगा
  • model open source है, इसलिए इसे local पर चलाया जा सकता है। क्या यह अपने आप में काफी महत्वपूर्ण बात नहीं है?

• मुझे “reliable code” का concept पसंद आया
  लेकिन comparison baseline उलझाने वाला है। वे इस बात पर ज़ोर देते हैं कि यह Haiku से सस्ता है, जबकि Haiku खुद इस काम में कमजोर है और Leanstral उससे भी कमजोर है
  अगर लक्ष्य accuracy है, तो “सस्ता लेकिन कमजोर” क्यों महत्वपूर्ण है, यह समझ नहीं आता
  फिर भी Opus भी परफेक्ट नहीं है, इसलिए scale बढ़ाने पर शायद बेहतर नतीजे मिल सकते हैं

  • graph देखें तो pass count बढ़ने के साथ performance बेहतर होती है
    2 runs पर यह Haiku और Sonnet से बेहतर है, और 16 runs पर Opus के करीब पहुँचता है, जबकि cost efficiency भी बनी रहती है
  • असल में बात सरल है — prompt में बस “केवल भरोसेमंद output” माँग दीजिए

• Lean को न जानने वाले के नज़रिए से, समझ नहीं आता कि इसका सीधा मूल्य क्या है
  क्या यह Go जैसी भाषा के कोड के साथ अपने-आप proofs जोड़ता है, या फिर बस open models की विविधता का समर्थन करना चाहिए?

  • शायद संरचना यह होगी कि एजेंट Lean4 specification बनाता है, और उसी specification के आधार पर software का मूल्यांकन किया जाता है
    लेकिन आखिरकार Lean4 specification खुद भी एक software artifact बन जाती है
    तब सवाल फिर वहीं लौटता है कि उस specification की शुद्धता कैसे verify होगी — यानी अंततः human review की ज़रूरत रहती है

• मैं कुछ हफ्तों से इस दिशा की उम्मीद कर रहा था, इसलिए सही साबित होना अच्छा लग रहा है
  LLM युग में शायद कोड की human-friendliness से ज़्यादा provability और token efficiency महत्वपूर्ण हो जाएगी
  Lean और Rust को मिलाकर शायद ऐसी दुनिया आ सकती है जहाँ “सिर्फ proven code ही compile हो”
  इससे जुड़ी चर्चा मैंने पिछली टिप्पणी में लिखी थी

  • हालांकि कोई भी proof system “सही proof” की गारंटी नहीं देता
    वह सिर्फ logically valid होने की गारंटी देता है
    proof किस चीज़ को साबित कर रहा है, इसे पूरी तरह समझना उतना ही कठिन है जितना किसी program को समझना, लेकिन इस प्रक्रिया में सोच और गहरी होती है

• अच्छा लगा कि “open source” सिर्फ कहने के लिए नहीं, बल्कि वास्तव में Apache-2.0 licensed weights के रूप में जारी किया गया है

  • लेकिन community standards के हिसाब से, अगर model को reproduce नहीं किया जा सकता, तो वह “open weights” है, “open source” नहीं

• Mistral की आधिकारिक खबर के अनुसार
  Claude Opus की लागत 1,650 डॉलर पर स्कोर 39.6 है,
  Leanstral pass@8 की लागत 145 डॉलर पर 31.0 है, और pass@16 की 290 डॉलर पर 31.9,
  इसलिए cost के मुकाबले performance efficiency काफी अच्छी लगती है