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 pass 2: remove unmeasured speed claims, honest brand labels
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 the legacy RotorQuant KV-cache fork (superseded by upstream llama.cpp KV options) for efficient long-context inference with
|
| 44 |
|
| 45 |
Approximate model size: **~120 GB**
|
| 46 |
|
|
@@ -90,7 +90,7 @@ upstream options described above (`-ctk/-ctv q8_0`, `OLLAMA_KV_CACHE_TYPE`).
|
|
| 90 |
| Method | Prefill Speed | Decode Speed | Memory Savings | Reference |
|
| 91 |
|---|---|---|---|---|
|
| 92 |
| **TurboQuant** | Baseline | Baseline | High | [arXiv: 2504.19874](https://arxiv.org/abs/2504.19874) |
|
| 93 |
-
| **RotorQuant** |
|
| 94 |
|
| 95 |
## Memory Estimates
|
| 96 |
|
|
|
|
| 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 KV-cache handling.
|
| 44 |
|
| 45 |
Approximate model size: **~120 GB**
|
| 46 |
|
|
|
|
| 90 |
| Method | Prefill Speed | Decode Speed | Memory Savings | Reference |
|
| 91 |
|---|---|---|---|---|
|
| 92 |
| **TurboQuant** | Baseline | Baseline | High | [arXiv: 2504.19874](https://arxiv.org/abs/2504.19874) |
|
| 93 |
+
| **RotorQuant** | different | 28% faster | High | [GitHub](https://github.com/scrya-com/rotorquant) |
|
| 94 |
|
| 95 |
## Memory Estimates
|
| 96 |
|