Instructions to use FrenzyMath/REAL-Prover with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use FrenzyMath/REAL-Prover with Transformers:

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

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

# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("FrenzyMath/REAL-Prover")
model = AutoModelForCausalLM.from_pretrained("FrenzyMath/REAL-Prover")
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=40)
print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:]))

Notebooks
Google Colab
Kaggle
Local Apps

vLLM

How to use FrenzyMath/REAL-Prover with vLLM:

Install from pip and serve model

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

Use Docker

docker model run hf.co/FrenzyMath/REAL-Prover

SGLang

How to use FrenzyMath/REAL-Prover 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 "FrenzyMath/REAL-Prover" \
    --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": "FrenzyMath/REAL-Prover",
		"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 "FrenzyMath/REAL-Prover" \
        --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": "FrenzyMath/REAL-Prover",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use FrenzyMath/REAL-Prover with Docker Model Runner:
```
docker model run hf.co/FrenzyMath/REAL-Prover
```

mmtke commited on Jul 17, 2025

Commit

1fc4a9b

verified ·

1 Parent(s): 4e5194c

Update README.md

Browse files

Files changed (1) hide show

README.md +1 -1

README.md CHANGED Viewed

@@ -63,7 +63,7 @@ python -m experiment.run /path/to/config.toml
 ## 4. Citation
 ```bibtex
-@article{shen2025realproverretrievalaugmentedlean,
       title={REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning},
       author={Ziju Shen and Naohao Huang and Fanyi Yang and Yutong Wang and Guoxiong Gao and Tianyi Xu and Jiedong Jiang and Wanyi He and Pu Yang and Mengzhou Sun and Haocheng Ju and Peihao Wu and Bryan Dai and Bin Dong},
       year={2025},

 ## 4. Citation
 ```bibtex
+@misc{realprover2025,
       title={REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning},
       author={Ziju Shen and Naohao Huang and Fanyi Yang and Yutong Wang and Guoxiong Gao and Tianyi Xu and Jiedong Jiang and Wanyi He and Pu Yang and Mengzhou Sun and Haocheng Ju and Peihao Wu and Bryan Dai and Bin Dong},
       year={2025},