jackcloudman/leanstral-2603-gguf overview

{
  "metadata": {},
  "card_data": {
    "license": "apache-2.0",
    "base_model": "mistralai/Leanstral-2603",
    "tags": [
      "gguf",
      "llama-cpp",
      "mistral",
      "moe",
      "lean4",
      "math",
      "deepseek2"
    ],
    "quantized_by": "jackcloudman",
    "model_type": "deepseek2",
    "frontmatter": {
      "license": "apache-2.0",
      "base_model": "mistralai/Leanstral-2603",
      "tags": [
        "gguf",
        "llama-cpp",
        "mistral",
        "moe",
        "lean4",
        "math",
        "deepseek2"
      ],
      "quantized_by": "jackcloudman",
      "model_type": "deepseek2"
    },
    "hero_image_url": "",
    "summary": "GGUF quantizations of mistralai/Leanstral-2603 for use with llama.cpp. Leanstral is the first open-source code agent designed for Lean 4, 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.",
    "quick_links": [],
    "benchmark_table_html": "",
    "readme_markdown": "---\nlicense: apache-2.0\nbase_model: mistralai/Leanstral-2603\ntags:\n  - gguf\n  - llama-cpp\n  - mistral\n  - moe\n  - lean4\n  - math\n  - deepseek2\nquantized_by: jackcloudman\nmodel_type: deepseek2\n---\n\n# Leanstral 119B A6B - GGUF\n\nGGUF quantizations of [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603) for use with [llama.cpp](https://github.com/ggml-org/llama.cpp).\n\nLeanstral 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.\n\n## Available Quantizations\n\n| File | Quant | Size | Description |\n|------|-------|------|-------------|\n| `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 |\n| `mistralai_Leanstral-128x3.9B-2603-Q8_0.gguf` | Q8_0 | 118 GB | Near-lossless. Good base for custom requantization |\n\n## Architecture\n\n- **Type**: Mixture of Experts (MoE) + Multi-head Latent Attention (MLA)\n- **GGUF arch**: `deepseek2` (Mistral 4 uses the same architecture as DeepSeek V3)\n- **Total parameters**: 119B (6.5B active per token)\n- **Experts**: 128 routed + 1 shared, 4 active per token\n- **MLA**: q_lora_rank=1024, kv_lora_rank=256, qk_rope_head_dim=64\n- **Context**: Up to 1M tokens (256k recommended)\n- **RoPE**: YaRN scaling (factor=128, original_ctx=8192)\n- **Vocab**: 131,072 tokens (Tekken tokenizer)\n\n## How to Run\n\n### llama-server (recommended)\n\n```bash\n./llama-server \\\n  -m mistralai_Leanstral-128x3.9B-2603-Q4_K_M.gguf \\\n  -fit on -fa on \\\n  --host 0.0.0.0 \\\n  --ctx-size 128000 \\\n  --jinja \\\n  --chat-template-file chat_template.jinja\n```\n\n> **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).\n\n### Reasoning\n\nThe model supports `reasoning_effort` via the chat template:\n- `\"high\"` - Enables thinking (recommended for Lean 4 proofs and complex tasks)\n- `\"none\"` - Direct answers without reasoning\n\nPass `reasoning_effort` in your API request body, or modify the chat template default.\n\n### Performance\n\nOn 2x RTX 4090 (48GB VRAM) + 192GB RAM with Q4_K_M:\n- ~34 tokens/s generation speed\n- Model splits between GPU and system RAM automatically with `-fit on`\n\n## Conversion Details\n\n- **Source**: FP8 (e4m3) consolidated weights from [mistralai/Leanstral-2603](https://huggingface.co/mistralai/Leanstral-2603)\n- **Pipeline**: FP8 consolidated → dequant to BF16 → Q8_0 GGUF → Q4_K_M GGUF (with `--allow-requantize`)\n- **Converter**: `convert_hf_to_gguf.py` with `--mistral-format` flag (llama.cpp)\n- **Tokenizer**: Tekken v15 (requires `mistral-common >= 1.10.0` for conversion)\n\n## License\n\nApache 2.0 - same as the original model.\n\n## Credits\n\n- Original model by [Mistral AI](https://huggingface.co/mistralai)\n- Quantized by [jackcloudman](https://huggingface.co/jackcloudman)\n",
    "related_quantizations": []
  },
  "tags": [
    "gguf",
    "llama-cpp",
    "mistral",
    "moe",
    "lean4",
    "math",
    "deepseek2",
    "base_model:mistralai/Leanstral-2603",
    "base_model:quantized:mistralai/Leanstral-2603",
    "license:apache-2.0",
    "endpoints_compatible",
    "region:us"
  ],
  "likes": 4,
  "downloads": 1630,
  "gated": false,
  "private": false,
  "last_modified": "2026-03-17T03:23:58.000Z",
  "created_at": "2026-03-17T01:59:02.000Z",
  "pipeline_tag": "",
  "library_name": ""
}

{
  "_id": "69b8b5665bff04a265cae305",
  "id": "jackcloudman/Leanstral-2603-GGUF",
  "modelId": "jackcloudman/Leanstral-2603-GGUF",
  "sha": "1630e7bd5104a13e8a76c8fb7ba948a6a0bed1cb",
  "createdAt": "2026-03-17T01:59:02.000Z",
  "lastModified": "2026-03-17T03:23:58.000Z",
  "author": "jackcloudman",
  "downloads": 1630,
  "likes": 4,
  "gated": false,
  "private": false,
  "pipeline_tag": "",
  "library_name": "",
  "siblings_count": 5
}