Instructions to use Pengzhen23/Gobble-Prover-1.7B with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use Pengzhen23/Gobble-Prover-1.7B with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="Pengzhen23/Gobble-Prover-1.7B")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# pip install -U transformers accelerate
# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("Pengzhen23/Gobble-Prover-1.7B")
model = AutoModelForCausalLM.from_pretrained("Pengzhen23/Gobble-Prover-1.7B", device_map="auto")
messages = [
    {"role": "user", "content": "Who are you?"},
]
inputs = tokenizer.apply_chat_template(
	messages,
	add_generation_prompt=True,
	tokenize=True,
	return_dict=True,
	return_tensors="pt",
).to(model.device)

outputs = model.generate(**inputs, max_new_tokens=256)
print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:]))

Notebooks
Google Colab
Kaggle
Local Apps Settings

vLLM

How to use Pengzhen23/Gobble-Prover-1.7B with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "Pengzhen23/Gobble-Prover-1.7B"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "Pengzhen23/Gobble-Prover-1.7B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/Pengzhen23/Gobble-Prover-1.7B

SGLang

How to use Pengzhen23/Gobble-Prover-1.7B with SGLang:

Install from pip and serve model

# Install SGLang from pip:
pip install sglang
# Start the SGLang server:
python3 -m sglang.launch_server \
    --model-path "Pengzhen23/Gobble-Prover-1.7B" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "Pengzhen23/Gobble-Prover-1.7B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker images

docker run --gpus all \
    --shm-size 32g \
    -p 30000:30000 \
    -v ~/.cache/huggingface:/root/.cache/huggingface \
    --env "HF_TOKEN=<secret>" \
    --ipc=host \
    lmsysorg/sglang:latest \
    python3 -m sglang.launch_server \
        --model-path "Pengzhen23/Gobble-Prover-1.7B" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "Pengzhen23/Gobble-Prover-1.7B",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use Pengzhen23/Gobble-Prover-1.7B with Docker Model Runner:
```
docker model run hf.co/Pengzhen23/Gobble-Prover-1.7B
```

Gobble-Prover-1.7B

Model released with the paper Efficient Proof Generation for Lean Statements with Multiple Candidate Answers (Pengzhen Lin, Ke Zhang, Maziar Raissi, Zhouxing Shi, University of California, Riverside, 2026). Code and reproduction package: https://github.com/Linppz/Gobble-Prover

Gobble-Prover-1.7B is fine-tuned from AI-MO/Kimina-Prover-Distill-1.7B using supervised fine-tuning followed by GRPO. It generates Lean 4 proofs for statements with multiple candidate answers.

This repository contains the model weights, model configuration, and tokenizer. Generated proofs must be checked with Lean.

The base model was developed by Project Numina and Kimi teams and is released under the Apache 2.0 license. See the linked base model card for upstream information.

Citation

@article{lin2026efficient,
  title={Efficient Proof Generation for Lean Statements with Multiple Candidate Answers},
  author={Lin, Pengzhen and Zhang, Ke and Raissi, Maziar and Shi, Zhouxing},
  journal={arXiv preprint},
  year={2026}
}

Downloads last month: 59

Safetensors

Model size

2B params

Tensor type

BF16

Model tree for Pengzhen23/Gobble-Prover-1.7B

Base model

Qwen/Qwen3-1.7B-Base

Finetuned

Qwen/Qwen3-1.7B

Finetuned

project-numina/Kimina-Prover-Distill-1.7B

Finetuned

(3)

this model