mistralai/Leanstral-1.5-119B-A6B

Leanstral 1.5 119B A6B

!leanstral_benchmark_comparison

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 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:

• 1. Spin up a vllm server as explained in [Usage - vllm](#vllm)
• 2. 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)"
description = "Lean 4 mode using local vLLM"
safety = "neutral"

system_prompt_id = "lean"
active_model = "leanstral"

[[providers]]
name = "vllm"
api_base = "http://:8000/v1"
api_key_env_var = ""
backend = "generic"
reasoning_field_name = "reasoning_content"

[[models]]
name = "mistralai/Leanstral-1.5-119B-A6B"
provider = "vllm"
alias = "leanstral"
thinking = "high"
temperature = 1.0
auto_compact_threshold = 168000

[tools.bash]
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).

vLLM

Let's use this model with the vLLM library to implement production-ready inference pipelines.

1. 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.

2. Launch server

We recommend that you use Leanstral in a server/client setting.

vllm serve mistralai/Leanstral-1.5-119B-A6B \
--max-model-len 200000 \
--tensor-parallel-size 4 \
--attention-backend FLASH_ATTN_MLA \
--tool-call-parser mistral \
--enable-auto-tool-choice \
--reasoning-parser mistral

3. Client

from openai import OpenAI
from huggingface_hub import hf_hub_download

# Modify OpenAI's API key and API base to use vLLM's API server.
openai_api_key = "EMPTY"
openai_api_base = ""

client = OpenAI(
api_key=openai_api_key,
base_url=openai_api_base,
)

TEMP = 1.0
MAX_TOK = 32000
REASONING = "high" # switch to 'none' for faster answers

models = client.models.list()
model = models.data[0].id

prompt = """Define the transition rules as an inductive proposition.

This choice provides better support for proving properties about valid transitions and is generally more natural for modeling state machines in Lean, where you want to express logical rules rather than just computing a yes/no vale for each possible transition."""
messages = [
{
"role": "user",
"content": [
{
"type": "text",
"text": prompt,
},
],
},
]

response = client.chat.completions.create(
model=model,
messages=messages,
temperature=TEMP,
max_tokens=MAX_TOK,
reasoning_effort=REASONING,
)...