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
python
1from mlx_vlm import load, generate
23model, processor = load("mlx-community/Leanstral-2603-8bit")4output = generate(model, processor,"Prove that the sum of two even numbers is even in Lean 4", max_tokens=4096)5print(output)
