Leanstral-1.5-119B-A6B-MLX-4bit

4-bit MLX affine quantization of mistralai/Leanstral-1.5-119B-A6B, a 119B-parameter (A6B active) mixture-of-experts vision-language model tuned for Lean 4. Produced with mlx_vlm.convert on Apple silicon.

Quantization recipe

• Method: affine, group size 64, 4-bit.
• Effective: ~4.59 bits/weight.
• Router precision: the 36 MoE router gates (*.mlp.gate) are kept at 8-bit regardless of the target width, matching the reference recipe. This protects expert selection, which is disproportionately sensitive to quant noise.
• Full precision: vision tower, multimodal projector, and lm_head are left unquantized.

Usage

pip install mlx-vlm
python -m mlx_vlm.generate \
  --model mvid/Leanstral-1.5-119B-A6B-MLX-4bit \
  --max-tokens 512 \
  --prompt "State and prove in Lean 4 that addition on the naturals is commutative."

MLA attention is expanded to full MHA in mlx-vlm's cache, so long-context runs are memory-heavy on this engine; for large contexts prefer a GGUF build under llama.cpp / LM Studio, which keeps the KV cache compressed.

Sibling quants

MLX-8bit · MLX-6bit · MLX-5bit · MLX-4bit · MLX-3bit