lean-standard-prover-qwen3-8b-reasoning-grpo/README.md

---
library_name: transformers
pipeline_tag: text-generation
base_model: Qwen/Qwen3-8B-Base
base_model_relation: finetune
language:
- en
tags:
- lean
- lean4
- theorem-proving
- qwen3
- standard-prover
- reasoning
- grpo
datasets:
- EPFL-LARA/lean-world-model-cpt
- EPFL-LARA/lean-world-model-sft
- EPFL-LARA/lean-world-model-reasoning-sft
- Goedel-LM/RL_dataset_V2
---

# Lean Standard Prover — Qwen3-8B

**Paper model:** S8 + reasoning · **Stage:** After informal reasoning

Generates complete Lean proofs from theorem statements using the standard prover response format. This variant writes an informal reasoning plan before each proof attempt.

## Hugging Face Transformers

Load the published weights from the Hub and generate on your GPU:

```bash
pip install 'transformers==4.57.3' accelerate torch
hf download EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo example_transformers.py inference.py prompt_utils.py Example.lean --local-dir lean-standard-prover-qwen3-8b-reasoning-grpo
cd lean-standard-prover-qwen3-8b-reasoning-grpo
python example_transformers.py
```

The included `Example.lean` is the input; replace it with your own imports,
context, and theorem ending in `by sorry`:

```lean4
import Mathlib

theorem demo (n : ℕ) : n + 0 = n := by sorry
```

The complete Transformers example is:

```python
from pathlib import Path

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer, set_seed

from inference import build_prompt

MODEL_ID = 'EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo'

source = Path("Example.lean").read_text(encoding="utf-8")
prompt = build_prompt(source)
tokenizer = AutoTokenizer.from_pretrained(MODEL_ID)
model = AutoModelForCausalLM.from_pretrained(
    MODEL_ID, dtype=torch.bfloat16, device_map="auto", attn_implementation="sdpa",
).eval()
inputs = tokenizer(prompt, return_tensors="pt", add_special_tokens=False).to(model.device)
prompt_length = inputs["input_ids"].shape[1]
budget = min(2048, 32768 - prompt_length)
if budget <= 0:
    raise ValueError("The prompt must leave room for a proof in the 32,768-token context.")

set_seed(0)
with torch.inference_mode():
    output = model.generate(
        **inputs, max_new_tokens=budget, do_sample=True,
        temperature=0.3, top_p=0.95, top_k=0, min_p=0.0,
        repetition_penalty=1.0, num_beams=1,
        pad_token_id=tokenizer.pad_token_id,
    )
response = tokenizer.decode(output[0, prompt_length:], skip_special_tokens=True)
print(response, end="")
```

`build_prompt` supplies this checkpoint's exact raw completion prompt.
Tokenization uses `add_special_tokens=False`; the context budget is 32,768
tokens. This compact example allows up to 2,048 generated tokens and prints
only the generated response.

## Example output

Recorded with the script above on an H100 in BF16, using seed 0,
temperature 0.3, and top-p 0.95. This is the extracted final proof, checked
with Lean 4.15 and Mathlib:

```lean4
import Mathlib


theorem demo (n : ℕ) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp_all
```

<details>
<summary>Full generated response</summary>

````text
[Problem Restatement]

For every natural number \(n\), adding zero to \(n\) leaves \(n\) unchanged. In symbols, the claim is

\[
n + 0 = n.
\]

This is one of the basic properties of addition on the natural numbers.

[Useful Observations]

1. **Zero is the additive identity.** In any algebraic structure with addition, the element \(0\) is defined by the property that adding it to any element does not change that element. For natural numbers, this is exactly the statement \(n + 0 = n\).

2. **Natural numbers are built recursively.** The natural numbers are generated from \(0\) by repeatedly applying the successor operation. This means any proof about all natural numbers can be reduced to checking the base case \(n = 0\) and then verifying that the property is preserved when moving from \(n\) to \(n+1\).

3. **The successor case is immediate.** If we already know \(n + 0 = n\), then adding one more zero gives \((n+1) + 0 = n+1\). This is just the same identity applied to the successor of \(n\).

