mlx-community/Leanstral-2603-8bit

Leanstral-2603 MLX 8-bit

MLX 8-bit quantized version of mistralai/Leanstral-2603.

• Architecture: Mistral-Small-4 (119B params, 6.5B active per token, MoE with 128 experts)
• Specialization: Lean 4 proof engineering
• Quantization: 8-bit (~8.5 bits/weight), 119 GB
• Format: MLX safetensors (for Apple Silicon)
• RAM required: ~128 GB+ unified memory

Usage

from mlx_vlm import load, generate

model, processor = load("mlx-community/Leanstral-2603-8bit")
output = generate(model, processor, "Prove that the sum of two even numbers is even in Lean 4", max_tokens=4096)
print(output)