Modelpublic

tinyopsec/Pythagoras-Prover-4B-GGUF

sourceHugging Faceapache-2.0updated 13d agoView on Hugging Face

1likes2.3kdownloads

Model Card

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
Q5KM / Q5KS	4 GB	5 GB
Q4KM / Q4KS	4 GB	4 GB
Q3K*	3 GB	4 GB
Q2_K	3 GB	3 GB

Usage

llama.cpp

bash

./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

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

bash

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