Upload README.md with huggingface_hub

README.md

@@ -0,0 +1,84 @@
+---
+license: apache-2.0
+base_model: mistralai/Leanstral-2603
+tags:
+  - gguf
+  - llama-cpp
+  - mistral
+  - moe
+  - lean4
+  - math
+  - deepseek2
+quantized_by: jackcloudman
+model_type: deepseek2
+---
+
+# Leanstral 119B A6B - GGUF
+
+GGUF quantizations of [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) for use with [llama.cpp](https://github.com/ggml-org/llama.cpp).
+
+Leanstral is the first open-source code agent designed for [Lean 4](https://github.com/leanprover/lean4), a proof assistant for formal mathematics and software verification. Built as part of the Mistral Small 4 family, it combines multimodal capabilities with an efficient MoE + MLA architecture.
+
+## Available Quantizations
+
+| File | Quant | Size | Description |
+|------|-------|------|-------------|
+| `mistralai_Leanstral-128x3.9B-2603-Q4_K_M.gguf` | Q4_K_M | 68 GB | Best balance of quality and size. Runs on 2x RTX 4090 + RAM offload |
+| `mistralai_Leanstral-128x3.9B-2603-Q8_0.gguf` | Q8_0 | 118 GB | Near-lossless. Good base for custom requantization |
+
+## Architecture
+
+- **Type**: Mixture of Experts (MoE) + Multi-head Latent Attention (MLA)
+- **GGUF arch**: `deepseek2` (Mistral 4 uses the same architecture as DeepSeek V3)
+- **Total parameters**: 119B (6.5B active per token)
+- **Experts**: 128 routed + 1 shared, 4 active per token
+- **MLA**: q_lora_rank=1024, kv_lora_rank=256, qk_rope_head_dim=64
+- **Context**: Up to 1M tokens (256k recommended)
+- **RoPE**: YaRN scaling (factor=128, original_ctx=8192)
+- **Vocab**: 131,072 tokens (Tekken tokenizer)
+
+## How to Run
+
+### llama-server (recommended)
+
+```bash
+./llama-server \
+  -m mistralai_Leanstral-128x3.9B-2603-Q4_K_M.gguf \
+  -fit on -fa on \
+  --host 0.0.0.0 \
+  --ctx-size 128000 \
+  --jinja \
+  --chat-template-file chat_template.jinja
+```
+
+> **Note**: You need a chat template that supports `[THINK]` blocks for reasoning. Download the template from the [original model repo](https://huggingface.co/mistralai/Leanstral-2603).
+
+### Reasoning
+
+The model supports `reasoning_effort` via the chat template:
+- `"high"` - Enables thinking (recommended for Lean 4 proofs and complex tasks)
+- `"none"` - Direct answers without reasoning
+
+Pass `reasoning_effort` in your API request body, or modify the chat template default.
+
+### Performance
+
+On 2x RTX 4090 (48GB VRAM) + 192GB RAM with Q4_K_M:
+- ~34 tokens/s generation speed
+- Model splits between GPU and system RAM automatically with `-fit on`
+
+## Conversion Details
+
+- **Source**: FP8 (e4m3) consolidated weights from [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603)
+- **Pipeline**: FP8 consolidated → dequant to BF16 → Q8_0 GGUF → Q4_K_M GGUF (with `--allow-requantize`)
+- **Converter**: `convert_hf_to_gguf.py` with `--mistral-format` flag (llama.cpp)
+- **Tokenizer**: Tekken v15 (requires `mistral-common >= 1.10.0` for conversion)
+
+## License
+
+Apache 2.0 - same as the original model.
+
+## Credits
+
+- Original model by [Mistral AI](https://huggingface.co/mistralai)
+- Quantized by [jackcloudman](https://huggingface.co/jackcloudman)