Summary (Overview)

• Reap is an open framework implementing policy–value-guided Monte Carlo Tree Search (MCTS) directly as a Lean 4 tactic, enabling native proof-state transitions, AND–OR search, and replay verification.
• Reaper-1, a 1.7B-parameter policy–value model, achieves 79.9% pass@32 on miniF2F-test, establishing state-of-the-art performance among open provers of comparable size.
• The system demonstrates strong transfer across four additional benchmarks: 33.9% on ProofNet-test, 81.3% on FATE-M, 21/660 on PutnamBench, and 7/100 on CombiBench.
• Reinforcement learning induces a "search-interaction compression" effect: shorter proof trajectories with fewer top-level search decisions, but more compound tactics performing greater computation per action.
• The framework provides high observability through structured action logs, enabling detailed statistical analysis of how training reshapes proof-search behavior.

Introduction and Theoretical Foundation

Formal theorem proving offers a rigorous testbed for machine reasoning: proof assistants expose explicit proof states and verify completed proofs with a trusted kernel. Recent systems like Kimina-Prover, DeepSeek-Prover-V2, and Seed-Prover achieve strong performance with increasingly large models, while step-level reinforcement learning has substantially improved neural theorem provers.

The paper identifies a key gap: while high-performing provers achieve impressive results, they are often difficult to study independently due to limited implementation access or substantial computational requirements. The authors' central goal is combining strong theorem-proving performance with an accessible and observable search framework.

The theoretical foundation builds on:

• AlphaProof-style expert iteration (Hubert et al., 2026): policy–value-guided tree search coupled with iterative reinforcement learning
• HyperTree Proof Search (Lample et al., 2022): AlphaZero-inspired search over AND–OR structure of proof obligations
• RMaxTS (Xin et al., 2025): MCTS variant encouraging exploration over intermediate tactic states

Methodology

Reap: Lean-Native Monte Carlo Tree Search

Reap implements the search loop directly inside Lean's tactic monad, with key design elements:

Native proof states and tactic evaluation:

• State transitions manipulate Lean's proof-state objects directly using built-in save/restore primitives
• Each node stores a Tactic.SavedState; tactic execution is bounded by Lean heartbeats and wall-clock timeouts
• Unsuitable tactics (e.g., sorry, simp?) are filtered before elaboration

AND–OR proof search:

• OR nodes represent tactic choices (solved when any child is solved)
• AND nodes represent independent proof obligations (require all children solved)
• Multiple goals decompose into AND nodes only when they contain no unresolved expression metavariables

Progressive sampling and PUCT: New tactics are sampled according to:

$$M(s) \leq C N(s)^{\alpha}.\tag{1}$$

Child selection uses the PUCT score:

$$\mathrm{PUCT}(s, a) = \gamma^{-V(s,a)-1} + c(N(s)) P(s,a) \frac{\sqrt{N(s)}}{1 + N(s,a)},\tag{2}$$

where the exploration coefficient is:

$$c(N) = c_{\mathrm{init}} + \log \frac{N + c_{\mathrm{base}} + 1}{c_{\mathrm{base}}},\tag{3}$$

Here, $P(s,a)$ is the normalized policy prior, and $V(s,a) = \bar{v}(s') - d(a)$ is the child node's value estimate after subtracting edge cost $d(a)$, where $d(a) = 1$ for tactic edges and $d(a) = 0$ for synthetic focus edges.

State deduplication: Serialized pretty-printed proof-states prevent duplicate nodes on the MCTS path and merge repeated tactic text within sampling batches.

Proof reconstruction: Replays selected tactics from the root and validates via Lean's ordinary declaration-checking pipeline.

Reaper-1: Model and Training

Architecture: 1.7B-parameter model initialized from Qwen3-1.7B-Base with:

• Shared Transformer backbone for both policy and value prediction
• Policy head: autoregressive tactic generation conditioned on proof state and premises
• Value head: discretized value representation estimating remaining proof-search cost

Training stages:

1. Continued pre-training (CPT): On FineLeanCorpus, LeanWorkbook, NuminaMath-Lean, DeepSeek-Prover-V1 data, and Mathlib v4.28.0-rc1
2. Supervised fine-tuning (SFT): Step-level examples from existing Lean proofs with retrieved premises
3. Iterative reinforcement learning: Five stages of MCTS-guided RL on ~25K curated AoPS problems, with budgets increasing from 512 to 8,192 simulations

Policy–value training objective:

$$\begin{array}{r l} & \mathcal{L} = \lambda_{P} \big(\underbrace{-\mathbb{E}_{(s,a,y)\sim\mathcal{D}_{\mathrm{RL}}}[\log \pi_{\theta}(a \mid s)]}_{\mathcal{L}_{\mathrm{policy}}}\big) \\ & \qquad + \lambda_{V} \big(\underbrace{-\mathbb{E}_{(s,a,y)\sim\mathcal{D}_{\mathrm{RL}}}[\log p_{\theta}(y \mid s)]}_{\mathcal{L}_{\mathrm{value}}}\big). \end{array}\tag{4}$$

Value targets are backed up through the AND–OR tree and discretized into $K = 32$ bins.

Premise selector: PS-2, a separately trained Qwen3-Embedding-8B selector following the LeanSearch-PS recipe, remains fixed during RL.

Empirical Validation / Results

Main Results

Table 1: Main benchmark results ("–" indicates results not reported by the original work)

Ablation Studies

Value head ablation (8,192 simulations, pass@32, on 193 both-solved problems):

Premise retriever replacement (same RL5 checkpoint):

Search Scaling

Coverage begins to saturate at 2,048 simulations, with diminishing returns at larger budgets.

How RL Reshapes Proof Search

Table 5: Proof and action statistics (151-problem common solved set across checkpoints):

Theoretical and Practical Implications

Search-interaction compression: RL reduces the number of top-level search decisions while shifting more proof construction and solver work into each individual action. This suggests that the model becomes better at:

• Identifying useful intermediate structural lemmas
• Concentrating proof attempts on steps that make substantive progress
• Reducing reliance on repeated local manipulations

Value guidance effectiveness: Enabling value guidance biases MCTS toward shorter successful trajectories, with both fewer tactic steps and root values closer to zero.

Retriever independence: The learned prover operates effectively with rule-based retrievers (75.8% with SineQuoNon vs. 79.9% with PS-2), supporting inference-time replacement of the neural retrieval component.

Practical accessibility: The entire system uses only 60 NVIDIA A100 GPU days for RL training, and evaluating all 244 miniF2F-test problems at pass@32 takes approximately 3 hours using 32 A100 GPUs and 800 CPU cores.

Conclusion

The paper introduces Reap, an open MCTS framework whose semantics-critical search loop runs directly inside Lean, and Reaper-1, a lightweight 1.7B-parameter policy–value model achieving strong performance across multiple Lean benchmarks. The analysis reveals that search-based RL refines proof strategy, enabling effective use of auxiliary lemmas and more direct routes to complete arguments.

Key limitations and future directions:

• The number of tactic-level search actions as a proxy for proof cost may not reflect actual complexity; future objectives could incorporate tactic execution time, generated-token length, or finer-grained action complexity measures
• The extent to which these dynamics generalize to substantially larger models or other proof assistants remains to be studied
• As individual tactics take on larger roles in local reasoning, closer attention to their computational demands is needed

The framework supports further research on training objectives that encourage meaningful proof progress, making learning dynamics accessible to systematic study.