Leanstral-1.5-119B-A6B

Leanstral 1.5 119B A6B Leanstral 1.5 is an open-source code agent model 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. [!Note] This is an updated model of our previously released Leanstral model. 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 Recommended Settings **Temperature**: 1.0 **Reasoning Effort**: `'none'` → Do not use reasoning `'high'` → Use reasoning (recommended for complex prompts). **Context Length**: ≤ 200k tokens recommended Usage Installing Mistral Vibe and Leanstral** If you have already installed Leanstral it should automatically use the new model. **** Verify your Mistral account settings at https://chat.mistral.ai/ - Sign up or Sign in - You can stay on the **free** plan (there is no need to sign up to Mistral Pro to use Leanstral). - Opt into “Enable Labs models” in https://admin.mistral.ai/plateforme/privacy - Make an API key in https://admin.mistral.ai/organization/api-keys Follow the instructions to install the mistral vibe CLI at https://docs.mistral.ai/getting-started/quickstarts/vibe-code/install-cli Setup should happen automatically, requesting your API key. But if not, use `vibe --setup` from the terminal. To setup Leanstral in Mistral `vibe` enter: - `/leanstall` (lean + [in]stall) - `exit` (to leave `vibe`) Using Leanstral** Type `vibe --agent lean` in the terminal (**ensure Leanstral displays at the top**). - We recommend running `vibe` inside vs code terminal so you can