[Reasoning Path]

To prove \(n + 0 = n\) for all natural numbers, we use the recursive definition of the natural numbers.

- **Base case:** When \(n = 0\), the statement becomes \(0 + 0 = 0\), which is true by the definition of addition.

- **Inductive step:** Assume the statement holds for some natural number \(n\), i.e., \(n + 0 = n\). We must show it holds for \(n+1\), i.e., \((n+1) + 0 = n+1\). But \((n+1) + 0\) is just \(n+1\) by the definition of addition, so the statement is true for \(n+1\) as well.

Since both the base case and the inductive step are immediate, the identity holds for every natural number \(n\).

[Key Derivation]

The entire derivation is captured by the two equations:

\[
0 + 0 = 0,
\]

and

\[
(n+1) + 0 = n+1.
\]

These are exactly the base and successor cases of the recursive definition of addition on natural numbers.

[Proof Type]

This is a direct proof by induction on the natural number \(n\).

[Formal Anchors]

The Lean proof uses induction on \(n\):

```lean4
induction n with
| zero => rfl
| succ n ih => ...
```

The base case is closed by reflexivity (`rfl`), and the successor case follows from the induction hypothesis (`ih`) together with the simplifier (`simp`), which uses the recursive definition of addition.

[Final Solution]

We prove that \(n + 0 = n\) for every natural number \(n\) by induction.

- For \(n = 0\), we have \(0 + 0 = 0\), which is true.
- Assume \(n + 0 = n\). Then \((n+1) + 0 = n+1\), which is also true.

By induction, \(n + 0 = n\) for all natural numbers \(n\).

The complete typechecked Lean 4 proof is:

```lean4
import Mathlib


theorem demo (n : ℕ) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp_all
```
````

</details>

[Full response](https://huggingface.co/EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo/blob/main/example_response.txt) ·
[Input/output JSON](https://huggingface.co/EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo/blob/main/example_output.json) ·
[Lean proof](https://huggingface.co/EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo/blob/main/example_proof.lean)

## vLLM

For multiple samples and longer output budgets:

```bash
pip install 'vllm==0.12.0'
hf download EPFL-LARA/lean-standard-prover-qwen3-8b-reasoning-grpo inference.py prompt_utils.py Example.lean --local-dir lean-standard-prover-qwen3-8b-reasoning-grpo
python lean-standard-prover-qwen3-8b-reasoning-grpo/inference.py lean-standard-prover-qwen3-8b-reasoning-grpo/Example.lean --samples 1
```

The vLLM runner uses the same raw prompt. Its default temperature is 0.3
for one sample and 0.7 for 32 samples; top-p is 0.95. Output tokens fit
within the context remaining after the prompt. Use `--print-prompt` to
inspect the exact input without loading weights.

## Prompt template

The reasoning template follows `evaluate_prover_model_run.py`.
Replace the placeholder with the imports, context, and theorem ending in
`by sorry`, and keep the final newline:

````text
Solve the following problem with Lean 4 code and explanatory comments:

```lean4
{formal_statement_with_imports}
```

Replace every sorry statement with an appropriate proof. Before writing any Lean code, give an informal solution with the sections [Problem Restatement], [Useful Observations], [Reasoning Path], [Key Derivation], [Proof Type], [Formal Anchors] and [Final Solution]. Then provide the complete solution in the lean4 code block. If a previous attempt failed, first give [Error Analysis], [Revised Reasoning] and [Updated Proof Plan], then provide the corrected solution.
````

## Expected response

The requested informal-solution sections precede the Lean proof. A repair begins with `[Error Analysis]`, `[Revised Reasoning]`, and `[Updated Proof Plan]`.

The response contains a complete proof in a `lean4` code fence, together with explanatory text or comments.

Use the **last complete Lean code block** as the final proof candidate for Lean verification. The vLLM runner returns the full `response`, extracted `lean_code`, and `finish_reason` as JSONL.

[Formal Theorem Proving with Lean World Models](https://huggingface.co/collections/EPFL-LARA/formal-theorem-proving-with-lean-world-models-6ad2b4aa4400b3e2933f380d)