Instructions to use DiffLean/K2-Prover-SFT-8B-LORA with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use DiffLean/K2-Prover-SFT-8B-LORA with Transformers:

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

pipe = pipeline("text-generation", model="DiffLean/K2-Prover-SFT-8B-LORA")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("DiffLean/K2-Prover-SFT-8B-LORA")
model = AutoModelForCausalLM.from_pretrained("DiffLean/K2-Prover-SFT-8B-LORA")
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 DiffLean/K2-Prover-SFT-8B-LORA with vLLM:

Install from pip and serve model

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

Use Docker

docker model run hf.co/DiffLean/K2-Prover-SFT-8B-LORA

SGLang

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

Docker Model Runner
How to use DiffLean/K2-Prover-SFT-8B-LORA with Docker Model Runner:
```
docker model run hf.co/DiffLean/K2-Prover-SFT-8B-LORA
```

You need to agree to share your contact information to access this model

This repository is publicly accessible, but you have to accept the conditions to access its files and content.

K2-Prover-SFT-8B-LORA

Merged 8B SFT model for Lean 4 theorem proving.

This repository contains the merged full model produced from:

Base model: /scratch/joshua.ong/models/Qwen3-8B
LoRA adapter: /scratch/joshua.ong/k2-diffusion-synthetic/LLaMA-Factory/saves/qwen3-8b/lora_clean/difflean_sft_ds2_test/checkpoint-7036
Merge config: examples/merge_lora/k2_prover_sft_8b_lora.yaml

The LoRA weights have been merged into the base model, so inference should load this as a standard Transformers causal language model without a separate adapter.

Downloads last month: 262

Safetensors

Model size

8B params

Tensor type

BF16