Leanstral 1.5 119B A6B - GGUF

This repository contains the GGUF quantized version (Q4_K_M) of mistralai/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 the previously released Leanstral model.

Key Features (Base Model)

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

Local GGUF Deployment

Because this is a GGUF file, you can run it locally using llama.cpp or other GGUF-compatible inference frameworks. Due to the 119B parameter scale, ensure your system has enough combined VRAM/RAM to host a ~70-80GB model file.

1. Run via llama.cpp Server (OpenAI Compatible API)

You can spin up a local server that mimics the OpenAI API layout, making it easy to drop into agent workflows or VS Code extensions:

./llama-server \
  -m Leanstral-1.5-119B-A6B-Q4_K_M.gguf \
  -c 32768 \
  --port 8080 \
  --n-gpu-layers 99