---

license: apache-2.0

base_model: Pythagoras-LM/Pythagoras-Prover-4B

tags:

- llama-cpp

- gguf

- quantized

- math

- reasoning

- theorem-proving

language:

- en

pipeline_tag: text-generation

library_name: llama-cpp

---

Pythagoras-Prover-4B GGUF

GGUF quantizations of Pythagoras-LM/Pythagoras-Prover-4B — a 4B model specialized in mathematical reasoning and formal theorem proving.

Quantized by tinyopsec.

---

Quantization Table

| File | Bits | Size | Use Case |

|------|------|------|----------|

| model_f16.gguf | 16 | ~8.8 GB | Full precision, reference |

| model_q8_0.gguf | 8 | ~4.7 GB | Max quality, fits in 6GB VRAM |

| model_q6_k.gguf | 6 | ~3.6 GB | Near-lossless, recommended |

| model_q5_k_m.gguf | 5 | ~3.1 GB | Balanced quality/size |

| model_q5_k_s.gguf | 5 | ~3.0 GB | Slightly smaller than K_M |

| model_q4_k_m.gguf | 4 | ~2.5 GB | Good quality, popular choice |

| model_q4_k_s.gguf | 4 | ~2.4 GB | Smaller footprint |

| model_q3_k_l.gguf | 3 | ~2.1 GB | Low VRAM, acceptable quality |

| model_q3_k_m.gguf | 3 | ~2.0 GB | Low VRAM |

| model_q3_k_s.gguf | 3 | ~1.9 GB | Minimum recommended |

| model_q2_k.gguf | 2 | ~1.5 GB | Extreme compression, lossy |

---

VRAM Requirements

| Quant | Min VRAM | Recommended |

|-------|----------|-------------|

| F16 | 10 GB | 12 GB+ |

| Q8_0 | 6 GB | 8 GB |

| Q6_K | 5 GB | 6 GB |

| Q5_K_M / Q5_K_S | 4 GB | 5 GB |

| Q4_K_M / Q4_K_S | 4 GB | 4 GB |

| Q3_K_* | 3 GB | 4 GB |

| Q2_K | 3 GB | 3 GB |

---

Usage

llama.cpp

./llama-cli \
  -m model_q4_k_m.gguf \
  -p "Prove that there are infinitely many prime numbers." \
  -n 512 \
  --temp 0.7

llama-cpp-python

from llama_cpp import Llama

llm = Llama(
    model_path="model_q4_k_m.gguf",
    n_ctx=4096,
    n_gpu_layers=-1,
)

response = llm(
    "Prove that sqrt(2) is irrational.",
    max_tokens=512,
    temperature=0.7,
)
print(response["choices"][0]["text"])

LM Studio

1. Download any .gguf file from this repo
2. Open LM Studio → Load Model → select the file
3. Start chatting

Ollama

ollama run hf.co/tinyopsec/Pythagoras-Prover-4B-GGUF:Q4_K_M

---

Recommended Quant

Q4_K_M — best balance of quality and size for most hardware.

Q6_K — if you have 6GB+ VRAM and want near-lossless math reasoning.

---

Original Model

• Pythagoras-LM/Pythagoras-Prover-4B