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.
MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs. It is built from three agent types (Planning, Check, and Lean) composed by a recursive outer loop whose unit of revision is the proof plan itself, and uses no fine-tuning, no custom RL objective, and no theorem-specific scaffolding. On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23, surpassing the strongest published open-source baseline (OpenGauss, 8/23). On Putnam2025, the same harness closes 12/12 with substantially lower total wall-clock than the next-best system that closes the full set. The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones. These results suggest that harness design is a central factor in end-to-end Lean4 theorem proving, alongside raw model capability, and that a relatively simple harness can already be effective.
Jinzheng Li, Zeru Zhu, Yuanjie Ren
1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology
Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both supervised fine-tuning (SFT) and sampling expensive. We introduce Pythagoras-Prover, a compute-efficient open-source family of Lean theorem provers built for practical compute budgets. The family spans two generation paradigms: autoregressive models at 4B and 32B parameters, and a first proof-of-concept diffusion-based prover (4B) that iteratively refines Lean proofs at inference time. For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT, so models acquire proof skills progressively from shorter, simpler proofs to longer, harder ones. During SFT, a dynamic proof-reasoning filtering scheme preserves informative proof traces while keeping each instance within an 8k-token context budget. We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements, populated via self-distillation for extra training signal without formally verifying every mutated instance. By perturbing known problems while preserving their formal character, ALF reduces reliance on any statement's surface form. Empirically, Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test (86.1% vs 82.4%) with ~167x fewer parameters, while Pythagoras-Prover-32B sets the open-source state of the art at 93.0% on MiniF2F-Test and solves 93 of 672 PutnamBench problems. We release MiniF2F-ALF, an ALF-mutated contamination-sensitive benchmark on which every evaluated model loses accuracy; here our 32B remains strongest and our 4B matches the prior state of the art, Goedel-Prover-V2-32B.
Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian +5
Imperial College London · University of Edinburgh · Nanyang Technological University +1
We introduce NanoProof, to our knowledge the first factorized execution-guided theorem prover in Lean 4 whose training data, extraction tooling, training pipeline, and weights are all released, making it end-to-end reproducible using open-source resources. To this end, we build and release a dataset of structured proof trees, as well as a tool for programmatic interaction and data extraction within the Lean 4 formal verifier. To support sustainable research, we focus on compute efficiency to facilitate accessible training and evaluation. NanoProof achieves 50.8% pass@16 on MiniF2F-Test, exceeding the two closest systems of its class, HyperTree Proof Search and ABEL, at roughly 90x and 7x less compute, and using more than four orders of magnitude less compute than AlphaProof. Stronger open-weight provers exist, but they are fine-tuned from large pretrained language models and release neither training data nor pipeline; NanoProof shows that the factorized execution-guided class of provers can be rebuilt from scratch with modest resources.
Matěj Kripner, Milan Straka
Institute of Formal and Applied Linguistics, Faculty of Mathematics and Physics, Charles University Prague, Czech Republic