mistralai/Leanstral-1.5-119B-A6B · Hugging Face
Log In<br>Sign Up
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.
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 :<br>'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/<br>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:<br>/leanstall (lean + [in]stall)
exit (to leave vibe)
Using Leanstral
Type vibe --agent lean in the terminal (ensure Leanstral displays at the top ).<br>We recommend running vibe inside vs code terminal so you can see both vibe and your code.
We recommend running vibe inside your Lean project directory.
To auto-approve model changes (be careful!), use vibe --agent lean --yolo.
Ask Leanstral to do any coding task for you, such as prove a given theorem or fix some code in your project.
Leanstral is capable of doing very long range tasks which requires hours of work. Don’t hesitate to let it work away at a problem.
Using Leanstral with the lean-lsp-mcp
We recommend trying Leanstral with the lean-lsp-mcp, a standard tool for AI agents to interact with Lean. The lean-lsp-mcp README has instructions for setting up the MCP with Mistral Vibe.
Local server
If instead of pinging the Mistral API, you want to use your local vLLM server, you can do the following:
Spin up a vllm server as explained in Usage - vllm
Create a new agent file called lean.toml in ~/.vibe/agents:
mkdir ~/.vibe/agents/ && touch ~/.vibe/agents/lean.toml
And then copy-paste the following config into ~/.vibe/agents/lean.toml
display_name = "Lean (local vLLM)"<br>description = "Lean 4 mode using local vLLM"<br>safety = "neutral"
system_prompt_id = "lean"<br>active_model = "leanstral"
[[providers]]<br>name = "vllm"<br>api_base = "http://:8000/v1"<br>api_key_env_var = ""<br>backend = "generic"<br>reasoning_field_name = "reasoning_content"
[[models]]<br>name = "mistralai/Leanstral-1.5-119B-A6B"<br>provider = "vllm"<br>alias = "leanstral"<br>thinking = "high"<br>temperature = 1.0<br>auto_compact_threshold = 168000
[tools.bash]<br>default_timeout = 1200
Note : Make sure to overwrite with your server's url.
Then restart vibe and "tab-shift" to "lean" mode.
Give it a try on some "lean" code such as, e.g.: PrimeNumberTheoremAnd
Local Deployment
The model can also be deployed with vLLM, we advise everyone to use the Mistral AI API if the model is subpar with local serving:
vllm (recommended): See here.
vLLM
Let's use this model with the vLLM library to implement production-ready inference pipelines.
Installation
Make sure to install vllm >= 0.24.0 :
uv pip install -U vllm --torch-backend=auto
Doing so should automatically install mistral_common >= 1.11.5.
To check:
python -c "import mistral_common; print(mistral_common.__version__)"
You can also make use of a ready-to-go docker image or on the docker hub.
Launch server
We recommend that you use Leanstral in a server/client setting.
vllm serve mistralai/Leanstral-1.5-119B-A6B \<br>--max-model-len 200000 \<br>--tensor-parallel-size 4 \<br>--attention-backend FLASH_ATTN_MLA \<br>--tool-call-parser mistral \<br>--enable-auto-tool-choice \<br>--reasoning-parser mistral
Client
from openai import OpenAI<br>from huggingface_hub import hf_hub_download
# Modify OpenAI's API key and API base to use vLLM's API server.<br>openai_api_key = "EMPTY"<br>openai_api_base = ""
client = OpenAI(<br>api_key=openai_api_key,<br>base_url=openai_api_base,
TEMP = 1.0<br>MAX_TOK = 32000<br>REASONING = "high" # switch to 'none' for faster answers
models = client.models.list()<br>model =...