DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

ArXiv: 2408.08152

🎯 Pitch

Giving up on intermediate proof steps cripples theorem proving—until now. DeepSeek-Prover-V1.5 learns from a proof assistant’s online binary feedback and uses a new intrinsic-reward-driven search to explore tactic states it has never seen, smashing prior records on the miniF2F (63.5%) and ProofNet (25.3%) benchmarks by turning partial proofs into stepping stones instead of dead ends.

---

1. Executive Summary

This paper introduces DeepSeek-Prover-V1.5, an open-source 7B-parameter language model for formal theorem proving in Lean 4 that integrates reinforcement learning from proof assistant feedback (RLPAF) — using binary verification results from the Lean prover as rewards to fine-tune via GRPO — with a novel Monte-Carlo tree search variant called RMaxTS — an intrinsic-reward-driven exploration algorithm that awards maximal reward for discovering unseen tactic states, combined with discounted upper confidence bounds to handle non-stationary rewards — to bridge whole-proof generation and proof-step search through a truncate-and-resume mechanism that parses generated proofs at the first verification error and resumes from intermediate tactic states. DeepSeek-Prover-V1.5 achieves new state-of-the-art pass rates of 63.5% on the miniF2F-test benchmark (a 13.5 percentage-point absolute improvement over DeepSeek-Prover-V1's 50.0%) and 25.3% on the undergraduate-level ProofNet benchmark, establishing that the combination of online RL and exploration-oriented tree search yields substantial gains across difficulty levels, while the intrinsic-reward mechanism proves essential — ablations show that removing it causes tree search performance to degenerate to parity with non-search single-pass generation, confirming that sparse extrinsic rewards alone cannot drive effective proof-space exploration.

2. Context and Motivation

The Core Problem: Bridging the Gap Between Neural and Symbolic Reasoning in Formal Theorem Proving

This paper addresses a fundamental tension at the heart of AI for formal mathematics: language models are effective generators of proof code, but they lack access to the intermediate logical states that determine whether their reasoning is valid. In formal theorem proving systems like Lean 4 (Moura and Ullrich, 2021), proofs are constructed as sequences of tactics — commands that transform the current proof goal into simpler subgoals until no goals remain. Each tactic application produces a new tactic state (the set of remaining goals and available hypotheses), and the proof assistant verifies every step mechanically. This means the ground truth is perfectly accessible at every intermediate point. Yet the dominant paradigm for neural theorem proving, whole-proof generation, throws away this rich intermediate signal entirely: the language model generates the complete proof code in one shot, the prover checks the final result, and the model receives only a binary pass/fail verdict at the end.

The problem is not merely one of inefficient feedback. The authors identify a more subtle issue in Section 1, which they connect to the compounding error phenomenon from imitation learning (Ross et al., 2011):

"In Lean's tactic mode, proofs are constructed through a sequence of tactics that transform the proof state. This sequential nature introduces the risk of compounding errors, where a single misinterpretation can lead to significant deviations from a valid proof path. More specifically, the auto-regressive model may have incorrect believes on intermediate tactic states when generating long proofs."

This is the central gap the paper addresses. When a language model generates a 20-tactic proof autoregressively, it never observes the actual tactic states produced by tactics 1 through 19. It must maintain an implicit, learned internal representation of what the state should be after each step — a representation that can silently drift, causing later tactics to operate on assumptions that are inconsistent with the real proof state. The model writes code as if it were at goal G, but the proof assistant's actual state is G', and the mismatch compounds with each subsequent tactic. The binary pass/fail signal at the end provides no gradient about where the drift began or what the correct intermediate representation should have been.

Why This Problem Matters

The importance of this problem extends beyond theorem proving into the broader landscape of AI reasoning. Formal mathematics represents one of the few domains where correctness is fully verifiable — there is no ambiguity, no approximate grading, no need for human judgment. This makes it an ideal testbed for studying the fundamental capabilities and limitations of neural-symbolic integration. If language models cannot effectively utilize intermediate symbolic feedback even when it is perfectly available, that signals a deeper architectural limitation in how they perform multi-step logical reasoning.

On the practical side, the paper positions formal theorem proving as a critical capability for several downstream applications (Section 5, implicitly):

• Mathematical research assistance: Automating routine proof steps and verifying complex derivations could accelerate mathematical discovery. The gap between current models (~63% on high-school competition problems) and the frontier of mathematical practice remains large, and improvements in intermediate feedback utilization are a plausible path to narrowing it.
• Software verification: The same formal reasoning infrastructure that proves mathematical theorems can verify program correctness properties. Many verification tasks share the structure of long-horizon sequential reasoning where intermediate state tracking is essential.
• Self-improving AI systems: Formal verification provides an oracle reward signal — a rare and valuable property. Systems that can learn effectively from this signal, by decomposing it into step-level feedback, could form the basis for self-improving reasoning agents that generate and verify their own chains of thought.

The paper's framing also connects to a broader trend in the field: the shift from training-time scaling (bigger models, more data) toward inference-time compute scaling (search, iterative refinement, planning). The observation that test-time search can substitute for model scale — familiar from game-playing systems like AlphaZero (Silver et al., 2018) — is underexplored in theorem proving, where the search space is combinatorially explosive and the reward signal is extremely sparse. This paper explicitly aims to fill that gap by developing search methods that work under sparse-reward conditions.

Prior Approaches and Their Shortcomings

The paper categorizes existing neural theorem proving methods into two strategies, analyzed in Section 3.5. Understanding their respective weaknesses is essential to understanding why the paper's hybrid approach is motivated.

Strategy 1: Single-Pass Whole-Proof Generation

In this paradigm, the language model receives the theorem statement (and possibly a natural language description) and generates the entire proof script in one autoregressive pass. The proof is then submitted to the Lean prover. If it compiles and closes all goals, success; otherwise, the model tries again from scratch in the next attempt. Methods in this category include DSP (Jiang et al., 2022), Subgoal-Prover (Zhao et al., 2023), LEGO-Prover (Wang et al., 2023), Lyra (Zheng et al., 2023), miniCTX (Hu et al., 2024), and the paper's own predecessor, DeepSeek-Prover-V1 (Xin et al., 2024).

This approach has significant practical advantages. It is computationally efficient: the model and the theorem prover communicate only once per attempt. There is no overhead from repeatedly invoking the prover, parsing intermediate states, and feeding them back to the model. This matters enormously at scale — the paper notes that DeepSeek-Prover-V1 achieved state-of-the-art results using this paradigm precisely because it could generate thousands of proof attempts with minimal coordination cost.

However, the weaknesses are equally significant. Beyond the compounding error problem discussed above, the whole-proof approach provides no mechanism for incremental improvement. If a 50-tactic proof fails at tactic 47 because of a subtle type error, the model receives no information about which earlier tactic caused the problem or what the correct intermediate state should have been. It must generate entirely new proofs, potentially repeating the same successful initial tactics in slightly different variants without learning which parts were actually correct. The binary reward signal is perfectly accurate but structurally impoverished — it cannot decompose credit across the proof's internal structure.

The paper's predecessor, DeepSeek-Prover-V1, achieved 50.0% on miniF2F-test using this approach (with 16 × 4096 = 65,536 total proof attempts), which demonstrates the power of sheer scale. But it also illustrates the ceiling: doubling or quadrupling the sample budget yields rapidly diminishing returns because the model cannot learn which parts of its proofs are reliable.

Strategy 2: Multi-Pass Proof-Step Generation

In this paradigm, the prover model generates one tactic at a time, the tactic is submitted to the proof assistant, and the resulting tactic state is fed back to the model before generating the next tactic. This interleaves generation with verification, giving the model access to ground-truth intermediate states at every step. Methods include GPT-f (Polu and Sutskever, 2020; Polu et al., 2022), Thor (Jiang et al., 2022), ReProver (Yang et al., 2023), Hypertree Proof Search (Lample et al., 2022), Lean-STaR (Lin et al., 2024), and InternLM2-StepProver (Wu et al., 2024).

This approach directly addresses the compounding error problem: after each tactic, the model sees exactly what goals remain, what hypotheses are available, and what the current context is. There is no drift between the model's implicit state and the prover's actual state because the model's context is reset to reality at every step.

However, this comes at a steep cost. Each proof attempt requires potentially dozens of round-trips between the model and the prover, each involving: (1) the model generating a single tactic, (2) the prover parsing and executing it, (3) extracting the resulting tactic state, (4) formatting it for the model's context window, and (5) the model generating the next tactic. This multiplies the communication cost by the proof length, creating a bottleneck in proof-per-second throughput. It also complicates training: the training data format (interleaved tactic states and tactic predictions) is more complex than simple code completion, requiring careful extraction of intermediate states from the prover.

Moreover, multi-step methods typically require separate models or objectives for the step-generation task, which differs from standard language model pre-training. This creates a gap between the model's pre-training objective (next-token prediction on text) and its deployment task (tactic prediction conditioned on prover state), potentially wasting the knowledge acquired during pre-training.

The Gap Neither Strategy Addresses: Effective Exploration Under Sparse Rewards

Both existing strategies share a deeper limitation that the paper identifies in Section 3.3: the reward signal for proof search is extremely sparse. Whether you generate whole proofs or single steps, the only non-zero reward comes from completely solving the theorem. Partial progress — proving a lemma, reducing the goal to a simpler form, discovering a useful intermediate fact — yields no explicit reward.

This is not merely an inconvenience; it is a fundamental exploration problem. The search tree for a typical theorem is enormous, with most paths leading to dead ends. Without any reward gradient to follow, search algorithms default to essentially random exploration, which becomes exponentially inefficient as proof length grows. The paper explicitly frames this as matching "a famous hard-exploration case (Krishnamurthy et al., 2016) in the literature of statistical reinforcement learning" (Section 3.3).

Prior proof search methods like Hypertree Proof Search (Lample et al., 2022) used standard MCTS with extrinsic rewards only (1 for success, 0 otherwise), relying entirely on the UCB exploration bonus to drive search. The authors' ablation study (Figure 5) demonstrates the consequences: without intrinsic rewards, tree search degenerates to single-pass generation performance because the UCB bonus alone cannot overcome the reward sparsity.

How This Paper Positions Itself

The paper's position is not to argue for one strategy over the other, but rather to unify them through a novel truncate-and-resume mechanism that inherits the efficiency of whole-proof generation while incorporating intermediate tactic state information from the proof assistant. This is a genuinely hybrid approach: the model generates complete proofs (whole-proof paradigm), but when verification fails, the system truncates at the first error, extracts the successful prefix as individual tactic applications, and resumes generation from the intermediate tactic state (proof-step paradigm). Critically, this is integrated directly into the MCTS framework: the truncation points are not deterministic (always at the first error) but are scheduled by the tree search policy, allowing the system to explore alternative continuations from any node in the tree.

The paper explicitly contrasts this with both existing strategies in Section 3.5:

"Our proof tree search method uniquely bridges these two strategies, offering a novel hybrid approach. It starts with whole-proof generation, similar to the single-pass approach, but extends this by implementing a sophisticated truncate-and-resume mechanism."

This is not merely an engineering convenience. It means the same model, trained with a unified objective (described in Section 2.2), can operate in both modes: single-pass whole-proof generation when speed matters, and tree search with intermediate state feedback when problem difficulty demands it. The model is trained during supervised fine-tuning to predict both the next tactic and the intermediate tactic state (as an auxiliary objective), creating a shared representation that serves both deployment modes.

Beyond the architectural unification, the paper positions its RMaxTS algorithm as a fundamental contribution to proof search methodology. The core insight is that exploration in theorem proving should not be driven by extrinsic rewards alone (which are too sparse) but by intrinsic rewards for discovering novel tactic states. This is an application of the RMax principle (Brafman and Tennenholtz, 2002) to the tree search setting: the agent receives a reward of 1 whenever it adds a previously unseen node to the search tree, and 0 otherwise. Because multiple tactic sequences can lead to the same tactic state, this reward implicitly encourages the agent to discover semantically distinct proof approaches rather than syntactically varied ones that converge to the same state.

The paper positions this against the standard UCT (Kocsis and Szepesvári, 2006) MCTS baseline used in prior work, and demonstrates through ablation (Figure 5) that intrinsic rewards are not a minor enhancement but are essential for tree search to outperform single-pass generation. Without them, the search degenerates to blind sampling.

The paper also positions its discounted UCB (DUCB) mechanism (Garivier and Moulines, 2011) as a crucial complement to intrinsic rewards. Standard UCB1 (Auer et al., 2002) assumes stationary reward distributions — the expected value of an action does not change over time. But intrinsic rewards are inherently non-stationary: the probability of discovering a new tactic state decreases as the search tree grows, because most reachable states have already been visited. Standard UCB1 weights all historical observations equally, causing the value estimates to be dominated by stale data from early exploration. DUCB applies a discount factor ($\gamma = 0.99$) to historical rewards, ensuring that recent observations — where intrinsic rewards are harder to obtain — have proportionally greater weight in the value estimate. This accelerates the propagation of non-stationary reward signals through the tree.

This dual mechanism — RMax intrinsic rewards for exploration, DUCB for non-stationary value estimation — is the paper's algorithmic contribution to the tree search literature, specifically adapted to the unique properties of formal proof spaces.

The paper also positions its reinforcement learning from proof assistant feedback (RLPAF) as a distinct contribution relative to prior work on RL for mathematical reasoning. While DeepSeekMath (Shao et al., 2024) showed that RL primarily improves the model's ability to select correct answers from a set of candidates (boosting pass@K), the authors argue (Section 2.4, Figure 3) that in formal theorem proving, RL produces a genuine enhancement of fundamental capabilities — improving pass@1 as well as pass@K, with gains that remain stable as the sample budget increases. They attribute this to the unique nature of the feedback: binary verification from the proof assistant provides perfectly accurate (if sparse) reward signals, unlike the approximate reward models used in natural language math reasoning.

Finally, the paper positions the entire pipeline — pre-training, supervised fine-tuning with thought augmentation and tactic state prediction, RLPAF, and RMaxTS — as laying groundwork for what it calls "an AlphaZero-like pipeline for formal theorem proving" (Section 5). The parallel is explicit: just as AlphaZero combined a learned policy/value network with MCTS to achieve superhuman performance through self-play, the paper envisions a system where the prover model (policy), a future critic model (value function), and tree search (planning) form a closed loop, with the proof assistant acting as the perfect environment oracle. The current work focuses on the exploration aspect of this pipeline; the exploitation aspect — training a critic to evaluate partial proofs — is flagged as the key next step for future work.

In summary, the paper addresses a clear gap — the inability of existing neural theorem provers to effectively utilize intermediate proof assistant feedback while maintaining computational efficiency — through a three-part contribution: (1) a training pipeline that teaches the model to predict intermediate tactic states alongside proof code, enabling a unified whole-proof and proof-step capability; (2) RLPAF, which uses the proof assistant's binary verification as an accurate (if sparse) reward signal to improve fundamental model capability beyond what SFT achieves; and (3) RMaxTS, an exploration-oriented MCTS algorithm that uses intrinsic rewards for discovering novel tactic states and discounted UCB for non-stationary value estimation, enabling effective tree search under the extreme reward sparsity characteristic of formal theorem proving.

3. Technical Approach

3.1 Reader Orientation

This paper is primarily a systems and algorithms paper with strong empirical validation: the core idea is that you can build a state-of-the-art neural theorem prover by training a language model to predict not only proof code but also intermediate tactic states (enabling a hybrid whole-proof/step-wise proving capability), then fine-tuning it with reinforcement learning using the proof assistant's binary verification as a reward signal, and finally deploying it with a novel Monte-Carlo tree search algorithm that uses intrinsic rewards for discovering unseen tactic states to overcome the extreme reward sparsity of theorem proving.

The system solves the problem that whole-proof generation is efficient but suffers from compounding errors due to lack of intermediate state feedback, while proof-step generation provides rich feedback but is computationally expensive due to repeated model-prover communication; the solution's "shape" is a unified model trained with an auxiliary objective to predict tactic states, coupled with a truncate-and-resume mechanism that lets the same model serve both deployment modes, and an exploration-driven tree search that bridges the gap between these modes by treating the proof tree as a search problem where the reward for finding novel states drives systematic exploration.

3.2 Big-Picture Architecture (Diagram in Words)

The system has four major components connected in a training-then-inference pipeline:

1. Pre-training (Section 2.1): The base language model (DeepSeekMath-Base 7B) undergoes additional pre-training on formal mathematical languages (Lean, Isabelle, Metamath) and mathematical reasoning data, producing DeepSeek-Prover-V1.5-Base.

2. Supervised Fine-Tuning (Section 2.2): The pre-trained model is fine-tuned on an augmented dataset of 9.645 million Lean 4 proof sequences. Each training example includes: (a) theorem statements with natural language chain-of-thought comments inserted by DeepSeek-Coder V2 236B, and (b) intermediate tactic state information inserted as comments at each proof step. The model learns to predict both the natural language reasoning and the subsequent tactic code, with tactic state tokens as an auxiliary prediction objective. This produces DeepSeek-Prover-V1.5-SFT.

3. Reinforcement Learning from Proof Assistant Feedback — RLPAF (Section 2.3): The SFT model is further trained using GRPO (Group Relative Policy Optimization) on a filtered subset of approximately 4,500 theorem statements. For each theorem, the model generates 32 candidate proofs; the Lean 4 prover verifies each, assigning a reward of 1 for correct proofs and 0 otherwise. The GRPO algorithm optimizes the model based on the relative rewards within each group, using a KL divergence penalty to constrain deviation from the SFT model. This produces DeepSeek-Prover-V1.5-RL.

4. Monte-Carlo Tree Search with RMaxTS (Section 3): At inference time, the RL model can be deployed in either single-pass generation mode or tree search mode. The tree search uses a truncate-and-resume mechanism: the model generates whole proofs, the proof is parsed into tactics and submitted to the Lean prover, the proof is truncated at the first verification error, the successful prefix is decomposed into individual tactic steps (each becoming a node in the search tree), and subsequent generations resume from intermediate tactic states (with the current tactic state appended as a comment). The RMaxTS algorithm drives the search using intrinsic rewards — the agent receives a reward of 1 whenever an expansion adds at least one new node to the tree — combined with discounted upper confidence bounds (DUCB) to handle the non-stationary nature of these intrinsic rewards as the tree grows.

Information flows as follows: a theorem statement enters the system → the language model generates a whole-proof completion → the Lean prover verifies it → if correct, the system terminates; if incorrect, the proof is truncated at the first error → the successful prefix is parsed into a chain of tactic nodes → the current tactic state is extracted from the Lean prover → this state is used to prompt the next generation attempt → the tree search policy (RMaxTS) selects which node to expand next based on accumulated intrinsic rewards and UCB exploration bonuses → the process repeats until a correct proof is found or the sample budget is exhausted.

3.3 Roadmap for the Deep Dive

• First, the supervised fine-tuning data pipeline and training procedure (Section 2.2), because the truncate-and-resume mechanism that unifies whole-proof and step-wise generation depends critically on the model being trained to predict intermediate tactic states and understand tactic state comments — without this, tree search cannot resume from intermediate states effectively.

• Second, the reinforcement learning from proof assistant feedback (Section 2.3), including the GRPO algorithm, the reward structure, and the prompt filtering strategy, because RLPAF produces the model that serves as the proposal distribution for tree search, and understanding why RL improves fundamental capabilities (not just top-K selection) is essential for interpreting the tree search results.

• Third, the tactic-level tree abstraction and truncate-and-resume mechanism (Section 3.1), because this is the interface between whole-proof generation and tree search — it defines how the continuous proof text gets decomposed into discrete tree nodes representing tactic applications, which is the foundation the search algorithm operates on.

• Fourth, the Monte-Carlo tree search algorithm (Section 3.2), including the selection policy, expansion procedure, and backpropagation, because this defines how the tree is traversed and grown, and the specific design choices (virtual nodes, multi-node expansion per iteration) adapt standard MCTS to the whole-proof generation setting.

• Fifth, the RMaxTS intrinsic reward mechanism and discounted UCB (Section 3.3), because this is the core algorithmic contribution — understanding why intrinsic rewards are necessary requires understanding the reward sparsity problem, and understanding why discounted UCB is necessary requires understanding the non-stationarity of intrinsic rewards.

• Sixth, the parallelization infrastructure (Section 3.4), because the practical feasibility of tree search with large language models depends on efficient parallelization across GPUs and CPU cores.

3.4 Detailed, Sentence-Based Technical Breakdown

Supervised Fine-Tuning: Dataset Construction and Training

The supervised fine-tuning stage produces a model that can (a) generate natural language chain-of-thought reasoning interleaved with Lean 4 proof code, and (b) interpret and generate tactic state comments that enable the truncate-and-resume mechanism. This involves three data augmentation techniques applied to proof data inherited from DeepSeek-Prover-V1.

Base data sources. The dataset is constructed from formal theorems sourced from Mathlib4 (the standard Lean 4 mathematics library), synthetic theorems from DeepSeek-Prover-V1 and Lean Workbook, and validation sets from miniF2F and ProofNet. The data curation follows an expert iteration process: the model generates proofs, verified proofs are added to the training set, the model is retrained, and the improved model generates more proofs, iterating. Between iterations, DeepSeek-Coder V2 236B (a 236B-parameter code-specialized model) annotates the thought process as comments. The final dataset consists of 9,645,000 sequences.

Thought-augmented proof generation. The core problem this addresses, identified in DeepSeek-Prover-V1, is a mismatch between how language models reason in natural language and how they generate Lean code. In natural language, models produce detailed step-by-step deductions. In Lean, they often resort to high-level tactic calls that "brute-force" solutions — powerful tactics like nlinarith or simp can close goals in one step, but this obscures the underlying mathematical reasoning and makes it harder for the model to decompose complex goals into structured subproblems.

The solution is to insert natural language chain-of-thought reasoning directly as comments within the proof code, in two forms. First, a complete natural language solution is inserted at the beginning of the proof block (before any tactics), describing the overall proof strategy. Second, for each tactic, a specific natural language step is inserted as a comment preceding that tactic, explaining what that step accomplishes and why. DeepSeek-Coder V2 236B generates these annotations from the existing proof code.

Training the model on this format teaches it to first articulate the mathematical reasoning and then translate that reasoning into precise tactic calls. This creates a behavior where the model's internal reasoning process is externalized in the generated text, which (a) improves proof quality by enforcing explicit reasoning before tactic generation, and (b) makes the proofs more interpretable. Two distinct guiding prompts differentiate between CoT mode and non-CoT mode during training and inference, with the CoT prompt instructing the model to "complete with explanatory comments preceding each line of code."

Prompt augmentation with tactic state information. This is the technical foundation for the truncate-and-resume mechanism. The authors enhance the Lean REPL (Read-Eval-Print Loop) with data extraction tools from LeanDojo to extract tactic information in triples: for each tactic application, they record the position of the tactic in the code, the tactic state before its application (the goals and hypotheses available at that point), and the tactic state after its application (the new goals and hypotheses).

For each tactic in a valid formal proof from the training data, the tactic state returned by the Lean prover is inserted as a comment block of the form /- tactic state: ... -/ immediately after the tactic that produced it. During training, the model's loss is computed differently on different parts of the sequence: all tokens following the /- tactic state: marker serve as responses (contributing to the supervised fine-tuning loss), while all tokens before this comment serve as prompts (contributing no loss). This means the model is explicitly trained to predict both the tactic state content and the subsequent proof steps when given a prefix that ends with a tactic state comment.

Why this design: training the model to generate tactic states (rather than just consume them) serves a dual purpose. At deployment, when the model receives an incomplete proof with a tactic state comment extracted from the Lean prover, it has been trained to attend to this information and use it to guide subsequent generation. Additionally, by making tactic state prediction an auxiliary task, the model develops internal representations that track the expected proof state, which reduces the compounding error problem — the model learns to predict what the state should be after each tactic, making it more likely to detect and correct discrepancies between its implicit beliefs and the actual prover state.

Training hyperparameters. Supervised fine-tuning is conducted on the pre-trained model for 9 billion tokens, with a batch size of 2,048 and a constant learning rate of $1 \times 10^{-4}$. The training process begins with 100 warm-up steps. Training examples are randomly concatenated to form sequences, with a maximum context length of 4,096 tokens. The authors note that this is a moderate context window relative to the length of some proofs, which suggests that longer proofs must either fit within this window or the model must handle them through the truncate-and-resume mechanism at inference time.

Reinforcement Learning from Proof Assistant Feedback (RLPAF)

The reinforcement learning stage takes the SFT model and further optimizes it using binary verification feedback from the Lean 4 prover. The goal is to improve the model's alignment with the formal specification of the proof system — generating proofs that not only look plausible but actually compile and close all goals.

Prompt selection. The RL stage uses a subset of theorem statements from the SFT dataset, filtered to retain only those for which DeepSeek-Prover-V1.5-SFT has a moderate success rate. This is a critical design choice: if the model can never solve a theorem (0% success rate), it receives no positive feedback and RL cannot improve its policy on that theorem; if it always solves a theorem (100% success rate), there is no room for improvement. The filtering ensures that each training prompt falls in a "zone of proximal development" where the model sometimes succeeds and sometimes fails, providing both positive and negative feedback signals.

After filtering, approximately 4,500 unique theorem statements remain. Each theorem is prefixed with both CoT and non-CoT guiding prompts, doubling the effective prompt set and ensuring the model improves in both generation modes.

Reward structure. The reward is defined simply: each generated proof receives a reward of 1 if the Lean 4 prover verifies it as correct, and 0 otherwise. This binary signal has the unique property of being perfectly accurate — there are no false positives or false negatives in the Lean kernel's verification. However, it is also extremely sparse: the model receives the same zero reward for a proof that fails at the last step as for a proof that fails at the first step, even though the former represents substantially more progress.

The authors explicitly acknowledge this sparsity as a challenge and address it through prompt selection (ensuring there are enough positive examples to provide a learning signal) rather than through reward shaping (which would require a learned reward model that might introduce inaccuracies, defeating the purpose of using formal verification).

GRPO algorithm. The paper employs Group Relative Policy Optimization (GRPO), which was introduced in DeepSeekMath (Shao et al., 2024) as an alternative to PPO (Schulman et al., 2017). The key advantage of GRPO is that it eliminates the need for a separate critic model — a neural network trained to predict the expected future reward from a given state, which is a standard but computationally expensive component of actor-critic RL algorithms.

GRPO works as follows. For each theorem prompt, the current policy model samples a group of candidate proofs (in this paper, the group size is 32). Each candidate is scored by the Lean prover, producing binary rewards. Rather than using the absolute reward values, GRPO computes the relative advantage of each candidate within its group — how much better or worse it is than the average candidate in the group. The policy is then updated to increase the probability of generating candidates that outperform the group mean and decrease the probability of those that underperform.

The optimization objective includes a KL divergence penalty that constrains the updated policy from deviating too far from the reference model (the SFT model used as initialization). This prevents catastrophic forgetting — where the policy radically changes its behavior to exploit the reward signal at the cost of losing general proof-generation capability. The KL penalty coefficient is set to 0.02.

$\text{Objective} = \mathbb{E}\left[\text{Advantage}(\text{candidate}) \cdot \log \pi_\theta(\text{candidate} \mid \text{prompt}) - \beta \cdot D_{KL}(\pi_\theta \parallel \pi_{\text{ref}})\right]$

where $\pi_\theta$ is the current policy, $\pi_{\text{ref}}$ is the reference (SFT) policy, $\beta = 0.02$ is the KL penalty coefficient, and the Advantage is computed as the standardized relative reward within the group of 32 candidates.

What this computes: for each group of 32 proof candidates generated for a theorem, the GRPO objective computes a policy gradient update that increases the log-probability of candidates that scored above the group average (positive advantage) and decreases the log-probability of candidates that scored below average (negative advantage), while simultaneously penalizing the KL divergence between the current policy and the SFT reference model to prevent the policy from drifting too far.

Why this form: the group-relative advantage normalizes the reward signal, which is essential when the raw rewards are binary and sparse — a candidate that scores 1 when the group average is 0.1 receives a much larger gradient update than a candidate that scores 1 when the group average is 0.9, reflecting the fact that the former provides more informative feedback. The KL penalty is important because formal theorem proving is a narrow domain with specific syntax; without it, the policy might over-optimize for the binary reward by generating proofs that exploit quirks of the verifier rather than learning general proving strategies, a phenomenon analogous to reward hacking in RLHF.

Training hyperparameters. RL training is conducted based on the SFT model, which serves as both the initial model and the reference model for the KL penalty. The learning rate is constant at $5 \times 10^{-6}$. For each theorem, 32 candidate proofs are sampled, with maximum length set to 2,048 tokens. The training batch size is 512 (presumably 512 ÷ 32 = 16 theorems per batch, though the paper does not explicitly state this). The authors note that this prompt selection strategy is designed to likely include both correct and incorrect proofs among the group of 32, which aligns with the group-relative nature of GRPO — if all candidates in a group were correct, the advantage would be zero for all, and no learning would occur.

Why RL improves fundamental capabilities. The paper makes an important observation in Section 2.4 (Figure 3): unlike in natural language mathematics (DeepSeekMath), where RL primarily improves pass@K by boosting the model's ability to select correct answers from a set of candidates, in formal theorem proving RL improves pass@1 as well as pass@K, and the improvement remains stable as the sample budget increases. The authors argue this represents a "genuine enhancement of fundamental capabilities" rather than just better candidate ranking.

Why might this be? In natural language math reasoning, RL typically uses a learned reward model that provides scalar scores for answer correctness. This reward model is imperfect, so RL can teach the model to exploit reward model biases without genuinely improving reasoning. The gains manifest primarily in better answer selection from a pool of candidates. In contrast, the Lean prover provides a binary reward that is perfectly accurate — there is no "reward hacking" possible because the verifier cannot be fooled. The only way to increase reward is to generate proofs that are actually correct. The RL process therefore forces the model to learn more robust proof-generation strategies that work consistently rather than occasionally, which manifests as improved pass@1 (the model is more likely to produce a correct proof on any single attempt).

Tactic-Level Tree Abstraction: The Truncate-and-Resume Mechanism

This mechanism is the bridge between whole-proof generation (efficient, one-shot) and tree search (interactive, feedback-driven). It defines how a single generated proof — a continuous string of text — is decomposed into nodes in a search tree, and how subsequent generations can resume from intermediate points in the tree.

Proof decomposition into tree nodes. The tree is constructed at the tactic level: each edge in the tree represents a single tactic application that transforms one tactic state to the next. The process begins when the model generates a complete proof. This entire proof is submitted to the Lean prover, which parses it into individual tactics and executes them sequentially. The Lean prover identifies the first tactic that causes a verification error (e.g., a type mismatch, a missing hypothesis, a tactic that doesn't apply to the current goal).

The proof is then truncated at this first error: all tactics after the error are discarded, and only the verified-successful prefix is retained. This prefix is segmented into individual tactic code blocks, each accompanied by its associated chain-of-thought comments (if in CoT mode). Each such block becomes an edge in the search tree, with the corresponding tactic state stored at the node it leads to.

The resulting structure is a path from the root node (the initial theorem statement with no tactics applied) through a sequence of nodes, each representing the tactic state after applying the corresponding tactic. The root node contains the file header (imports, options), the theorem statement, and the initial proof block opening. Each subsequent node adds one successful tactic to the prefix.

Multiple tactic codes per node. A crucial property of Lean 4's tactic language is that different sequences of tactics can lead to the same tactic state. For example, simp [h] and rw [h] might both transform a hypothesis h: a = b into the same substituted goal. The tree abstraction accounts for this by storing a set of equivalent tactic codes at each node — all the different code sequences that have been observed to lead to this particular tactic state. When the tree search agent later selects this node for expansion, it randomly samples one of these stored codes to use as the prompt, encouraging exploration of syntactically diverse approaches that achieve the same semantic result.

Resuming generation from a tree node. When the tree search policy selects a node for expansion, the system constructs a prompt from that node's stored information. The prompt consists of: (1) the file header and theorem statement (common to all nodes), (2) the sequence of successfully applied tactics from the root to the selected node, ending with the chosen tactic code from the node's stored set, and (3) a comment block containing the current tactic state, formatted as /- tactic state: ... -/, extracted from the Lean prover when that tactic was first applied.

This prompt is then fed to the language model, which has been trained (during SFT) to recognize and utilize the tactic state comment. The model generates a completion — a sequence of subsequent tactics — which is appended to the prefix and submitted to the Lean prover for verification. If the verification succeeds completely (no remaining goals), the search terminates with a correct proof. If verification fails, the truncation process repeats, and new nodes are added to the tree.

Why this abstraction matters. The tactic-level tree abstraction transforms the continuous problem of proof generation into a discrete search problem over tactic state transitions. Each node in the tree represents a semantically meaningful intermediate state (the actual goals and hypotheses at that point in the proof), not just a syntactic position in the text. This means the tree search is operating in a state space where progress can be measured and compared — two different proof attempts that reach the same tactic state have made equivalent progress, regardless of how many tactics each used. The stored set of tactic codes per node also enables the search to recognize and exploit equivalences, avoiding redundant exploration of multiple syntactic paths that converge to the same state.

Monte-Carlo Tree Search for Interactive Theorem Proving

The tree search algorithm adapts the standard MCTS paradigm (selection, expansion, simulation, backpropagation) to the whole-proof generation setting, with the truncate-and-resume mechanism serving as the expansion step.

Selection. The selection step traverses the tree from the root to identify a promising node for expansion, balancing exploration (trying under-visited parts of the tree) and exploitation (focusing on parts that have yielded progress in the past). The tree policy at each node $s$ selects the action $a$ — either moving to an existing child node or expanding the current node — that maximizes the value:

$TreePolicy(s) = \arg\max_{a \in Children(s) \cup \{\oslash\}} QUCB(s, a)$

where $Children(s)$ is the set of existing child nodes (each corresponding to a previously observed tactic application from state $s$), and $\oslash$ is a special "virtual node" token representing the action of expanding node $s$ itself.

The $QUCB(s, a)$ value for each action is composed of two terms:

$QUCB(s, a) = \underbrace{Q(s, a)}_{\text{Exploitation}} + \underbrace{UCB(s, a)}_{\text{Exploration}}$

where $Q(s, a)$ is the sample-based estimate of the action value (the average reward received when taking action $a$ from state $s$ in previous iterations), and $UCB(s, a)$ is the exploration bonus computed by upper confidence bounds, which decreases with the number of times the state-action pair $(s, a)$ has been selected.

What these equations compute: at each node, a score for each possible action (move to an existing child, or expand the current node) that combines the historical average reward from that action with a bonus that is larger for less-frequently-tried actions. The policy selects the highest-scoring action.

Why virtual nodes are necessary. In standard MCTS for games like Go or Chess, the action space is finite and known in advance (all legal moves from a given board state). In theorem proving, the action space is generated by a language model whose output scope cannot be predetermined — the model might generate one tactic, or five tactics, or a completely novel proof approach. The virtual node mechanism handles this open-ended action space by treating "expand this node" as an action that can be selected repeatedly, even though the node already has child nodes from previous expansions. This allows the tree search to continue exploring from non-leaf nodes, generating multiple alternative continuations from the same intermediate state.

Expansion. When the selection step nominates a node for expansion (either via the virtual node token or by selecting an existing child), the system invokes the proof generation model. The prompt is constructed from the node's incomplete proof prefix and the current tactic state (as described in Section 3.1). The model generates a completion, which is verified by the Lean prover.

There are three possible outcomes. First, if the verification succeeds completely — the proof has no remaining goals — the search procedure terminates, having found a correct proof. Second, if verification fails, the generated code is truncated at the first error, parsed into tactics (using the same decomposition procedure from Section 3.1), and each tactic becomes a new node added as a child beneath the expanded node. This creates a path of new nodes — not just a single new node — in a single expansion step. Third, the node might be a leaf that has been expanded multiple times; each expansion generates a potentially different set of tactics, creating additional child paths.

Why multi-node expansion per iteration. This design differs from conventional MCTS in competitive games, which typically expands only one node (one layer of children) per iteration. The multi-node expansion is a direct consequence of the whole-proof generation paradigm: the model generates multiple tactics at once, and the Lean prover can verify all of them up to the error point, so it is natural to add all of them to the tree simultaneously. This is more sample-efficient than generating one tactic per iteration because (a) it reduces the number of model invocations per tactic added to the tree, and (b) the model's completions benefit from the full context of the partial proof, which may help it generate more coherent tactic sequences than isolated single-tactic generation would.

Backpropagation. The final step updates value statistics along the selection trajectory — the path from the root to the expanded node. For each state-action pair $(s, a)$ on the trajectory, the accumulated reward statistics are updated with the reward received from the current expansion.

Let $\tau = \{(root, s^{(1)}), (s^{(1)}, s^{(2)}), (s^{(2)}, s^{(3)}), \ldots, (s^{(|\tau|-1)} = s_t, \oslash)\}$ denote the selection trajectory of the $t$-th iteration, which ends with the expanded node $s_t$. The reward $R(\tau)$ for this trajectory is assigned: 1 if the expansion produced a complete correct proof (extrinsic reward), 0 otherwise (extrinsic), plus potentially an intrinsic reward (defined in Section 3.3).

The updated Q-value for each state-action pair on the trajectory incorporates this reward, weighted by how recently it was received (via the discount mechanism, Section 3.3):

$Q(s, a) \leftarrow \frac{W_\gamma(s, a)}{N_\gamma(s, a)}$

where $W_\gamma$ is the discounted sum of rewards and $N_\gamma$ is the discounted count of visits (both defined precisely in Section 3.3, Equation 8 and Equation 9). This discounted averaging ensures that recent rewards — which reflect the current state of the search tree — influence the Q-values more than older rewards.

RMaxTS: Intrinsic Rewards and Discounted UCB

This is the core algorithmic contribution of the paper: a mechanism for driving exploration in proof search when extrinsic rewards are almost always zero.

The reward sparsity problem. In formal theorem proving, a proof attempt either succeeds (extrinsic reward = 1) or fails (extrinsic reward = 0). There is no partial credit. This means that in a standard MCTS implementation using only extrinsic rewards, the Q-values for all state-action pairs are zero except those that are on a path that eventually leads to a complete proof — and finding such a path is exactly the problem the search is trying to solve. The search faces a chicken-and-egg problem: it needs reward signals to guide exploration toward promising regions, but it cannot get reward signals until it has already found a proof.

The standard solution in MCTS is the UCB exploration bonus, which encourages visiting under-explored actions regardless of their Q-values. However, the authors demonstrate (Figure 5) that in theorem proving, the UCB bonus alone is insufficient — the search space is so large and the reward so sparse that pure exploration based on visit counts degenerates to essentially random sampling, performing no better than single-pass generation.

RMax intrinsic rewards. The RMax principle (Brafman and Tennenholtz, 2002), originally developed for tabular reinforcement learning with unknown transition dynamics, addresses exploration by awarding the agent a maximal reward whenever it reaches a previously unseen state. This "optimism in the face of uncertainty" encourages the agent to systematically explore the state space, visiting every reachable state at least once.

RMaxTS adapts this principle to Monte-Carlo tree search for theorem proving by defining the intrinsic reward as:

$R_{\text{intrinsic}}(\tau) = \mathbb{I}\left[\text{at least one new node is added to the search tree}\right]$

where $\tau$ is the most recent selection trajectory requiring a reward assignment for backpropagation, and $\mathbb{I}[\cdot]$ is the indicator function (1 if the condition is true, 0 otherwise).

What this computes: a binary reward that is 1 if the expansion step produced at least one tactic state that was not already present in the search tree (i.e., a new node was created), and 0 if all generated tactics led to already-existing nodes (i.e., the expansion redundantly explored known states).

Why this form: the design leverages a key property of the tactic state space: multiple different tactic sequences can lead to the same tactic state. The intrinsic reward does not reward merely generating syntactically different code; it rewards discovering semantically new states. A proof attempt that uses different tactics but arrives at the same set of remaining goals as a previous attempt receives no intrinsic reward, because it has not expanded the frontier of explored states. Conversely, a proof attempt that reaches a novel combination of goals and hypotheses — even if it doesn't solve the theorem — receives a reward for advancing the exploration frontier. This heuristics channels search effort toward diverse exploration of the proof state space rather than toward syntactic variations that converge to the same place.

The paper explicitly states that this intrinsic reward mechanism can "potentially reduce redundant generation and improve sample efficiency." This is because the search agent learns (through backpropagated intrinsic rewards) that certain nodes, when expanded, tend to produce novel states, while other nodes, when expanded, tend to produce states already in the tree. The Q-values augmented with intrinsic rewards will favor the former, systematically driving the search toward unexplored regions.

The non-stationarity problem with intrinsic rewards. A critical complication is that intrinsic rewards are inherently non-stationary: as the search tree grows and more of the reachable state space is discovered, the probability that a new expansion produces a novel state decreases. Early in the search, almost every expansion produces new nodes and receives an intrinsic reward of 1. Late in the search, most expansions redundantly visit already-discovered states and receive 0. The expected value of expanding any given node therefore changes over time as a function of how thoroughly the surrounding region has been explored, not just as a function of the node's properties.

Standard UCB1 (Auer et al., 2002) assumes stationary reward distributions and weights all historical observations equally:

$Q_{UCB1}(s, a) = \frac{W(s, a)}{N(s, a)} + \sqrt{\frac{2 \ln \sum_{a'} N(s, a')}{N(s, a)}}$

where:

$W(s, a) = \sum_{\tau \in \Gamma(s,a)} R(\tau)$

$N(s, a) = |\Gamma(s, a)|$

where $\Gamma(s, a) = \{\tau \mid (s, a) \in \tau\}$ is the list of all tree-policy trajectories containing $(s, a)$ as an intermediate selection step, ordered so that newer trajectories have larger indices.

Why UCB1 fails with intrinsic rewards. In the stationary setting, averaging all historical rewards equally produces an unbiased estimate of the true expected reward. But when rewards are non-stationary — when the same action that yielded reward 1 in iteration 10 now yields reward 0 in iteration 100 because the easy-to-reach novel states have been exhausted — UCB1's equal weighting causes the exploitation term $\frac{W(s,a)}{N(s,a)}$ to be dominated by stale data. An action that was highly rewarding early in the search will retain a high Q-value even after it ceases to produce novel states, misleading the selection policy into repeatedly expanding nodes that are no longer productive.

Discounted UCB (DUCB). To handle non-stationarity, the paper adopts discounted upper confidence bounds (Garivier and Moulines, 2011), which applies a discount factor $\gamma \in (0, 1)$ to smoothly down-weight older feedback:

$Q_{DUCB}(s, a) = \frac{W_\gamma(s, a)}{N_\gamma(s, a)} + \sqrt{\frac{2 \ln \sum_{a'} N_\gamma(s, a')}{N_\gamma(s, a)}}$

where:

$W_\gamma(s, a) = \sum_{t=1}^{N(s,a)} \gamma^{N(s,a) - t} R(\tau_t)$

$N_\gamma(s, a) = \sum_{t=0}^{N(s,a)-1} \gamma^t$

where $N(s,a)$ is the total number of times action $a$ has been selected from state $s$, and $\tau_t$ is the $t$-th trajectory containing $(s, a)$, indexed so that $t=1$ is the oldest and $t=N(s,a)$ is the newest. In practice, $\gamma = 0.99$.

What $W_\gamma(s,a)$ computes: the discounted cumulative reward, where each reward $R(\tau_t)$ is weighted by $\gamma^{N(s,a)-t}$. The most recent reward ($t = N(s,a)$) receives weight $\gamma^0 = 1$, the second-most-recent receives weight $\gamma^1 = 0.99$, the third-most-recent receives weight $\gamma^2 = 0.98$, and so on. Rewards from the distant past are exponentially down-weighted. This ensures that the Q-value tracks the recent performance of the action rather than being anchored to its initial performance when the state space was mostly unexplored.

What $N_\gamma(s,a)$ computes: the discounted visit count, which serves as the effective sample size for the exploitation term. With $\gamma = 0.99$ and many visits, $N_\gamma(s,a)$ converges to approximately $\frac{1}{1-\gamma} = 100$, meaning that only the most recent ~100 visits meaningfully contribute to the Q-value estimate. Older visits are effectively forgotten.

Why discounted UCB works with RMax. The combination of RMax intrinsic rewards and DUCB creates a dynamic where early in the search, when most expansions discover new states, the Q-values of all actions are high (because intrinsic rewards are high), and selection is driven primarily by the UCB exploration bonus (which favors less-visited actions). As the search tree grows and intrinsic rewards become sparser, the DUCB exploitation term for actions that continue to discover novel states remains high (because recent rewards are weighted more), while the exploitation term for actions that have stopped discovering novel states declines (because recent rewards of 0 dominate the discounted average). This causes the search to naturally shift from broad exploration (trying everything) to focused exploitation (expanding nodes that are still yielding novel states).

The paper's ablation (Figure 5) confirms this: RMaxTS with standard UCB1 (no discounting) performs comparably to UCT without intrinsic rewards, because the stale high rewards from early exploration prevent the policy from adapting to the changing reward landscape. RMaxTS with DUCB substantially outperforms both, demonstrating that the discount mechanism is not a minor refinement but a crucial complement to intrinsic-reward-driven exploration.

Why set the total reward to intrinsic only. In the paper's implementation, the total reward for backpropagation is $R(\tau) = R_{\text{intrinsic}}(\tau)$ — the extrinsic reward (1 for solved, 0 otherwise) is not used during search. The authors note this matches the ZeroRMax paradigm (Jin et al., 2020), where exploration is driven purely by intrinsic rewards. The extrinsic reward of 1 for a completed proof is used only to terminate the search; it is not backpropagated to update Q-values. This design choice reflects the extreme sparsity of extrinsic rewards: since almost no trajectories receive positive extrinsic rewards, including them would contribute negligible signal while adding implementation complexity. The intrinsic reward alone provides sufficient gradient for exploration.

Parallelization of Monte-Carlo Tree Search

Tree search with large language models presents unique parallelization challenges: each expansion requires invoking a 7B-parameter model on GPU and then verifying the output with the Lean prover on CPU, creating a heterogeneous workload with different bottlenecks.

Root parallelization. The system deploys 256 independent MCTS runners, each operating on a separate search tree (or separate copies of the same tree). One language model is allocated per GPU (details of GPU configuration are not specified), with a batch size of 512 for proof generation. The Lean prover is invoked through REPL and executed on a cluster with "thousands of CPU cores" — each proof verification task is handled by an individual process, created and terminated in a sandbox environment. Both language model inference and proof verification are handled asynchronously, meaning that MCTS runners do not block waiting for each other; they issue requests and continue processing when results return.

Tree parallelization. Each individual search tree is managed by 32 thread workers that parallelize the tree iteration steps. Each thread worker independently performs the full MCTS loop: it executes the selection step (traversing the tree using the current Q-values and UCB bonuses), identifies a node for expansion, invokes the language model to generate a proof completion, submits the generated code for Lean verification, and performs backpropagation to update Q-values along the selection path.

The challenge with multiple thread workers operating on the same tree is that they might select the same or similar nodes for expansion, reducing the diversity of exploration. To mitigate this, the paper employs a technique called virtual loss.

Virtual loss. When a thread worker selects a node for expansion, it immediately backpropagates a temporary reward of $R(\tau) = 0$ along the selection trajectory, updating the Q-values as if the expansion had already completed and yielded a reward of 0. This temporarily decreases the Q-values of the selected path, making it less attractive to other thread workers (who see the updated, lower Q-values). When the actual expansion completes and the true reward is known (1 if a new node was discovered, 0 otherwise), the temporary update is replaced with the true reward. This "optimistic locking" mechanism encourages different thread workers to explore different regions of the tree simultaneously, improving the diversity of parallel exploration.

The paper describes this as promoting "exploration of different nodes for expansion, thereby enhancing the overall search efficiency." Without virtual loss, all 32 thread workers might converge on the same high-UCB-value path, generating redundant expansions that all start from the same intermediate state and produce similar completions. With virtual loss, once one worker commits to a path, other workers are nudged toward alternative paths, increasing the breadth of the search.

Overall system scale. For the largest-scale experiments ($16 \times 6400$ or $32 \times 6400$ sample budgets), the system runs 16 or 32 independent MCTS attempts, each consuming up to 6,400 model generations. With 256 runners, 32 thread workers per tree, and thousands of CPU cores for verification, this represents a substantial computational infrastructure, though the paper does not report total wall-clock time or FLOP counts for these experiments.

4. Key Insights and Innovations

Innovation 1: The Truncate-and-Resume Mechanism as a Unifying Abstraction Between Two Opposing Paradigms

The field of neural theorem proving has been split between two approaches that each capture a valuable property while sacrificing the other. Whole-proof generation (DSP, LEGO-Prover, DeepSeek-Prover-V1) captures computational efficiency — one round-trip between the model and the prover per proof attempt, enabling massive sampling budgets — but lacks access to intermediate tactic states, forcing the model to maintain an implicit internal representation that can silently drift, producing compounding errors over long proofs. Proof-step generation (GPT-f, ReProver, Hypertree Proof Search, InternLM2-StepProver) captures intermediate feedback — the model sees ground-truth tactic states after every step — but at the cost of dozens of model-prover round-trips per proof, creating a communication bottleneck that limits total search budget.

Prior work treated this as an either-or choice: you picked one paradigm and accepted its limitations. The paper's truncate-and-resume mechanism (Section 3.1) is intellectually distinctive not merely as a hybrid — hybrid systems are common — but because it reframes the relationship between the two paradigms from alternative architectures to two views of the same process. The key move is recognizing that a whole-proof generation can be post-hoc decomposed into individual proof steps by leveraging the proof assistant's error-reporting capability: generate the whole proof, submit it to Lean, and the location of the first verification error tells you exactly where the successful prefix ends and where the state should be extracted. This converts the proof assistant from a final-answer grader into a state-space annotator — it not only says "wrong" but also says "this prefix was right, and here is the exact tactic state at the point of failure."

The unification goes deeper than the truncation mechanism itself. The paper shows that a single model, trained with a unified objective (predicting both proof code and tactic states during SFT), can serve both deployment modes. In single-pass mode, it generates whole proofs and receives no intermediate feedback (computationally cheap, good for easy problems). In tree search mode, the same model receives tactic state comments as input and generates continuations from intermediate states (feedback-rich, good for hard problems). The model doesn't need to know which mode it's in — the presence or absence of tactic state comments in the prompt switches its behavior naturally, because it was trained on both formats.

This is a fundamental conceptual advance rather than an incremental improvement because it changes what "a theorem prover" means architecturally. Rather than building separate systems for efficient sampling and interactive proving, one model trained with a carefully designed data format can do both, and the choice of which to use becomes a deployment-time decision based on the problem's difficulty and the available compute budget. The evidence for this unification's effectiveness is in Table 3: the same DeepSeek-Prover-V1.5-RL model achieves 60.2% in single-pass generation (16 × 6400 budget) and 63.5% with tree search (32 × 6400 mixture strategy), demonstrating that the model genuinely supports both modes without architectural modification.

---

Innovation 2: Intrinsic Rewards as a First-Class Solution to the Sparse-Reward Exploration Problem in Proof Search

Prior work on tree search for theorem proving — most notably Hypertree Proof Search (Lample et al., 2022) — applied standard MCTS with UCT (Kocsis and Szepesvári, 2006) directly, relying on the UCB exploration bonus to drive search in the absence of dense reward signals. The implicit assumption was that the UCB bonus's count-based exploration (preferring less-visited actions) would be sufficient to navigate the proof tree. This assumption turns out to be false in practice, and the paper's diagnostic contribution is to show exactly why and provide a principled alternative.

The core diagnostic insight is that the proof search problem matches what the theoretical RL literature calls a hard-exploration regime (Krishnamurthy et al., 2016): the search tree has an exponentially branching structure where almost all leaves yield zero extrinsic reward, and there is no gradient of partial progress to follow. In such regimes, count-based exploration (UCB without reward signal) reduces to essentially uniform random search — every action has Q-value zero, so selection is determined entirely by visit counts, which means "try everything equally." On a search tree with millions or billions of possible paths, this is indistinguishable from the single-pass generation baseline.

The paper's RMaxTS (Section 3.3) replaces this implicit assumption with an explicit exploration reward function derived from the RMax principle (Brafman and Tennenholtz, 2002): the agent receives a reward of 1 whenever it adds a previously unseen node to the search tree, and 0 otherwise. This is not merely "adding a bonus for novelty" — it restructures the entire credit assignment problem. In standard MCTS, the agent receives no feedback for partial progress. In RMaxTS, every expansion that discovers a new tactic state generates a positive reward that is backpropagated up the selection trajectory, creating a dense reward gradient that guides the tree policy toward actions that have historically led to novel states.

The subtlety that makes this more than a generic exploration bonus is the semantic interpretation of novelty. Because the tree abstraction (Section 3.1) maps multiple tactic sequences to the same node when they lead to the same tactic state, the intrinsic reward rewards discovering semantically distinct states, not syntactically different code. An expansion that generates different tactic text but arrives at the same set of remaining goals receives no reward. This channels exploration toward genuinely distinct proof approaches — different ways of decomposing the problem — rather than toward superficial variations. It implicitly encodes the insight that in formal theorem proving, progress is measured by goal reduction (transforming the current goals into simpler subgoals), not by code generation (producing tactic sequences).

The ablation study in Figure 5 makes the diagnostic case empirically: UCT without intrinsic rewards ("without R_intrinsic") achieves pass rates essentially identical to single-pass generation (column comparison: 61.1% at 16 × 6400 for UCT without intrinsic vs. 60.2% for single-pass), confirming that standard MCTS provides no benefit over blind sampling in this sparse-reward domain. RMaxTS with DUCB achieves 62.7% at the same budget, demonstrating that intrinsic rewards are not a minor enhancement but the mechanism that makes tree search work at all.

---

Innovation 3: Recognizing and Addressing Non-Stationarity as the Missing Piece for Intrinsic-Reward MCTS

Even with intrinsic rewards defined, a subtler problem arises that the paper diagnoses and solves: intrinsic rewards for discovering novel states are inherently non-stationary. Early in search, when the tree is small, almost every expansion discovers a new node and receives a reward of 1. Late in search, when most reachable states have been discovered, most expansions receive 0. The expected value of expanding any given node changes over time as a function of how thoroughly the surrounding region has been explored — not as a function of the node's inherent properties.

Standard UCB1 (Auer et al., 2002), used in virtually all prior MCTS applications to theorem proving, assumes stationary reward distributions and weights all historical observations equally when computing the exploitation term $Q(s,a) = W(s,a) / N(s,a)$. Under non-stationary rewards, this creates a staleness problem: an action that was highly rewarding during early exploration retains a high Q-value indefinitely, because those early rewards dominate the equally-weighted average. The UCB exploration bonus eventually counteracts this (as the action's visit count grows, the bonus shrinks), but only after the action has been selected many times — wasting samples on a now-unproductive node.

The paper's diagnostic move is recognizing this as an instance of the switching bandit problem studied in the theoretical bandit literature (Garivier and Moulines, 2011), and importing the solution: discounted UCB (DUCB), which applies a discount factor $\gamma = 0.99$ to historical rewards so that recent observations have proportionally greater weight. This means:

$W_\gamma(s,a) = \sum_{t=1}^{N} \gamma^{N-t} R(\tau_t)$

rather than the equally-weighted sum $W(s,a)$ used in UCB1.

The discount factor fundamentally changes the dynamics of value propagation. With DUCB, the effective memory of the Q-value is approximately $1/(1-\gamma) = 100$ visits. After ~100 visits, early observations are effectively forgotten, and the Q-value tracks only recent performance. If an action stops producing novel states (because its region of the state space is exhausted), its Q-value declines within roughly 100 iterations, causing the selection policy to naturally redirect exploration elsewhere — without needing to wait for the UCB bonus to decay slowly through visit counts.

The ablation in Figure 5 confirms that this is not a minor tuning detail. RMaxTS with UCB1 (standard, undiscounted) achieves 60.7% at 16 × 6400 — barely above the no-intrinsic-reward baseline (61.1%) and the single-pass baseline (60.2%), and substantially below RMaxTS with DUCB (62.7%). The interpretation is clear: intrinsic rewards without discounting fail because the value estimates are dominated by stale data from early exploration. The discount mechanism is essential for making intrinsic rewards usable as a guidance signal throughout the full search process.

This is a fundamental contribution to the MCTS literature applied to generative models, not just to theorem proving. It identifies a structural property of intrinsic-reward-driven search (non-stationarity from diminishing discovery probability) that is likely to arise in any domain where exploration systematically exhausts the reachable state space, and provides a principled solution with theoretical grounding in the bandit literature.

---

Innovation 4: Reinforcement Learning as Genuine Capability Improvement, Not Just Better Candidate Selection

A prominent finding from prior work on RL for mathematical reasoning — specifically DeepSeekMath (Shao et al., 2024) — was that RL primarily improves pass@K (the probability that at least one of K attempts is correct) rather than pass@1 (the probability that any single attempt is correct). The interpretation was that RL teaches the model to generate a more diverse set of candidates, increasing the chance that one of them is correct, but does not necessarily improve the model's fundamental reasoning capability — it becomes better at covering the space of possible answers, not better at producing the right answer on any given try.

DeepSeek-Prover-V1.5 presents a contrasting finding that changes how we should think about RL's role in formal domains. Figure 3 (Section 2.4) shows that RLPAF improves not only pass@128 (from 50.4% to 51.6% in CoT mode on miniF2F-test) but also improves across the entire range of K — the pass@K curves in the left panel are shifted upward uniformly, not just at the right tail. Moreover, the improvement persists and even amplifies at larger sample budgets in tree search: Table 3 shows that DeepSeek-Prover-V1.5-RL+RMaxTS achieves 62.7% vs. DeepSeek-Prover-V1.5-SFT+RMaxTS at 59.0% (both at 16 × 6400), a 3.7 percentage-point gap that is wider than the single-pass gap at the same budget (60.2% vs. 57.4%, a 2.8 percentage-point gap).

The intellectual significance of this finding is that it identifies a property of the reward signal — not the RL algorithm — as the key factor determining whether RL improves fundamental capability. In natural language math reasoning, the reward model is an imperfect learned function that can be exploited (the model learns to produce outputs that score highly under the reward model without being genuinely correct). In formal theorem proving, the Lean prover provides a perfectly accurate binary oracle — there is no way to "hack" the reward because the verifier cannot be fooled. The only way to increase the probability of receiving reward is to generate proofs that are actually correct according to the formal system's rules.

This reframes the RL-for-reasoning question from "does RL help?" to "under what conditions does RL help, and what type of improvement does it produce?" When the reward signal is noisy and approximate (learned reward models), RL primarily improves diversity and coverage (pass@K gains). When the reward signal is noiseless and exact (formal verification), RL improves the policy itself (pass@1 gains), because the only gradient available is toward genuine correctness. This is a valuable diagnostic distinction for future work: if you want RL to improve fundamental capability, invest in making your reward signal more accurate; if you only need better candidate coverage, approximate rewards may suffice.

The paper also shows that this capability improvement from RL is orthogonal to the gains from tree search — they compound rather than overlap. RMaxTS provides roughly +2–3 percentage points over single-pass generation regardless of whether the underlying model is SFT or RL, and RL provides roughly +2–4 percentage points regardless of whether deployment uses single-pass or tree search. This suggests that RL and tree search improve different aspects of the system: RL improves the quality of proposals (the model generates better proofs on each attempt), while tree search improves the efficiency of exploration (the system finds correct proofs with fewer total attempts by systematically covering the state space). The combination of both produces gains that neither achieves alone.

5. Experimental Analysis

Evaluation Methodology

• Dataset. The paper evaluates on two formal theorem proving benchmarks: miniF2F (Zheng et al., 2022), consisting of 244 validation and 244 test problems covering high-school level exercises and competitions (AMC, AIME, IMO) with emphasis on algebra and number theory, manually converted from Lean 3 to Lean 4.9.0 based on the version provided by Yang (2023); and ProofNet (Azerbayev et al., 2023), consisting of 185 validation and 186 test problems at the undergraduate level drawn from standard textbooks in real and complex analysis, linear algebra, abstract algebra, and topology, also manually converted from Lean 3 to Lean 4.9.0.

• Base model(s). All models are based on the DeepSeekMath-Base 7B architecture (Shao et al., 2024), further pre-trained on formal mathematical languages including Lean, Isabelle, and Metamath to produce DeepSeek-Prover-V1.5-Base. The model has 7 billion parameters. The paper uses this scale because it is "representative of the capabilities of many contemporary LLMs" and sits in a regime where test-time compute (through both RL and tree search) can produce measurable improvements — not at ceiling performance but with non-trivial baseline capability (29.7% on miniF2F-test with 3-shot prompting for the base model).

• Metrics. The primary metric is pass@K accuracy, which measures the probability that at least one correct proof is generated within K attempts. For single-pass sampling, K equals the total number of whole-proof generations. For best-first-search methods, $K = N \times S \times T$ where $N$ is the number of search attempts, $S$ is the number of tactics generated per expansion, and $T$ is the number of expansion iterations. For tree search methods (RMaxTS and Hypertree Proof Search), $K = N \times T$ where $N$ is the number of independent tree search attempts and $T$ is the number of model generations invoked in tree expansions. The generated proofs are verified using the Lean 4 theorem prover with Mathlib4 and Aesop imported, subject to a 300-second time limit per verification. Each model is deployed on a single A100-40G GPU using the vLLM framework (Kwon et al., 2023) with sampling parameters: temperature 1, top-p 0.95, maximum 2,048 tokens.

• Baselines. The paper compares against a wide range of prior work spanning both paradigms. For single-pass whole-proof generation: TheoremLlama (Wang et al., 2024) at 33.6% on miniF2F-test, and DeepSeek-Prover-V1 (Xin et al., 2024) at 50.0% (16 × 4096 budget). For tree search and proof-step generation methods: COPRA with GPT-4 (Thakur et al., 2023) at 26.6% (1 × 60 budget), Llemma-7B and Llemma-34B (Azerbayev et al., 2024) at 26.2% and 25.8% respectively (1 × 32 × 100 budget), ReProver (Yang et al., 2023) at 26.5%, LLMStep (Welleck and Saha, 2023) at 27.9% (1 × 32 × 100), GPT-f (Polu et al., 2022) at 36.6% (64 × 8 × 512), Hypertree Proof Search (Lample et al., 2022) at 41.0% (64 × 5000), Lean-STaR (Lin et al., 2024) at 46.3% (64 × 1 × 50), InternLM2-Math-7B (Ying et al., 2024) at 30.3% (1 × 32 × 100), InternLM2-Math-Plus-7B at 43.4% (1 × 32 × 100), and InternLM2-StepProver (Wu et al., 2024) at 54.5% (64 × 32 × 100). On ProofNet, the key baselines are ReProver at 13.8% and InternLM2-StepProver at 18.1%.

• Generation budget / compute accounting. The paper normalizes across paradigms by defining sample budget K as described above, factoring total model invocations to enable comparison between single-shot and search-based methods. For single-pass methods, the budget is simply the number of proof texts generated (e.g., 16 × 6400 means 16 groups of 6,400 independent generations). For tree search, budget equals the number of search attempts multiplied by model generations per attempt (e.g., 16 × 6400 means 16 independent tree searches, each consuming 6,400 model invocations). However, the paper does not account for the additional computation from parallel Lean verification processes, the cost of tactic state extraction, or the CPU resources for tree management — the budget reflects only language model inference cost.

• Cross-validation / statistical protocol. No cross-validation is used for the main benchmark evaluations — results are reported directly on the fixed test sets. Standard deviations are reported for some evaluations using the ± notation (e.g., "51.6% ± 0.5%"), but the paper does not specify the number of evaluation runs or the source of variance (across different random seeds, different sampling runs, or different model checkpoints). For the supervised fine-tuning data construction, an expert iteration loop is used where the model generates proofs, verified proofs are added to the training set, and the model is retrained, but the validation set of ProofNet is explicitly noted (Table 2) as being used in this iteration process, meaning ProofNet results may not represent held-out generalization for that benchmark. For difficulty analysis, no explicit cross-validation over difficulty strata is reported — the difficulty-dependent effects are discussed qualitatively (Section 4.3, Figure 5) rather than through a formal stratification protocol.

Main Quantitative Results

Single-Pass Whole-Proof Generation Results

The headline finding for single-pass generation is that DeepSeek-Prover-V1.5-RL achieves 60.2% on miniF2F-test with 16 × 6400 total proof attempts (Table 1), representing a 10.2 percentage-point absolute improvement over DeepSeek-Prover-V1's 50.0% at a comparable budget (16 × 4096). This result establishes a new state-of-the-art for whole-proof generation methods, substantially exceeding TheoremLlama (33.6%) and the previous best whole-proof approach.

At more modest budgets: at 128 attempts, DeepSeek-Prover-V1.5-RL achieves 51.6% ± 0.5% (CoT mode), which already surpasses DeepSeek-Prover-V1's 46.1% ± 0.5% and is competitive with the leading tree search method InternLM2-StepProver (54.5% at 64 × 32 × 100 — a budget that is difficult to directly equate but represents substantially more total model invocations). This demonstrates that the improvements from SFT and RL are not merely a function of massive sampling — the model is genuinely better at generating correct proofs even with limited attempts.

At 3200 attempts (a single run), DeepSeek-Prover-V1.5-RL achieves 54.9% ± 0.7%, surpassing InternLM2-StepProver's 54.5% (which required 64 × 32 × 100 = 204,800 total tactic generations), representing a dramatic sample efficiency advantage — the total model invocations differ by roughly two orders of magnitude depending on how one equates whole-proof generations to tactic-level generations.

On ProofNet (Table 2), DeepSeek-Prover-V1.5-RL achieves 23.7% on the test set at 4 × 6400, compared to InternLM2-StepProver's 18.1% and ReProver's 13.8%. At 128 attempts, the model achieves 18.2% ± 0.5% (CoT mode), demonstrating strong few-attempt performance. At 3200 attempts (single run), it achieves 22.0% ± 0.5% on the test set. The performance on ProofNet is notably lower than on miniF2F, reflecting the greater difficulty of the undergraduate-level problems.

Training stage progression (Figure 3) shows monotonic improvements at each stage. The base model (3-shot) achieves 29.7% ± 0.5% pass@128 on miniF2F-test. SFT (CoT mode) moves this to 50.4% ± 0.4% — a 1.7× improvement. RL (CoT mode) further improves to 51.6% ± 0.5%. On ProofNet-test, the progression is: base 9.7% ± 0.7%, SFT 15.9% ± 0.6%, RL 18.2% ± 0.5%. The pass@K curves (left panels) show that the gap between SFT and RL is consistent across K values (from K=1 to K=128), with RL curves shifted upward at all points rather than only at the right tail — the paper's key evidence that RL improves fundamental capability rather than just candidate diversity.

CoT vs. non-CoT comparison (Figure 3 and Table 3): CoT mode consistently outperforms non-CoT mode. At 128 attempts on miniF2F-test, RL-CoT achieves 51.6% ± 0.5% vs. RL-non-CoT at 50.5% ± 0.6%. At large budgets (16 × 6400), the gap widens: RL-CoT at 60.2% vs. RL-non-CoT at 57.4% (Table 3). On ProofNet-test at pass@128: RL-CoT at 18.2% ± 0.5% vs. RL-non-CoT at 17.5% ± 0.5%. The paper interprets this as evidence that chain-of-thought reasoning "diversifies the planning pathways of theorem proving," and the widening gap at larger budgets suggests that CoT enables the model to explore solution strategies that are not merely more effective but are different in kind from non-CoT strategies — they open up reasoning approaches that non-CoT mode cannot access at all.

Mixture strategy results (Table 3): Allocating half the sample budget to CoT mode and half to non-CoT mode yields performance that exceeds either mode alone. At 16 × 6400 total budget in single-pass generation (8 × 6400 CoT + 8 × 6400 non-CoT), the mixture achieves 60.7% for RL, compared to 60.2% (CoT only) and 57.4% (non-CoT only). In tree search with RMaxTS, the mixture at 32 × 6400 achieves 63.5% — the paper's overall best result. This complementarity is attributed to different problem-solving strengths: CoT mode excels at problems requiring "systematic and proactive mathematical thinking," while non-CoT mode efficiently handles problems solvable through Lean's built-in automation tactics (exemplified in the induction and IMO problems in Appendix B). The mixture strategy captures both strengths without requiring the system to know in advance which mode suits each problem.

Tree Search Results (RMaxTS)

The headline finding is that DeepSeek-Prover-V1.5-RL + RMaxTS achieves 63.5% on miniF2F-test with 32 × 6400 total generation budget using the mixture strategy (Table 1, Table 3). This represents the new state-of-the-art, exceeding the previous best (InternLM2-StepProver at 54.5%, which uses 64 × 32 × 100 budget — a different computational currency). Even at more modest tree search budgets: 1 × 3200 achieves 55.0% ± 0.7%, 4 × 6400 achieves 59.6% ± 0.6%, and 16 × 6400 achieves 62.7%.

The tree search gain over single-pass generation is visible by comparing corresponding rows in Table 3. At 16 × 6400 budget in CoT mode: RMaxTS achieves 62.7% vs. single-pass at 60.2% — a +2.5 percentage-point gain. At 4 × 6400: RMaxTS at 59.6% ± 0.6% vs. single-pass at 58.4% ± 0.5% — a +1.2 percentage-point gain. The tree search advantage is modest but consistent, and it compounds with both RL (RL + RMaxTS outperforms SFT + RMaxTS) and with the mixture strategy. This supports the paper's claim that tree search and RL are orthogonal improvements: RL improves the proposal quality (each generation is more likely to be correct), while tree search improves the efficiency of using those generations (systematic exploration finds correct proofs that random sampling might miss).

On ProofNet (Table 2), RMaxTS results are more striking: DeepSeek-Prover-V1.5-RL + RMaxTS achieves 25.3% at 4 × 6400, compared to 23.7% in single-pass generation at the same budget — a +1.6 percentage-point gain. The tree search also achieves 25.4% on the validation set, and 21.5% ± 0.8% on the test set with only 1 × 3200 budget (a single tree search run).

An important sample efficiency observation: DeepSeek-Prover-V1.5-RL with single-pass generation at 3200 attempts achieves 54.9% (Table 1), which already surpasses InternLM2-StepProver's 54.5% (which uses 64 × 32 × 100 = 204,800 tactic generations in best-first-search). However, this comparison requires caution: whole-proof generation and tactic-level generation consume different amounts of computation per "attempt." A single whole-proof generation of 2,048 tokens involves roughly 7B × 2,048 × 2 ≈ 2.9 × 10¹³ FLOPs (using the standard 2ND formula), while 100 tactic generations of average length 50 tokens each involves 7B × 50 × 100 × 2 ≈ 7.0 × 10¹³ FLOPs — on the same order of magnitude but with additional overhead from 100 round-trips to the Lean prover.

Large-Scale Ablation: Training Strategies Under Heavy Sampling

Table 3 presents a comprehensive matrix comparing SFT vs. RL, non-CoT vs. CoT, and single-pass vs. RMaxTS, all at large sample budgets (4 × 6400 and 16 × 6400). The primary takeaway is that every design choice contributes additively: RL improves over SFT by +2–4 percentage points across all settings; CoT improves over non-CoT by +1–3 percentage points; RMaxTS improves over single-pass by +1–3 percentage points; the mixture strategy adds another +1–2 percentage points. These improvements are remarkably consistent and largely independent — there is no evidence of diminishing returns or negative interactions between them.

Specific numbers for RL vs. SFT (Table 3): In CoT single-pass at 16 × 6400, RL (60.2%) exceeds SFT (57.4%) by +2.8 points. In CoT RMaxTS at 16 × 6400, RL (62.7%) exceeds SFT (59.0%) by +3.7 points. In non-CoT single-pass, RL (57.4%) exceeds SFT (56.1%) by +1.3 points. In the mixture strategy, RL consistently outperforms SFT. The fact that the RL advantage is larger in tree search (+3.7) than in single-pass (+2.8) at the same budget reinforces the paper's claim that RL and tree search are synergistic — the improved proposal quality from RL gives the tree search better material to work with.

Ablation Studies and Robustness Checks

Intrinsic rewards (R_intrinsic): removal causes tree search to collapse to single-pass performance. Figure 5 (left panel) shows the pass@K curves within a 6,400-generation budget. The "UCT (without R_intrinsic)" curve — standard MCTS with only UCB exploration bonus and no intrinsic rewards — tracks essentially identically to "w/o Tree Search" (single-pass generation), reaching approximately 57% at 6,400 samples vs. RMaxTS at approximately 58.5%. The right panel confirms: at 16 × 6400 budget, UCT without R_intrinsic achieves 61.1%, which is within 0.9 percentage points of single-pass generation at 60.2%, while RMaxTS achieves 62.7%. This is the paper's most important ablation: intrinsic rewards are not an enhancement but a necessary condition for tree search to provide any benefit over blind sampling. The interpretation is that in sparse-reward domains where almost all paths yield zero extrinsic reward, the UCB bonus alone (which is purely count-based) reduces to uniform random exploration, making the tree structure irrelevant — you get the same result as generating the same number of independent samples.

Discounted UCB (DUCB): replacement with standard UCB1 causes substantial degradation. Figure 5 also shows the "RMaxTS (DUCB → UCB1)" variant, which uses intrinsic rewards but with standard undiscounted UCB1 instead of DUCB. At 16 × 6400, this variant achieves 60.7% — essentially identical to the no-intrinsic-reward baseline (61.1%) and far below RMaxTS with DUCB (62.7%). The paper's explanation is that UCB1's equal weighting of all historical rewards causes the Q-values to be dominated by stale data from early exploration, when almost every expansion discovered new nodes and received intrinsic rewards of 1. These inflated Q-values persist throughout the search, preventing the policy from adapting to the reality that later expansions mostly produce redundant states. This is a critical diagnostic insight: intrinsic rewards without a mechanism to handle non-stationarity are actively harmful (or at best neutral), because they lock the exploration policy into a "remember when this was productive" regime.

Tactic state information removal: search benefit largely disappears. The "RMaxTS (without tactic state)" variant in Figure 5 removes the tactic state comment from the prompt when expanding a node — the model generates continuations from the raw incomplete code alone, without intermediate compiler feedback. At 16 × 6400, this variant achieves 61.1%, matching the no-intrinsic-reward baseline and substantially below full RMaxTS at 62.7%. At lower budgets (the left panel), the gap is smaller but still present. This confirms that the tactic state information is not merely a helpful feature but an essential component of the tree search's effectiveness. The reason is that without access to the ground-truth intermediate state, the model suffers from the same compounding error problem as whole-proof generation — it generates continuations based on an implicit state estimate that may have drifted from reality. The tactic state comment corrects this drift at each expansion point, aligning the model's context with the actual proof state.

Both prompting modes (CoT and non-CoT): complementary strengths justify mixture strategy. Appendix B provides qualitative examples of problems where CoT outperforms non-CoT (mathd_algebra_459, numbertheory_x5neqy2p4, amc12_2000_p12 — problems requiring systematic mathematical reasoning about algebraic identities, modular arithmetic cases, and optimization over integer possibilities) and where non-CoT outperforms CoT (induction_pord1p1on2powklt5on2, imo_1960_p2 — problems solvable through efficient Lean automation tactics like nlinarith, omega, and field_simp). This pattern is not formally quantified by difficulty level but provides a qualitative account of why the mixture strategy works: some problems benefit from explicit step-by-step mathematical planning (CoT), while others are more efficiently solved by letting Lean's tactic automation handle the reasoning (non-CoT). The mixture captures both without requiring per-problem mode selection.

Expert iteration data augmentation: no explicit ablation. The paper describes using expert iteration during SFT data construction, but does not present results with and without this iteration to quantify its contribution. The contribution of the thought-augmented annotation by DeepSeek-Coder V2 236B is similarly not isolated through an ablation — we cannot determine from the reported results how much of the SFT improvement comes from data quantity, data quality, or the chain-of-thought annotation specifically.

Critical Assessment

The paper's central claims and the evidence supporting or qualifying each:

---

Claim 1: "DeepSeek-Prover-V1.5 achieves new state-of-the-art results on miniF2F (63.5%) and ProofNet (25.3%)."

This claim is clearly supported by the benchmark comparisons in Tables 1 and 2. On miniF2F-test, the 63.5% result with RMaxTS and mixture strategy substantially exceeds all reported prior work: the next best are InternLM2-StepProver at 54.5% (Table 1) and Lean-STaR at 46.3%. The gap of nearly 9 percentage points is substantial for this benchmark. On ProofNet, the 25.3% exceeds InternLM2-StepProver's 18.1% and ReProver's 13.8% by even larger relative margins.

However, a critical qualification is needed: the sample budget accounting is not truly comparable across methods. The paper attempts to normalize by defining K as total model invocations, but a single whole-proof generation (up to 2,048 tokens) and a single tactic generation (maybe 20–50 tokens) consume vastly different FLOPs. InternLM2-StepProver at 64 × 32 × 100 budget performs 64 × 32 × 100 = 204,800 tactic generations. DeepSeek-Prover-V1.5 at 32 × 6400 performs 32 × 6400 = 204,800 whole-proof generations — the same count of invocations, but each whole-proof generation produces more tokens than a single tactic. A more rigorous FLOPs-matched comparison is not provided, which makes the "state-of-the-art" claim depend on whether one considers whole-proof generations and tactic steps as equivalent units of compute. The paper's own RMaxTS method blurs this line further, since each expansion generates multiple tactics at once. The field does not have a standardized compute accounting, and this paper does not fully solve that problem.

Additionally, the 63.5% result uses a mixture strategy (16 × 6400 non-CoT + 16 × 6400 CoT = 32 × 6400 total), which effectively doubles the budget compared to the pure CoT RMaxTS result of 62.7% at half the budget (16 × 6400). The improvement from 62.7% to 63.5% when doubling the budget from 16 × 6400 to 32 × 6400 is only 0.8 percentage points, suggesting significant diminishing returns.

---

Claim 2: "RLPAF produces genuine enhancement of fundamental capabilities, not just better top-K selection."

The evidence for this claim comes from Figure 3, which shows RL improving pass@1 and pass@K across all K values, and from Table 3, which shows the RL advantage persisting and growing under tree search. The finding is interesting and contrasts with prior work (DeepSeekMath), where RL primarily affected the right tail of the pass@K distribution.

But the claim rests on a specific interpretation of what "fundamental capability" means, and the paper's evidence has limitations. First, the improvement from SFT to RL is notably moderate — on miniF2F-test at pass@128, it's 50.4% → 51.6% (+1.2 percentage points; Figure 3). At larger budgets in Table 3, the RL advantage is +2.8 percentage points in single-pass (57.4% → 60.2%) and +3.7 percentage points in RMaxTS (59.0% → 62.7%). These are real but modest gains, especially compared to the 20.7 percentage-point jump from base to SFT (29.7% → 50.4%). RL improves the model, but the magnitude of improvement is an order of magnitude smaller than the SFT gain. The paper's narrative emphasizes RL's significance, but the quantitative contribution is heavily dominated by SFT.

Second, the paper does not provide a mechanistic explanation for why RL improves fundamental capability in this setting but not in natural language math. The explanation offered — that binary verification from Lean provides a "perfectly accurate oracle" — is plausible but untested. One could equally hypothesize that the RL improvement is simply a form of data augmentation (generating more on-policy training trajectories that happen to be correct) rather than a qualitative shift in capability. The difference between "selecting better from existing candidates" and "generating better candidates" is hard to distinguish without counterfactual experiments (e.g., using the SFT model as a proposal distribution for a fixed selection policy vs. using the RL model for the same).

Third, the paper does not report pass@1 numbers explicitly in the main text (Figure 3 shows curves but does not label the pass@1 intercepts cleanly). Pass@1 is the cleanest measure of "fundamental capability," and without it reported numerically, the claim rests on visual inspection of the full pass@K curve.

---

Claim 3: "RMaxTS with intrinsic rewards is essential for tree search — without it, tree search degenerates to single-pass generation performance."

This is the best-supported claim in the paper, with Figure 5 providing clear causal evidence. The UCT (without R_intrinsic) results at 16 × 6400 achieving 61.1% — essentially equal to single-pass at 60.2% — is striking and supports the claim strongly. The addition of RMaxTS with DUCB at 62.7% provides a clear positive control: intrinsic rewards produce a real gain.

However, the absolute magnitude of the tree search benefit deserves scrutiny. The gain from RMaxTS over single-pass is +2.5 percentage points at 16 × 6400 (62.7% vs. 60.2%) and +1.2 percentage points at 4 × 6400 (59.6% vs. 58.4%). These gains, while statistically significant (standard deviations ~0.5–0.7 percentage points), are surprisingly small for a sophisticated tree search algorithm consuming substantial additional computation (32 thread workers per tree, tactic state extraction, multiple Lean verification calls per generation). The paper frames the contribution as making tree search "work at all," which is true — without intrinsic rewards, tree search provides zero benefit. But even when it works, the benefit is modest relative to the machinery involved. This raises a question the paper doesn't address: under what conditions does tree search provide larger benefits, and is the modest average gain masking a larger gain on a subset of problems?

There is no per-problem-difficulty breakdown for tree search gains, analogous to what the example reference paper provided for search vs. best-of-N across difficulty quintiles. We don't know whether RMaxTS helps primarily on easy problems (where systematic exploration rounds out coverage), hard problems (where novelty-driven exploration finds uncommon proof paths), or medium problems. This is a significant gap — difficulty-stratified analysis is standard for this type of work and would strengthen the contribution considerably.

---

Claim 4: "The mixture of CoT and non-CoT prompting provides complementary advantages."

The quantitative evidence for this claim comes from Table 3: mixture strategies consistently outperform pure strategies. At 16 × 6400 in single-pass RL, mixture achieves 60.7% vs. 60.2% (CoT only) and 57.4% (non-CoT only). For RMaxTS at 32 × 6400, mixture achieves 63.5% vs. the best single-mode result of 62.7% (CoT only) — a +0.8 percentage-point gain.

These gains are small relative to the doubling of compute (the mixture at 32 × 6400 requires running both modes). If one had a fixed budget and had to choose between doubling the CoT budget or splitting between CoT and non-CoT, it's unclear from the paper's data which would be optimal — Table 3 doesn't show, for example, 32 × 6400 pure CoT vs. (16+16) × 6400 mixture. The complementary strengths argument is qualitatively illustrated in Appendix B with selected examples, but there is no quantitative analysis of what fraction of problems are solved uniquely by each mode, or whether the small aggregate gain from the mixture justifies the complexity of running two prompting strategies.

---

Missing experiments that would strengthen the paper:

• Difficulty-stratified analysis of all results. The paper never breaks down performance by problem difficulty (e.g., competition level, problem domain, proof length). This is a standard expectation for theorem proving benchmarks and would reveal where the gains are concentrated.
• FLOPs-matched or wall-clock comparison. The sample budget normalization across paradigms is acknowledged as approximate. A direct comparison that accounts for tokens generated, Lean verification time, and communication overhead would clarify whether the hybrid whole-proof/tree-search approach is actually more compute-efficient or simply uses a favorable budget definition.
• Ablation of expert iteration and thought annotation. The SFT stage introduces three simultaneous changes (more data, thought annotation, tactic state insertion), and the paper reports the aggregate improvement from base to SFT without isolating each contribution. This makes it impossible to determine whether the thought-augmented proof generation is actually driving improvement or whether data quantity alone would suffice.
• Pass@1 numbers reported explicitly. The claim about fundamental capability improvement would be more directly supported with numerical pass@1 values (with confidence intervals) rather than only pass@K curves.
• Analysis of where tree search helps vs. doesn't help. The average gain of +2.5 percentage points from RMaxTS might be the average of large gains on a subset of problems and zero gain (or even negative impact) on others. Understanding this distribution is essential for practitioners deciding whether to deploy tree search.
• Results on more model scales. All experiments use the 7B model. The paper positions the pipeline as an "AlphaZero-like" system where scaling model capacity could further improve results, but there is no evidence that the methods work at different scales or that the RL + tree search gains persist or grow with model size.

---

Conditional nature of the claims:

The paper's results clearly hold under the specific experimental conditions: 7B model, Lean 4, miniF2F and ProofNet benchmarks, the specific SFT and RL training recipes described, and the compute budgets tested. Extrapolation to different model scales, different proof assistants (Isabelle, Coq), different mathematical domains, or different budget regimes is not supported by the reported experiments. The paper's strongest contributions — the truncate-and-resume mechanism and the RMaxTS algorithm — are demonstrated to work in a specific regime with modest absolute gains. Whether these methods would provide larger gains with larger models (where the proposal distribution is better, potentially making tree search more productive) or whether they would be unnecessary (because a sufficiently capable model generates correct proofs without search) is an open question that the paper does not address.

6. Limitations and Trade-offs

6.1 The Sample Budget Accounting Across Paradigms Is Not Truly Comparable

The assumption or constraint. The paper defines the sample budget K uniformly across single-pass whole-proof generation, best-first-search, and tree search methods, asserting that this "aligns the computation budget across different generation schemes" (Section 4.1). For single-pass methods, K equals total proof generations; for best-first-search, K = N × S × T (attempts × tactics per expansion × expansion iterations); for tree search, K = N × T (attempts × model generations). The paper explicitly acknowledges that this is an approximation and does not account for: the variable token length per generation (whole-proof generations produce up to 2,048 tokens, while tactic-level generations produce tens of tokens), the cost of repeated Lean prover invocations, the overhead of tactic state extraction from the REPL, or the CPU resources for managing the search tree across 32 thread workers per tree and thousands of CPU cores.

The consequence. The headline comparison — that DeepSeek-Prover-V1.5-RL at 3,200 whole-proof generations (54.9%) surpasses InternLM2-StepProver at 64 × 32 × 100 = 204,800 tactic generations (54.5%) — is misleading if interpreted as a computational efficiency claim. A single whole-proof generation of 2,048 tokens from a 7B model involves approximately 7B × 2,048 × 2 ≈ 2.9 × 10¹³ FLOPs (using the standard 2ND forward-pass approximation), while 204,800 tactic generations averaging ~50 tokens each involve 7B × 50 × 204,800 × 2 ≈ 1.4 × 10¹⁴ FLOPs — roughly 5× more. However, this FLOP accounting ignores the communication cost: InternLM2-StepProver calls the Lean prover 204,800 times (once per tactic), while DeepSeek-Prover-V1.5 calls it only 3,200 times (once per whole-proof generation). The Lean prover verification time is not negligible — the paper sets a 300-second timeout per verification — and the total wall-clock time for 204,800 tactic verifications could easily dominate the FLOPs advantage. Without a unified compute metric (total FLOPs, total wall-clock time on equivalent hardware, or total monetary cost), a practitioner cannot determine which approach is actually more efficient for a given budget.

What evidence exists in the paper. The paper provides no FLOPs-matched comparison, no wall-clock measurements, and no per-generation token count averages. The only normalization is the sample budget K, which equates a 2,048-token whole-proof generation with a single-tactic generation as "one model invocation." This is an acknowledged limitation of the field more broadly — there is no standard compute accounting for theorem proving — but the paper does not attempt to quantify the discrepancy or provide the raw data (average tokens per generation, average Lean verification time per attempt) that would enable readers to perform their own normalization. The parallelization infrastructure description (Section 3.4) mentions "thousands of CPU cores" and 256 MCTS runners with one GPU each, but provides no cost model.

Mitigation status. The paper does not address this limitation. It acknowledges the normalization scheme as a practical convention ("we display the sample budget K according to the following rules to align the computation budget across different generation schemes," Section 4.1) but does not discuss its limitations or provide alternative metrics. No future work is suggested on standardizing compute accounting for theorem proving benchmarks.

---

6.2 The Hardest Problems See No Benefit from Any Method, and Difficulty Is Not Characterized

The assumption or constraint. The paper's methods are evaluated on benchmarks (miniF2F and ProofNet) that contain problems spanning a wide range of difficulty — from simple algebraic identities to IMO competition problems and undergraduate-level abstract algebra. However, the paper provides no difficulty-stratified analysis of where the gains from SFT, RL, or RMaxTS are concentrated. There is no breakdown by problem source (AMC vs. AIME vs. IMO), by proof length, by mathematical domain, or by any learned difficulty metric analogous to the pass@1-based quintile binning used in comparable work.

The consequence. Without difficulty stratification, the headline pass rates (63.5% on miniF2F, 25.3% on ProofNet) aggregate over problems where the model succeeds easily, problems where it sometimes succeeds with search, and problems where it never succeeds. A practitioner cannot determine whether the model is useful for their specific use case — e.g., whether it reliably proves AMC-level problems but fails on IMO, whether it handles algebra but not number theory, whether tree search helps primarily on problems of intermediate difficulty. More critically, the absolute ceiling of the approach is invisible: on the hardest problems in each benchmark, the pass rate may be near zero regardless of compute budget, training stage, or search algorithm. The paper's abstract and introduction present a narrative of continuous improvement (50.0% → 60.2% → 63.5%), but if the hardest problems account for, say, 30% of the benchmark and the model solves essentially none of them, then the maximum achievable pass rate is ~70%, and the remaining gap is concentrated in a regime that requires fundamentally different capabilities. The reader receives no information about where the ceiling lies or what problems it consists of.

What evidence exists in the paper. The paper does not report any difficulty-stratified results. The ablation study (Table 3, Figure 5) and the CoT vs. non-CoT comparison (Appendix B) present only aggregate numbers. Selected qualitative examples in Appendix B illustrate problem-specific differences between CoT and non-CoT modes but do not constitute a systematic difficulty analysis. The ProofNet benchmark has a natural difficulty gradient (undergraduate topics), and the drop from 63.5% on miniF2F to 25.3% on ProofNet is noted but not decomposed by topic or difficulty within ProofNet. The paper's analysis of the training stage progression (Figure 3) shows that pass@K curves improve monotonically, but these are aggregate curves that could mask a bimodal distribution where gains on easy problems saturate while hard problems remain at zero.

Mitigation status. The paper implicitly acknowledges the sparsity of progress on hard problems through the prompt filtering strategy for RL training (Section 2.3): they select only theorems where the SFT model has "a moderate success rate," explicitly excluding theorems where the model always fails. This filtering is sensible for RL training (no positive feedback means no learning signal), but it means the RL process was never exposed to the hardest problems and therefore cannot have learned to improve on them. The paper does not discuss this as a limitation or analyze the fraction of the benchmark excluded by this filtering. The "AlphaZero-like pipeline" envisioned in the conclusion (Section 5) suggests that future work on critic models and credit assignment might help with hard problems, but no concrete evidence or analysis supports this conjecture.

---

6.3 The Cost of Tactic State Extraction and RL Training Data Generation Is Not Accounted For

The assumption or constraint. The paper's training pipeline depends on two expensive data generation steps that are not included in the reported training compute budget. First, the expert iteration process for SFT data construction requires repeatedly: generating proofs with the current model, verifying them with the Lean prover, annotating them with chain-of-thought comments using DeepSeek-Coder V2 236B (a 236B-parameter model, approximately 34× larger than the model being trained), and retraining. Second, the tactic state annotation for the auxiliary prediction task requires extracting tactic information from the Lean REPL for every tactic in every valid proof — a process that involves running the Lean prover on potentially millions of proof steps and extracting the before-and-after tactic states using tools from LeanDojo (Section 2.2). The paper reports that the final SFT dataset consists of 9,645,000 sequences, each containing multiple tactics with annotated states, but provides no estimate of the computational cost to generate these annotations.

The consequence. The reported "efficiency" of the approach — particularly the 7B model achieving 63.5% on miniF2F — must be understood in the context of a training pipeline that depends on inference from a much larger model (DeepSeek-Coder V2 236B) for thought annotation and on repeated verification of millions of proof attempts during data construction. A practitioner attempting to replicate this pipeline would need access not only to the 7B model training infrastructure but also to a 236B-parameter code model and a large-scale Lean verification cluster, neither of which is accounted for in the reported compute budget. The expert iteration loop, in particular, is potentially the dominant computational cost: each iteration generates proofs with the current model, verifies them, and retrains, and the paper does not specify how many iterations were performed or how many GPU-hours were consumed.

Moreover, the dependence on DeepSeek-Coder V2 236B for thought annotation raises a subtle methodological concern: the quality of the chain-of-thought annotations is a function of the annotator model's capability, and the paper provides no evaluation of annotation quality or ablation showing that the specific annotator model matters. If a different annotator model produced different (worse) annotations, would the proof generation quality degrade proportionally? This external dependency means the reported SFT gain is not purely a function of the 7B training recipe — it is partially a transfer from a much larger model.

What evidence exists in the paper. The paper does not report any compute metrics for the SFT data construction pipeline. The expert iteration process is described qualitatively (Section 2.2: "This involves generating proofs using the language model, verifying the generated proof data, retraining the model with the verified data, and then using the optimized model to generate additional proof data"), but the number of iterations, the volume of generated proofs per iteration, the inference cost for DeepSeek-Coder V2 annotation, and the Lean verification cost are all absent. The RL training data filtering (reducing to ~4,500 theorems) is reported, but the cost of generating the initial pool of proofs used to assess the SFT model's success rate is not. The paper's open-source release includes the trained models and tree search code, but the data generation pipeline cost is not recoverable from this release.

Mitigation status. The paper does not discuss the cost of data generation as a limitation. The expert iteration and annotation processes are described as methodological contributions, not as costs to be optimized. The open-source release partially mitigates this for end users (they can use the pre-trained models without rerunning data generation), but does not help a practitioner who wants to adapt the pipeline to a new domain, proof assistant, or model architecture. The paper suggests no future work on reducing the cost of data annotation or eliminating the dependency on larger annotator models.

---

6.4 The Improvement from RMaxTS Tree Search Is Modest and Its Benefit Per Problem Is Unknown

The assumption or constraint. The paper presents RMaxTS as a core algorithmic contribution — an exploration-oriented MCTS algorithm that "diversifies the generation of proof steps" (Section 5) through intrinsic rewards and discounted UCB. The ablation study (Figure 5) demonstrates that intrinsic rewards are necessary for tree search to outperform single-pass generation, which is a valuable diagnostic result. However, the paper does not analyze how much tree search helps per problem or on what kind of problems it helps most.

The consequence. The absolute gain from RMaxTS over single-pass generation is modest. At 16 × 6400 budget in CoT mode, RMaxTS achieves 62.7% vs. single-pass at 60.2% — a +2.5 percentage-point gain (Table 3). At 4 × 6400, the gain is +1.2 percentage points (59.6% vs. 58.4%). At 1 × 3200, the gain is +0.1 percentage points (55.0% vs. 54.9%) — within the reported standard deviation. These gains, while statistically detectable, are surprisingly small relative to the computational complexity of the tree search infrastructure: 32 thread workers per tree, 256 parallel MCTS runners, asynchronous Lean verification on thousands of CPU cores, and management of a tree data structure with non-stationary intrinsic reward tracking.

For a practitioner, the decision to deploy tree search depends on whether the +2.5 percentage-point gain justifies the infrastructure cost. But the paper provides no information about which problems account for this gain. It is possible that the 2.5 points come from a small subset of problems where tree search is dramatically more effective (e.g., proofs requiring 10+ tactics where systematic exploration discovers correct paths that random sampling misses), while on the majority of problems, tree search provides no benefit. Alternatively, the gain might be a uniform +2.5% across all problems, which would be a different (and less compelling) value proposition — investing substantial search infrastructure for a uniform tiny improvement. Without per-problem or difficulty-stratified results, the practitioner cannot assess whether tree search is worth deploying for their specific problem distribution.

The gap between RMaxTS and the no-intrinsic-reward baseline (UCT) is clearer: UCT at 16 × 6400 achieves 61.1% vs. RMaxTS at 62.7%, a +1.6 percentage-point gap. But the UCT-to-single-pass gap is nearly zero (61.1% vs. 60.2%), confirming that the entire benefit of tree search is attributable to the intrinsic rewards mechanism. This makes RMaxTS a necessary condition for tree search to work at all, but it does not make tree search itself a large-effect intervention.

What evidence exists in the paper. The only evidence is the aggregate pass rates in Table 3 and the pass@K curves in Figure 5. The pass@K curves in Figure 5 show that RMaxTS and single-pass generation have nearly identical slopes — the curves are parallel, with RMaxTS consistently ~1–2 percentage points above single-pass across all budget levels from 0 to 6,400. This parallelism suggests that tree search provides a constant additive benefit across budgets rather than an increasing benefit as more compute is invested — a pattern that is inconsistent with the narrative that tree search enables "extensive exploration of the proof space" (Section 1.1), which would predict increasing gains at higher budgets as more of the space is covered. If the benefit is constant regardless of budget, tree search may be doing something simpler than systematic exploration — perhaps it is merely providing a small diversity bonus from the truncate-and-resume mechanism without the full exploration dynamics being realized.

Mitigation status. The paper does not address the modesty of the tree search gain or provide per-problem analysis. The conclusion (Section 5) frames RMaxTS as "highly effective in advancing superhuman performance" and suggests that adding a critic model (the exploitation aspect) would further improve results, implying that the current gains are a lower bound. But this is a forward-looking statement without evidence. The paper does not analyze the gap between the current RMaxTS performance and what a hypothetical optimal search algorithm could achieve, nor does it bound the maximum possible gain from better exploration given the current proposal model quality.

---

6.5 Single Benchmark Domain (Lean 4) and Single Model Scale (7B) Limit Generalization Claims

The assumption or constraint. All experiments use a single proof assistant (Lean 4), on two specific benchmarks (miniF2F and ProofNet), with a single model architecture and scale (DeepSeekMath-Base, 7B parameters). The paper's claims about the effectiveness of RLPAF ("genuine enhancement of fundamental capabilities," Section 2.4), the truncate-and-resume mechanism ("a unified approach combining the strengths of both proof-step and whole-proof generation," Section 1), and RMaxTS ("an innovative Monte-Carlo tree search algorithm," Section 1.1) are supported only within this narrow scope.

The paper explicitly mentions that pre-training included Isabelle and Metamath data (Section 2.1), but no evaluation is performed on Isabelle or Metamath benchmarks. The conclusion extrapolates ambitiously: "The framework of DeepSeek-Prover-V1.5 is designed to establish an AlphaZero-like pipeline for formal theorem proving" (Section 5), suggesting generality across proof assistants and problem domains, but the experimental support is entirely Lean 4-specific.

The consequence. The transfer of these methods to other proof assistants is uncertain for several reasons. Different proof assistants have fundamentally different tactic languages, verification models, and proof structures. Lean 4's tactic language is relatively high-level (tactics like nlinarith can close substantial arithmetic goals in one step), which may make whole-proof generation easier — the model can rely on powerful automation tactics rather than constructing detailed proof terms. In a system like Coq, where proofs are constructed as explicit proof terms (lambda terms) rather than tactic scripts, the truncate-and-resume mechanism would need to be redesigned because the notion of "truncating at a verification error" operates on a different syntactic level. In Isabelle, the structured proof language (Isar) interleaves natural language and formal steps differently than Lean's tactic mode, potentially affecting the thought-augmented proof generation approach.

More fundamentally, the paper's key design decisions may be coupled to the 7B model scale. The truncate-and-resume mechanism depends on the model being trained to predict tactic states as an auxiliary objective — the hypothesis is that this improves internal state tracking and reduces compounding errors. At larger model scales (e.g., 70B+), the base model may already have more robust internal state representations from pre-training, reducing the need for explicit tactic state prediction. Conversely, at smaller scales, the auxiliary task may consume capacity that would be better spent on proof generation itself. The paper provides no scaling analysis across model sizes to characterize how the relative contributions of each training stage change.

The 7B scale also affects the interpretation of the RL results. The paper contrasts its finding (RL improves fundamental capabilities) with DeepSeekMath (RL primarily improves pass@K), attributing the difference to the perfect accuracy of the Lean verifier. But DeepSeekMath used a 7B model for natural language math, while the verifier-based setting is formal theorem proving — the tasks are different in more ways than just the reward signal. Comparing across tasks without controlling for model scale or task difficulty conflates multiple variables. A within-task comparison at multiple model scales would be needed to isolate the effect of reward accuracy.

What evidence exists in the paper. All results are on Lean 4 with a 7B model. The paper provides no experiments on other proof assistants, other model scales, or other formal reasoning domains. The cross-benchmark comparison (miniF2F vs. ProofNet) provides some evidence of generalization across difficulty levels but not across proof assistants or model architectures. The paper references the use of Isabelle and Metamath in pre-training data but does not evaluate on those systems.

Mitigation status. The paper does not claim generalizability to other proof assistants as a demonstrated result; the framing in Section 5 ("designed to establish an AlphaZero-like pipeline") is explicitly aspirational. However, the abstract, introduction, and conclusions present the methods without qualification as to their scope, which may lead readers to assume broader applicability than the experiments support. The open-source release makes the 7B Lean 4 model available, enabling other researchers to test transfer, but the paper provides no guidance on how to adapt the pipeline to new settings or what components are likely to be domain-specific.

---

6.6 The RL Training Prompt Filtering Excludes the Hardest Problems and Creates an Unmeasured Selection Bias

The assumption or constraint. The RL training stage uses a subset of approximately 4,500 theorem statements filtered from the SFT dataset, selected because DeepSeek-Prover-V1.5-SFT has a "moderate success rate" on them (Section 2.3). The paper explicitly states the rationale: "This ensures that the model has room for improvement while still being able to receive positive feedback." The filtering criterion — moderate success rate — is not precisely quantified (what threshold? measured over how many attempts?), and the fraction of the original SFT dataset that is excluded is not reported.

The consequence. This filtering introduces a systematic selection bias whose consequences are unmeasured. The RL model is never trained on theorems where the SFT model always fails. This means the RL process cannot learn to solve problems that are outside the SFT model's initial capability range. The improvement from RL is therefore bounded above by the SFT model's frontier: RL can only improve performance on problems the SFT model can already sometimes solve; it cannot expand the set of solvable problems to include entirely new problem types or difficulty levels.

This has direct implications for the paper's claim that RL produces "genuine enhancement of fundamental capabilities" (Section 2.4). The observed improvement could be entirely within the SFT model's existing capability envelope — e.g., making the model more consistent on problems it already sometimes solves, reducing the variance of its proof generation, or shifting probability mass from incorrect to correct proof strategies on problems where both are within the model's repertoire. These are real improvements, but they are qualitatively different from teaching the model entirely new capabilities (solving problem types it previously could never solve). The paper's framing does not distinguish between these two types of improvement, and the filtering strategy ensures the latter cannot be observed.

Furthermore, the exclusion of hard problems from RL training means that any evaluation metric that weights problems uniformly (as the standard pass rate does) may overstate the practical impact of RL. If the hardest 20% of problems are excluded from RL training and the RL model's performance on them is identical to the SFT model (because it was never trained on them), then the aggregate pass rate gain from RL is diluted by a subpopulation on which RL provides zero benefit. The paper does not report RL vs. SFT performance specifically on the problems that were included in RL training vs. excluded, making it impossible to assess the filtering's impact.

What evidence exists in the paper. The paper reports that ~4,500 theorems are retained after filtering (Section 2.3) but does not report the pre-filtering size or the filtering threshold. The SFT dataset contains 9,645,000 sequences from "a wide range of formal theorems" including Mathlib4, synthetic theorems, and benchmarks (Section 2.2), but the number of unique theorems is not stated, preventing calculation of the retention ratio. Figure 3 and Table 3 show aggregate pass rates, not stratified by inclusion in RL training. There is no ablation comparing RL performance on filtered-in vs. filtered-out problems, which would directly measure the selection bias's impact.

Mitigation status. The paper acknowledges the filtering implicitly through its description of the rationale, but does not discuss the bias it introduces or measure its consequences. The filtering strategy is presented as a practical choice to handle reward sparsity, not as a limitation of the RL approach. The paper does not suggest future work on extending RL to harder problems (e.g., through reward shaping, curriculum learning, or exploration bonuses during training), which would be necessary to overcome this fundamental ceiling on RL's benefit.

7. Implications and Future Directions

How This Work Changes the Landscape

This paper does not introduce a paradigm shift in the sense of replacing one fundamental approach with another — the core components (whole-proof generation, SFT on formal proof data, MCTS, RL with verification feedback) all existed prior. Rather, it makes a diagnostic and architectural contribution that reframes how the field should think about integrating these components. The lasting impact will likely come from three specific reframings.

First, the truncate-and-resume mechanism dissolves the boundary between whole-proof and proof-step generation as architectural alternatives. Prior to this work, the field implicitly treated these as competing paradigms — one chose efficiency (whole-proof) or feedback-richness (proof-step) and accepted the corresponding sacrifice. The paper demonstrates that this choice is false: a single model, trained with a unified objective that includes predicting intermediate tactic states as an auxiliary task, can serve both deployment modes. The truncate-and-resume mechanism — generating a whole proof, submitting it to Lean, and using the location of the first verification error to extract the successful prefix and the exact tactic state at the failure point — converts the proof assistant from a binary grader into a state-space annotator that provides ground-truth intermediate states on demand, without the per-step communication overhead of traditional proof-step generation. This means the efficiency/feedback tradeoff becomes a spectrum rather than a binary choice: deploy in pure single-pass mode for easy problems, invoke truncate-and-resume occasionally for medium problems, or run full RMaxTS for hard problems. The same model supports all three without retraining.

This reframing makes whole-proof generation a more attractive research direction than it was before, because its primary limitation — lack of intermediate feedback — is shown to be addressable without abandoning the paradigm's computational advantages. Conversely, it makes pure proof-step generation less attractive as a standalone approach, because the communication overhead of per-tactic model-prover round-trips is now demonstrably unnecessary for achieving state-of-the-art results. The paper's 54.9% pass@3200 in single-pass mode already surpasses InternLM2-StepProver's 54.5% with 64×32×100 tactic generations (Table 1), and adding RMaxTS — which uses intermediate feedback selectively, not at every step — pushes performance to 63.5%. If the goal is state-of-the-art pass rates, the hybrid approach dominates both pure strategies.

Second, the paper provides the first clear causal evidence that tree search in formal theorem proving requires exploration mechanisms beyond standard UCT. The field has applied MCTS to theorem proving — most notably Hypertree Proof Search (Lample et al., 2022) — under the implicit assumption that the UCB exploration bonus would suffice to drive search in sparse-reward environments. The ablation study in Figure 5 disproves this assumption decisively: UCT without intrinsic rewards achieves 61.1% at 16×6400 budget, essentially identical to single-pass generation at 60.2%, confirming that standard MCTS provides zero benefit over blind sampling. Intrinsic rewards are not an enhancement — they are a necessary condition for tree search to outperform random generation.

This finding redirects research attention from search algorithm design (better tree policies, more sophisticated selection mechanisms) toward reward design for exploration. The paper shows that a simple exploration reward — +1 for discovering a previously unseen tactic state — combined with discounting to handle non-stationarity, is sufficient to make tree search productive. This opens a design space of alternative intrinsic reward functions: rewards based on goal reduction (how much simpler are the remaining goals after a tactic?), rewards based on proof length progress, or learned intrinsic rewards from a curiosity module. The key lesson is that in sparse-reward formal reasoning, how you reward partial progress is more important than how you search the tree, because without meaningful rewards, the tree structure is irrelevant. This is a conceptual inversion of the typical MCTS narrative (where search algorithm innovation is primary) and a valuable generalization to any domain where ground-truth intermediate states are accessible but binary success is the only extrinsic signal.

Third, the paper resolves a latent tension in the RL-for-reasoning literature about whether RL improves fundamental capability or merely candidate diversity. DeepSeekMath (Shao et al., 2024) found that RL primarily improved pass@K rather than pass@1 in natural language math reasoning, attributing this to approximate reward models that could be exploited without genuine reasoning improvement. This paper shows the opposite pattern (Figure 3): RL improves performance across all K values, with gains stable rather than concentrated at the right tail, and the improvement persists and amplifies under tree search (Table 3). The resolution lies in the nature of the reward signal, not the RL algorithm: when rewards are a perfectly accurate binary oracle (Lean verification), RL cannot hack them and must improve the policy itself to increase expected reward. When rewards are a learned approximator (natural language math grading), RL can exploit reward model biases without improving reasoning.

This reframing has direct implications for the RL-for-reasoning research agenda. It suggests that effort invested in making reward signals more accurate — through formal verification, through better automated grading, through decomposition of binary rewards into step-level signals — will be more productive than effort invested in RL algorithm innovations. The GRPO algorithm used here is the same as in DeepSeekMath; the difference in outcomes comes from the verifier, not the optimizer. For practitioners, this means: if you can provide a noiseless reward oracle (formal verification, unit tests, exact solvers), RL will genuinely improve your model's capability. If you must rely on learned reward models, expect RL to primarily improve coverage and candidate selection rather than single-attempt quality.

None of these reframings constitute a paradigm shift on the scale of AlphaZero — the paper does not introduce a fundamentally new learning or search paradigm. But they are high-value diagnostic contributions that clarify why certain previously observed phenomena occur (why UCT fails, why RL sometimes improves capability and sometimes doesn't) and provide concrete architectural guidance (how to build a unified whole-proof/step-wise prover, what reward structure makes tree search work). These will shape how subsequent work designs theorem provers and, more broadly, how the field thinks about integrating symbolic verification with neural generation.

---

Follow-Up Research This Work Enables

Scaling the model size to characterize how RL and tree search gains depend on base capability. The paper uses a single 7B model throughout. A natural extension is to replicate the full training pipeline (pre-training on formal languages, SFT with thought augmentation and tactic state prediction, RLPAF with GRPO, RMaxTS evaluation) at multiple scales — e.g., 1B, 7B, 34B, 70B — to answer two specific questions. First, does the RL gain (absolute percentage points) increase, decrease, or stay constant with model scale? If larger models benefit more from RL (because they generate more diverse candidate proofs per prompt, giving the GRPO advantage signal more variance to work with), this would strengthen the case for the AlphaZero-like pipeline the paper envisions. If RL gains diminish with scale (because larger models already saturate the "sometimes correct" regime), then RL is most valuable for smaller, more efficient models. Second, does the tree search gain from RMaxTS scale with model capability? A stronger proposal model might make tree search more productive (because the model generates higher-quality completions, and systematic exploration can find correct paths that random sampling misses by smaller margins) or less productive (because the model is so capable that single-pass generation already covers the correct paths). The paper's current 7B results show a modest +2.5 percentage-point gain from RMaxTS at 16×6400; whether this grows or shrinks at 34B is an open empirical question that would determine whether tree search is a complement to scaling or a substitute for it.

Training a partial-proof critic model for exploitation, completing the AlphaZero analogy. The paper explicitly identifies the exploitation counterpart of RMaxTS as the primary missing piece: "a promising future direction is training a critic model to assess incomplete proofs and prune search branches" (Section 5). Concretely, the idea is to train a value network (or fine-tune the prover model with a value head) that takes an incomplete proof prefix and its current tactic state as input and predicts the probability that a correct proof can be completed from this state. This critic could serve two roles in tree search: pruning branches with low predicted value (reducing wasted exploration) and providing a dense reward signal during backpropagation (value estimates for partial proofs, not just the binary success signal). The training data is available: the RLPAF process generates millions of proof attempts with known outcomes (the file data contains the full proof, the truncation point, and whether it succeeded or failed), providing natural labels for a partial-proof value function. A specific experimental design: train the critic on RLPAF-generated trajectories, integrate it into RMaxTS as both a pruning signal (threshold on predicted completion probability) and a reward shaping signal (backpropagating the critic's value estimate in addition to intrinsic rewards), and measure whether the tree search gain increases from the current +2.5 percentage points. The paper's finding that exploration is the bottleneck (Figure 5) suggests that adding exploitation should be complementary, not overlapping — if intrinsic rewards handle exploration and a critic handles exploitation, the combination should outperform either alone.

Difficulty-stratified analysis of where each component helps, to characterize the ceiling and guide resource allocation. The paper's results are entirely aggregate, with no breakdown by problem difficulty, proof length, or mathematical domain. A follow-up study should replicate the full evaluation pipeline and report pass rates stratified by: (1) proof length (number of tactics in the shortest known proof, to distinguish short automation-friendly problems from long multi-step reasoning problems), (2) problem source or difficulty tier (AMC vs. AIME vs. IMO within miniF2F; topic within ProofNet), and (3) a learned difficulty metric analogous to the pass@1-based binning used in comparable work. This would answer several open questions: Does RMaxTS help primarily on long proofs (where systematic exploration matters most) or is the benefit uniform? Does RLPAF improve performance on the hardest problems (contrary to the expectation from its filtering strategy), or is its benefit confined to the moderate-difficulty regime? What is the maximum achievable pass rate given the current model's capability — i.e., if we had an oracle search algorithm that always found a correct proof when one exists in the proposal distribution, what fraction of problems would remain unsolvable? This last question is critical for understanding whether future effort should go into improving the proposal model (training), the search algorithm (inference), or the reward design (credit assignment). The paper's current results cannot distinguish between a model that generates correct proofs for 80% of problems but finds them only on 63.5% (search-limited) and a model that generates correct proofs for exactly 63.5% of problems (proposal-limited). Difficulty-stratified pass@K curves with very large K (e.g., pass@infinity estimated via extrapolation) would resolve this.

Replacing the DeepSeek-Coder V2 annotator with a self-annotation procedure to eliminate the external model dependency. The SFT data construction depends on DeepSeek-Coder V2 236B — a model 34× larger than the one being trained — to annotate proof code with natural language chain-of-thought comments. This creates a methodological dependency that complicates replication and makes it unclear whether the thought-augmented training benefit comes from the annotation format or from knowledge distillation from a larger model. A specific follow-up: after one round of SFT training with DeepSeek-Coder-annotated data, use the resulting 7B model (DeepSeek-Prover-V1.5-SFT) to annotate its own correct proofs with chain-of-thought reasoning, then retrain on this self-annotated data in a second SFT round. Compare the resulting model against the externally-annotated baseline on pass@K. If self-annotation matches or approaches external annotation, the pipeline becomes fully self-contained (no model larger than 7B required). If self-annotation significantly degrades performance, it reveals that the thought-augmentation benefit is partially knowledge distillation, and alternative approaches (curriculum learning on thought generation, smaller annotator models, or RL-based thought improvement) become necessary research directions. This experiment also tests the paper's implicit assumption that the annotation format (interleaved comments) matters more than the annotator's capability.

Porting the truncate-and-resume mechanism and RMaxTS to Isabelle or Coq to test cross-assistant generalization. The paper pre-trains on Isabelle and Metamath data but evaluates only on Lean 4. The architectural claims — that truncate-and-resume unifies whole-proof and step-wise generation, that intrinsic rewards are necessary for tree search — are presented as general insights, not Lean-specific ones. A concrete replication: implement the truncate-and-resume mechanism for Isabelle (using Isabelle's tactic language and error-reporting infrastructure) and train an equivalent Isabelle prover model using the same pipeline (pre-training, SFT with thought and state augmentation, RLPAF with Isabelle verification feedback). Measure whether (a) the truncate-and-resume mechanism transfers without modification to Isabelle's different proof structure, (b) RMaxTS provides similar relative gains over single-pass generation in Isabelle as in Lean 4, and (c) the RLPAF benefit pattern (uniform pass@K improvement rather than right-tail concentration) replicates. Success would validate the paper's methods as assistant-agnostic; failure on any axis would identify which components are coupled to Lean 4's specific design (high-level tactics, error-reporting granularity, state representation format) and which are truly general.

Extending RMaxTS intrinsic rewards to reward goal simplification, not just state novelty, to provide a learning signal correlated with proof progress. The current intrinsic reward (+1 for any new tactic state) treats all state discoveries equally: reaching a state with one simple remaining goal and reaching a state with ten complex subgoals both yield the same reward, even though the former represents substantially more progress toward a proof. This means RMaxTS has no built-in preference for states that are "closer" to being solved. A natural extension is to augment or replace the novelty reward with a goal complexity reduction reward: when a tactic transforms the current goals into a new set of goals, compute a heuristic measure of goal difficulty (number of goals, depth of quantifier nesting, presence of decidable theories, etc.) and reward the reduction in difficulty. This would give the search a gradient to follow even within the space of novel states — preferentially exploring paths that simplify the problem rather than just branching it differently. The critical question is whether this reward shaping can be designed without introducing biases that degrade search quality (rewarding the appearance of simplicity rather than genuine progress). A specific experimental design: train a lightweight goal-difficulty predictor on the SFT training data (using the proof completion outcome as weak supervision — easier goals are those from which correct proofs were more frequently completed), integrate its predictions as a reward shaping term alongside RMaxTS intrinsic rewards, and measure whether the pass@K curves in Figure 5 shift upward (better sample efficiency) or the RMaxTS gain increases (better eventual performance).

---

Practical Applications and Downstream Use Cases

Automated grading and feedback for formal mathematics education. A model achieving 63.5% on high-school competition problems (miniF2F) and 25.3% on undergraduate problems (ProofNet) is not a fully reliable proof assistant, but it is a usable proof suggestion engine for educational settings. In a formal mathematics course using Lean 4, students typically spend substantial time stuck on routine proof steps — applying the wrong tactic, missing a hypothesis, or failing to recognize that a goal can be closed by a standard automation tactic. DeepSeek-Prover-V1.5 can serve as an interactive assistant: a student writes a partial proof, the model suggests completions (via the truncate-and-resume mechanism, which naturally handles partial proofs), and the Lean verifier filters incorrect suggestions. The 300-second timeout per verification is acceptable for interactive use. On miniF2F-level problems (the difficulty of advanced high-school or introductory university exercises), the model solves nearly two-thirds of problems automatically, meaning it could reduce routine proof burden significantly. The CoT mode generates natural language explanations alongside formal code, providing pedagogical value. The open-source release makes this deployable on a single A100-40G GPU, which is within the budget of many university computing clusters.

Data generation for self-improving formal mathematics libraries. The paper's expert iteration process — generate proofs, verify them, add verified proofs to the training set, retrain — is a concrete recipe for expanding formal mathematics libraries like Mathlib4. The current model at 63.5% on miniF2F suggests that on easier theorems (the first few difficulty quintiles, if one were to perform the difficulty analysis recommended above), the success rate is substantially higher — likely 80%+ on simple algebraic identities and routine calculus lemmas. By deploying DeepSeek-Prover-V1.5-RL with RMaxTS on a large corpus of unproven formal theorem statements (e.g., the Lean Workbook synthetic theorems, Mathlib4's sorry'd lemmas), and routing the verified outputs into the training data for the next iteration, the pipeline can bootstrap a growing library of formalized mathematics with minimal human annotation. The key practical advantage is the perfect verification oracle: any proof that passes the Lean kernel is guaranteed correct, so the generated training data has zero label noise, unlike synthetic data in natural language domains. The RLPAF-trained model is specifically optimized to maximize the probability of generating verifiably correct proofs, making it well-suited for this data generation role. The paper's finding that RL improves fundamental capability (pass@1, not just pass@K) matters here: for data generation, you want a model that reliably generates correct proofs on each attempt, not one that occasionally gets lucky across many attempts. A 7B model generating thousands of verified proofs per day on a modest GPU cluster could meaningfully accelerate Mathlib4's growth.

Formal verification of competition mathematics solutions. In mathematical competitions (IMO, national olympiads, the Putnam), human solutions are typically written in informal natural language and checked by human graders. Errors in human solutions — missing edge cases, implicit assumptions, leaps in logic — are common and occasionally lead to incorrect medals being awarded. A formal verification pipeline using DeepSeek-Prover-V1.5 could serve as a second-pass verification layer: after a human contestant produces an informal solution, a human formalizer translates it into a Lean statement, and the model attempts to generate a formal proof. If the model succeeds (in ~63% of high-school competition problems), the solution is guaranteed correct. If the model fails, that doesn't mean the solution is wrong — but it flags the problem for additional human scrutiny. The value proposition is asymmetric: model success provides a strong guarantee (formal verification), while model failure provides a weak signal (needs review). As pass rates improve — either through scaling or through the AlphaZero-like self-play pipeline the paper envisions — the fraction of competition problems automatically verifiable will increase. The current 63.5% on miniF2F, which includes AMC, AIME, and IMO problems, suggests this is already practical for easier competition tiers. An IMO-specific evaluation subset would clarify the current ceiling on the hardest problems.