Instructions to use lm-provers/QED-Nano with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use lm-provers/QED-Nano with Transformers:

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

pipe = pipeline("text-generation", model="lm-provers/QED-Nano")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("lm-provers/QED-Nano")
model = AutoModelForCausalLM.from_pretrained("lm-provers/QED-Nano")
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]:]))

Inference
Notebooks
Google Colab
Kaggle
Local Apps

vLLM

How to use lm-provers/QED-Nano with vLLM:

Install from pip and serve model

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

Use Docker

docker model run hf.co/lm-provers/QED-Nano

SGLang

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

Docker Model Runner
How to use lm-provers/QED-Nano with Docker Model Runner:
```
docker model run hf.co/lm-provers/QED-Nano
```

Formal proofs

by catalin-hanga - opened Feb 17

Discussion

catalin-hanga

Feb 17

Hi,
Is the model able to generate formal proofs in the Lean 4 language, or use tools (like a Python REPL tool) ?
Thanks

JasperDekoninck

LM Provers org Feb 17

Hi!
The model was trained to produce proofs in natural language, not Lean (or any other formal language).
While the base model (Qwen3-4B-Think) supports tool-use, we did not do any finetuning with tool calls. The model might have therefore lost its ability to make effective use of tools.

przemekch

Feb 27

Hi, it might be interesting though to connect it to our UlamAI Prover via Ollama which uses LLM - LeanDojo loop to formalize mathematics from .tex - https://github.com/ulamai/ulamai -- I'm happy to collab more on the integration because it genuinely seems like something that can run locally.

JasperDekoninck

LM Provers org Feb 27

QED-Nano itself is not really perfectly suited for this; as mentioned above, it lacks Lean and tool-calling capabilities. It is therefore unlikely it knows (1) enough syntax to produce correct Lean, (2) is able to bridge the significant gap between natural language and formal proofs when attempting autoformalization, and (3) interact with the provided tools in a meaningful way.

We are currently not (yet) looking at creating a model that can do those things, instead focusing on improving our model for natural language theorem proving.

Upload images, audio, and videos by dragging in the text input, pasting, or clicking here.

Tap or paste here to upload images

· Sign up or log in to comment