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
- Download any
.gguffile from this repo - Open LM Studio → Load Model → select the file
- 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.