| --- |
| base_model: mistralai/Leanstral-2603 |
| library_name: mlx |
| tags: |
| - rotorquant |
| - kv-cache-quantization |
| - mlx |
| - 4-bit |
| - weight-quantization |
| - leanstral |
| - lean4 |
| - formal-proofs |
| - theorem-proving |
| - quantized |
| - apple-silicon |
| - mistral |
| - moe |
| license: apache-2.0 |
| --- |
| |
| # Leanstral-RotorQuant-MLX-4bit |
|
|
| **4-bit MLX weight-quantized [Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) with [RotorQuant](https://github.com/scrya-com/rotorquant) KV-cache quantization for high-throughput Lean 4 formal proof generation on Apple Silicon.** |
|
|
| Leanstral is the first open-source AI agent purpose-built for Lean 4 formal proofs -- generating both executable code and machine-checkable mathematical proofs. This variant combines **dual compression**: 4-bit MLX weight quantization plus RotorQuant KV-cache quantization, delivering **5.3x faster prefill** and **28% faster decode** compared to TurboQuant equivalents. |
|
|
| ## Overview |
|
|
| This repository provides a **dual-compressed** configuration with RotorQuant's superior throughput: MLX 4-bit weight quantization reduces the static memory footprint, while RotorQuant's rotation-aware KV-cache compression delivers faster prefill and decode. This is the recommended MLX variant for interactive theorem proving on Apple Silicon. |
|
|
| | Spec | Value | |
| |------|-------| |
| | Base model | [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) | |
| | Architecture | Mistral MoE (~119B parameters, 7 consolidated shards) | |
| | Weight quantization | 4-bit (MLX) | |
| | KV-cache quantization | RotorQuant | |
| | Weight memory | ~60 GB | |
| | Prefill speedup | 5.3x vs TurboQuant | |
| | Decode speedup | 28% vs TurboQuant | |
| | Runtime | MLX (Apple Silicon) | |
| | License | Apache 2.0 | |
| | Use case | Lean 4 formal verification, theorem proving, mathematical proofs | |
|
|
| ## Quickstart |
|
|
| ```python |
| from mlx_lm import load, generate |
| |
| model, tokenizer = load("majentik/Leanstral-RotorQuant-MLX-4bit") |
| |
| prompt = "Prove that for all natural numbers n, n + 0 = n in Lean 4:" |
| response = generate( |
| model, |
| tokenizer, |
| prompt=prompt, |
| max_tokens=512, |
| ) |
| print(response) |
| ``` |
|
|
| ## What is RotorQuant? |
|
|
| [RotorQuant](https://github.com/scrya-com/rotorquant) is an advanced KV-cache quantization method that leverages rotation-aware quantization to achieve superior throughput compared to standard KV-cache compression. By exploiting the rotary positional embedding structure, RotorQuant achieves: |
|
|
| - **5.3x faster prefill** -- critical for long Lean 4 proof contexts |
| - **28% faster decode** -- faster token-by-token proof generation |
| - Equivalent memory savings to TurboQuant with better computational efficiency |
|
|
| Combined with MLX 4-bit weight quantization, this is the highest-quality Apple Silicon variant with optimized throughput. |
|
|
| ## Memory Estimates |
|
|
| | Component | Estimate | |
| |-----------|----------| |
| | Model weights (4-bit) | ~60 GB | |
| | KV-cache | Reduced via RotorQuant | |
| | Recommended hardware | Mac Studio M2/M3/M4 Ultra (192 GB+) or Mac Pro | |
|
|
| ## Lean 4 Use Case |
|
|
| Leanstral excels at: |
| - **Formal verification** -- generating machine-checkable proofs of mathematical theorems |
| - **Theorem proving** -- interactive and automated proof search in Lean 4 |
| - **Code generation** -- writing verified Lean 4 programs with correctness guarantees |
| - **Proof repair** -- fixing incomplete or broken proof scripts |
|
|
| ## See Also |
|
|
| - [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) -- Base model |
| - [majentik/Leanstral-RotorQuant](https://huggingface.co/majentik/Leanstral-RotorQuant) -- Full-precision weights + RotorQuant KV cache |
| - [majentik/Leanstral-RotorQuant-MLX-2bit](https://huggingface.co/majentik/Leanstral-RotorQuant-MLX-2bit) -- MLX 2-bit + RotorQuant |
| - [majentik/Leanstral-RotorQuant-MLX-1bit](https://huggingface.co/majentik/Leanstral-RotorQuant-MLX-1bit) -- MLX 1-bit + RotorQuant |
| - [majentik/Leanstral-TurboQuant-MLX-4bit](https://huggingface.co/majentik/Leanstral-TurboQuant-MLX-4bit) -- MLX 4-bit + TurboQuant |
| - [RotorQuant repository](https://github.com/scrya-com/rotorquant) |
|
|
