Text Generation
MLX
Safetensors
mistral3
rotorquant
kv-cache-quantization
8bit
weight-quantization
leanstral
lean4
formal-proofs
theorem-proving
quantized
apple-silicon
mistral
Mixture of Experts
8-bit precision
Instructions to use majentik/Leanstral-RotorQuant-MLX-8bit with libraries, inference providers, notebooks, and local apps. Follow these links to get started.
- Libraries
- MLX
How to use majentik/Leanstral-RotorQuant-MLX-8bit with MLX:
# Make sure mlx-lm is installed # pip install --upgrade mlx-lm # if on a CUDA device, also pip install mlx[cuda] # Generate text with mlx-lm from mlx_lm import load, generate model, tokenizer = load("majentik/Leanstral-RotorQuant-MLX-8bit") prompt = "Once upon a time in" text = generate(model, tokenizer, prompt=prompt, verbose=True) - Notebooks
- Google Colab
- Kaggle
- Local Apps Settings
- LM Studio
- MLX LM
How to use majentik/Leanstral-RotorQuant-MLX-8bit with MLX LM:
Generate or start a chat session
# Install MLX LM uv tool install mlx-lm # Generate some text mlx_lm.generate --model "majentik/Leanstral-RotorQuant-MLX-8bit" --prompt "Once upon a time"
- Atomic Chat
Card accuracy sweep: honest brand labeling, remove dead links, upstream KV tip
Browse files
README.md
CHANGED
|
@@ -40,7 +40,7 @@ pipeline_tag: text-generation
|
|
| 40 |
|
| 41 |
**8-bit MLX weight-quantized [Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) with [RotorQuant](https://github.com/scrya-com/rotorquant) KV-cache quantization for Lean 4 formal proof generation on Apple Silicon.**
|
| 42 |
|
| 43 |
-
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**: 8-bit MLX weight quantization for reduced model size plus RotorQuant KV-cache
|
| 44 |
|
| 45 |
Approximate model size: **~120 GB**
|
| 46 |
|
|
@@ -76,15 +76,14 @@ response = generate(
|
|
| 76 |
print(response)
|
| 77 |
```
|
| 78 |
|
| 79 |
-
##
|
| 80 |
|
| 81 |
-
|
| 82 |
-
|
| 83 |
-
-
|
| 84 |
-
-
|
| 85 |
-
|
| 86 |
-
|
| 87 |
-
Combined with MLX 8-bit weight quantization, this dual compression approach makes it feasible to run Leanstral's ~119B parameter model on Apple Silicon hardware with excellent throughput.
|
| 88 |
|
| 89 |
## KV-Cache Quantization Comparison
|
| 90 |
|
|
@@ -112,7 +111,6 @@ Leanstral excels at:
|
|
| 112 |
## See Also
|
| 113 |
|
| 114 |
- [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) -- Base model
|
| 115 |
-
- [majentik/Leanstral-RotorQuant-MLX-4bit](https://huggingface.co/majentik/Leanstral-RotorQuant-MLX-4bit) -- MLX 4-bit + RotorQuant
|
| 116 |
- [majentik/Leanstral-RotorQuant-MLX-2bit](https://huggingface.co/majentik/Leanstral-RotorQuant-MLX-2bit) -- MLX 2-bit + RotorQuant
|
| 117 |
- [majentik/Leanstral-TurboQuant-MLX-8bit](https://huggingface.co/majentik/Leanstral-TurboQuant-MLX-8bit) -- MLX 8-bit + TurboQuant
|
| 118 |
- [RotorQuant GitHub](https://github.com/scrya-com/rotorquant)
|
|
@@ -137,11 +135,7 @@ Leanstral excels at:
|
|
| 137 |
|
| 138 |
| Variant | Runtime | Approx size | Use case |
|
| 139 |
|---|---|---|---|
|
| 140 |
-
| [RotorQuant](https://huggingface.co/majentik/leanstral-rotorquant) | runtime modifier | n/a | KV-cache root (weight-agnostic) |
|
| 141 |
| [RotorQuant-MLX-2bit](https://huggingface.co/majentik/leanstral-rotorquant-mlx-2bit) | mlx-lm | card-only | Apple Silicon, smallest |
|
| 142 |
-
| [RotorQuant-MLX-4bit](https://huggingface.co/majentik/leanstral-rotorquant-mlx-4bit) | mlx-lm | card-only | Apple Silicon balanced |
|
| 143 |
| **RotorQuant-MLX-8bit** | mlx-lm | card-only | Apple Silicon reference |
|
| 144 |
-
| [TurboQuant](https://huggingface.co/majentik/leanstral-turboquant) | runtime modifier | n/a | KV-cache root (weight-agnostic) |
|
| 145 |
| [TurboQuant-MLX-2bit](https://huggingface.co/majentik/leanstral-turboquant-mlx-2bit) | mlx-lm | card-only | Apple Silicon, smallest |
|
| 146 |
-
| [TurboQuant-MLX-4bit](https://huggingface.co/majentik/leanstral-turboquant-mlx-4bit) | mlx-lm | card-only | Apple Silicon balanced |
|
| 147 |
| [TurboQuant-MLX-8bit](https://huggingface.co/majentik/leanstral-turboquant-mlx-8bit) | mlx-lm | card-only | Apple Silicon reference |
|
|
|
|
| 40 |
|
| 41 |
**8-bit MLX weight-quantized [Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) with [RotorQuant](https://github.com/scrya-com/rotorquant) KV-cache quantization for Lean 4 formal proof generation on Apple Silicon.**
|
| 42 |
|
| 43 |
+
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**: 8-bit MLX weight quantization for reduced model size plus the legacy RotorQuant KV-cache fork (superseded by upstream llama.cpp KV options) for efficient long-context inference with faster prefill and decode.
|
| 44 |
|
| 45 |
Approximate model size: **~120 GB**
|
| 46 |
|
|
|
|
| 76 |
print(response)
|
| 77 |
```
|
| 78 |
|
| 79 |
+
## About the RotorQuant / TurboQuant labels
|
| 80 |
|
| 81 |
+
RotorQuant and TurboQuant are this project's **release labels**, not distinct
|
| 82 |
+
quantization algorithms — for any given tier, both brand repos carry
|
| 83 |
+
byte-identical weights produced with the standard MLX / llama.cpp quantizers.
|
| 84 |
+
No brand-specific speedup is claimed or measured. The KV-cache fork these
|
| 85 |
+
labels originally referred to is legacy; for KV-cache memory savings use the
|
| 86 |
+
upstream options described above (`-ctk/-ctv q8_0`, `OLLAMA_KV_CACHE_TYPE`).
|
|
|
|
| 87 |
|
| 88 |
## KV-Cache Quantization Comparison
|
| 89 |
|
|
|
|
| 111 |
## See Also
|
| 112 |
|
| 113 |
- [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) -- Base model
|
|
|
|
| 114 |
- [majentik/Leanstral-RotorQuant-MLX-2bit](https://huggingface.co/majentik/Leanstral-RotorQuant-MLX-2bit) -- MLX 2-bit + RotorQuant
|
| 115 |
- [majentik/Leanstral-TurboQuant-MLX-8bit](https://huggingface.co/majentik/Leanstral-TurboQuant-MLX-8bit) -- MLX 8-bit + TurboQuant
|
| 116 |
- [RotorQuant GitHub](https://github.com/scrya-com/rotorquant)
|
|
|
|
| 135 |
|
| 136 |
| Variant | Runtime | Approx size | Use case |
|
| 137 |
|---|---|---|---|
|
|
|
|
| 138 |
| [RotorQuant-MLX-2bit](https://huggingface.co/majentik/leanstral-rotorquant-mlx-2bit) | mlx-lm | card-only | Apple Silicon, smallest |
|
|
|
|
| 139 |
| **RotorQuant-MLX-8bit** | mlx-lm | card-only | Apple Silicon reference |
|
|
|
|
| 140 |
| [TurboQuant-MLX-2bit](https://huggingface.co/majentik/leanstral-turboquant-mlx-2bit) | mlx-lm | card-only | Apple Silicon, smallest |
|
|
|
|
| 141 |
| [TurboQuant-MLX-8bit](https://huggingface.co/majentik/leanstral-turboquant-mlx-8bit) | mlx-lm | card-only | Apple Silicon reference |
|