Leanstral-2603

Leanstral 119B A6B Leanstral is the first open-source code agent designed for Lean 4, a proof assistant capable of expressing complex mathematical objects such as perfectoid spaces and software specifications like properties of Rust fragments. Built as part of the Mistral Small 4 family, it combines multimodal capabilities and an efficient architecture, making it both performant and cost-effective compared to existing closed-source alternatives. For more details about the model and its scope, please read the related blog post. Key Features Leanstral incorporates the following architectural choices: **MoE**: 128 experts, 4 active per token **Model Size**: 119B parameters with 6.5B activated per token **Context Length**: 256k tokens **Multimodal Input**: Accepts text and image input, producing text output Leanstral offers these capabilities: **Proof Agentic**: Designed specifically for proof engineering scenarios **Tool Calling Support**: Optimized for Mistral Vibe **Vision**: Can analyze images and provide insights **Multilingual**: Supports English, French, Spanish, German, Italian, Portuguese, Dutch, Chinese, Japanese, Korean, and Arabic **System Prompt Compliance**: Strong adherence to system prompts **Speed-Optimized**: Best-in-class performance **Apache 2.0 License**: Open-source license for commercial and non-commercial use **Large Context Window**: Supports up to 256k tokens Recommended Settings **Temperature**: 1.0 **Reasoning Effort**: `'none'` → Do not use reasoning `'high'` → Use reasoning (recommended for complex prompts) Use `reasoning_effort="high"` for complex tasks **Context Length**: ≤ 200k tokens recommended Usage Mistral-Vibe Use `Leanstral 119B A6B` with Mistral Vibe. Install the latest version (2.5.0): Leanstral can be added by starting `vibe` and simply running: This will add `leanstral` as an additional model, add a system prompt (see LEAD.md) as well as ensure `leanstral` can be used as a subagent. Then just press "tab+shift" a couple times un