Organizations: Peking University · IQuest Research · Beijing International Center for Mathematical Research and the New Cornerstone Science Laboratory, Peking University · Center for Machine Learning Research, Peking University · Center for Intelligent Computing, Great Bay Institute for Advanced Study, Great Bay University · Zhongguancun Academy
We present Reap, an open framework for learning and analyzing formal proof search in Lean4. Reap implements policy-value-guided Monte Carlo Tree Search directly in Lean, sharing proof-state transitions, AND-OR search, and replay verification between inference and training rollouts. Structured action logs expose how neural predictions and tactic execution interact during search. Using this framework, we train Reaper-1, a 1.7B-parameter policy-value model, through continued pre-training, supervised tactic learning, and iterative search-based reinforcement learning. Using a separate premise selector, the final system solves 79.9% of miniF2F-test at pass@32, establishing state-of-the-art performance among open provers of comparable size while remaining competitive with substantially larger models. Beyond improved solve rates, our results suggest that RL strengthens the prover's ability to organize proofs around useful intermediate results, favoring substantial advances over repeated local adjustments. This more directed proof construction is accompanied by increasingly elaborate tactic programs: fewer explicit search decisions are needed, while more work is performed within each decision. The resulting trade-off between search effort and tactic execution cost provides insight into how learning changes the prover's problem-solving strategy.
Figures & tables
Figure 1: Overview of Reap’s proof-search and learning interface. A shared policy–value backbone and a fixed premise retriever provide guidance to Monte Carlo Tree Search running inside Lean’s tactic monad, where native proof-state transitions are selected, expanded, evaluated, and backed up. Successful proofs are checked by Lean’s kernel and exposed through traces and replay; the same interface supports reinforcement-learning rollouts and inference, enabling transparent analysis of how training changes proof structure and computation within each action.
Figure 2: Overview of Reap’s training pipeline and Lean-native MCTS. In the backup rule, OR/AND labels refer to the successor node’s type. Both Q(s,a) and the return v account for the edge cost: one for tactic edges and zero for synthetic focus edges. Here, M(s) counts direct policy–value evaluations.
System
Budget
miniF2F
ProofNet
FATE-M
PutnamBench
CombiBench
Whole-proof systems
DeepSeek-Prover-V2-7B ( Ren et al., 2025 )
pass@32
75.6%
–
–
9/660
6 (pass@16)
Goedel-Prover-V2-8B ( Lin et al., 2026 )
pass@32
84.6%
–
–
25/660
–
Kimina-Prover-7B ( Wang et al., 2025 )
pass@32
78.3%
–
–
–
7 (pass@16)
Kimina-Prover-RL-1.7B ( Wang et al., 2025 )
pass@32
76.6%
–
–
–
–
Pythagoras-Prover-4B ( Leang et al., 2026 )
pass@32
86.1%
–
–
–
–
Table 1: Main benchmark results. “–” indicates that the corresponding result was not reported by the original work.
Figure 3: Reinforcement-learning progression. (a) Retrospective evaluation on miniF2F-test at 8,192 MCTS simulations and pass@8. (b) Pass@1 on the full RL training corpus. (c) Sequential RL5 small-batch evaluation; the dashed horizontal line marks the B00 value (48.26%).
Model
Solved
Avg. tactic steps
Avg. root value
RL5
195
16.4553
-9.9174
RL5 w/o value head
193
17.4435
-11.0221
Table 2: Value-head ablation on miniF2F-test with 8,192 simulations and pass@32. Tactic steps are computed by first averaging proved passes within each theorem and then averaging equally across theorems. Average tactic steps and root value are computed on the both-solved 193 problems.
Retriever
PS-2
MePo
SineQuoNon
Pass@32
79.9% (195/244)
67.6% (165/244)
75.8% (185/244)
Table 3: Inference-time retriever replacement on miniF2F-test with the same RL5 checkpoint and 8,192 MCTS simulations per search. PS-2 is neural; MePo and SineQuoNon are rule-based. Parentheses give solved/total problems.
MCTS budget
512
1024
2048
4096
8192
Pass@32
77.05%
78.28%
79.51%
79.51%
79.92%
Table 4: Search scaling of Reaper-1 on miniF2F-test under pass@32.
Metric
SFT
RL4
RL5
Pass@32
62.3%
78.3%
79.9%
Mean proof steps
21.7
11.2
5.2
Mean search-tree nodes
2,368
162
119
Median action characters
19
23
66
Tactic identifiers/action
1.38
1.38
2.80
Actions containing <;>
2.9%
4.5%
23.9%
Table 5: How reinforcement learning reshapes proof search. Coverage uses all 244 miniF2F-test problems; proof and action statistics use the 151-problem common solved set.
Appendix figures & tables10 assets
Supplementary material from the paper’s appendix.
Appendix
Parameter
Value
Search algorithm
MCTS
Maximum MCTS simulations
8,192
Maximum tree nodes
65,536
Independent attempts
32
Policy samples/state
6
Retrieved premises/state
8
Appendix
Table 6: MCTS and inference hyperparameters used in the controlled miniF2F experiments.
Setting
Configuration
CPT global batch size
1,024
CPT learning rate
3×10−4→3×10−5
CPT schedule
Cosine decay
RL learning rate
2×10−5→5×10−7
RL policy/value loss-weight ratio λP:λV
1:0.3→1:0.05
RL1 MCTS budget
512 simulations/search
Appendix
Table 7: Training hyperparameters for Reaper-1.
Metric
SFT
RL4
RL5
Pass@32
152 (62.3%)
191 (78.3%)
195 (79.9%)
Proof steps, mean
21.7
11.2
5.2
Proof steps, median [IQR]
7 [2, 18]
2 [1, 8.5]
2 [1, 3.5]
One-step proofs
23.2%
49.0%
49.0%
Tree nodes, mean
2,368
162
119
Tree nodes, median [IQR]
901 [10, 3,891]
3 [2, 18]
3 [2, 7]
Appendix
Table 8: Coverage and successful-search efficiency across checkpoints. Coverage uses all 244 miniF2F-test problems; the remaining rows use one canonical proof for each of the 151 problems solved by all three checkpoints.
Figure 4: Verified proof length and successful-search tree size on the paired 151-problem common core. Each checkpoint contributes one earliest-success canonical proof per theorem. Boxes show the interquartile range and the annotated line is the median; both axes are logarithmic.
Figure 5: Outer-head tactic composition with a shared taxonomy and legend. (a) Action-weighted shares on the paired common core across checkpoints. (b) Shares across online-RL rollout batches.
Metric
SFT
RL4
RL5
Action characters, median
19
23
66
Tactic identifiers/action
1.38
1.38
2.80
Contains <;>
2.9%
4.5%
23.9%
Multiline action
7.0%
3.5%
24.7%
Contains nested := by
1.5%
3.8%
17.5%
Explicit retrieved-premise use
6.4%
7.8%
19.5%
Appendix
Table 9: Granularity of canonical-proof actions on the paired common core. “Identifiers/action” counts tactic identifiers lexically throughout each action, including nested blocks.
Metric
SFT
RL4
RL5
Completed evaluator calls
24.57M
18.01M
5.99M
Tactic chars, median [IQR]
47 [19, 87]
25 [15, 47]
89 [57, 159]
Latency ms, median [IQR]
12.0 [5.4, 35.0]
15.2 [4.4, 74.6]
43.2 [9.7, 229.2]
Evaluator accepted
58.1%
61.3%
35.0%
Calls exceeding 1 second
1.85%
3.84%
9.73%
Calls/problem, median
29,512
992.5
257
Appendix
Table 10: Search-wide Lean tactic evaluations. Counts and rates are exact over all completed calls; quantiles use a deterministic 200,000-call uniform reservoir per run. Summed duration is overlapping service time, not wall-clock runtime.
Figure 6: Search-wide distributions of generated tactic length and Lean evaluation latency. Boxes show the interquartile range, whiskers show the 5th and 95th percentiles, and annotations mark medians. Each run contributes a uniform 200,000-call reservoir; axes are logarithmic.
Figure 7: Canonical-proof granularity across online-RL batches: (a) median action length, (b) compound-action share, (c) median top-level proof steps, and (d) median proof-text length.
Figure 8: Search-wide tactic-evaluation trends across online-RL batches: (a) median tactic length, (b) median evaluation latency, (c) acceptance rate, and (d) median evaluation calls per problem.