DeepSeek-Prover-V1.5 with RMaxTS
A Lean 4 prover is trained with proof-checker feedback, then searched with a tree search that rewards reaching new proof states.
The loop
- Proposes
Lean 4 proofs and proof steps from a language model
- Judged by
The Lean 4 proof assistant, which accepts or rejects each proof and each step
- Steers
Lean outcomes are the RL reward; at inference, RMaxTS tree search rewards new states to pick branches
Headline result
With RL plus RMaxTS at a sample budget of 32 x 6400 (mixture of two guiding prompts) it reaches 63.5% on miniF2F-test; on the ProofNet test set it reaches 25.3% at a budget of 4 x 6400. The paper calls both new state of the art at publication.
What this does not prove
Numbers depend heavily on sample budget: the same model gets 50.0% to 54.9% at 32 to 3200 samples without search. The ProofNet validation set was used for expert iteration, so the test column is the clean one.
How it generalizes the harness
- A domain authority judges
- Feedback retrains the generator
- Search over a population
- The output outlives the model
Lean is the judge, its verdicts retrain the model weights, and a tree of many partial proofs is searched; the finished proof is checkable without the model.
Classification
| What it proposes | Proof |
|---|---|
| Generative model | DeepSeek-Prover-V1.5 (DeepSeekMath-Base fine-tuned for Lean 4) |
| Algorithmic authority | Lean 4 proof assistant |
| Feedback | Reward signal |
| What gets updated | Model weights and search tree |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |