Technical Summary: Why Agentic Theorem Prover Works

Problem Statement

Recent agentic theorem provers, which combine large language models (LLMs) with retrieval, search, and proof assistant verifiers, have demonstrated empirical success in generating verified mathematical proofs. However, existing theoretical frameworks struggle to explain this success. Classical proof theory addresses the existence of proofs, while complexity theory addresses worst-case hardness. Neither adequately explains why a specific algorithm succeeds with high probability on a fixed compute budget for the specific, biased distributions of theorems encountered in practice (e.g., library theorems, benchmark families).

The paper addresses the question: What is the probability that a specific agentic prover generates a verifier-accepted proof within a fixed budget on a specified stream of theorem instances? The authors argue that understanding this "statistical provability" is essential to explaining why components like retrieval, verifier feedback, and decomposition improve performance without contradicting classical undecidability or worst-case lower bounds.

Methodology

1. Formalization as a Reachability MDP

The authors model formal proof search as a finite-horizon reachability Markov Decision Process (MDP) with deterministic dynamics:

• State ($X$): The current proof obligation (e.g., a list of open goals in Lean) plus verifier feedback.
• Action ($A$): Prover moves such as tactics, inference rules, or retrieval commands.
• Transition ($F$): A deterministic verifier update map $F: X \times A \to X$. Invalid actions map to failure states; valid actions transition to new proof states.
• Goal ($G$): The set of solved states (empty goal lists).

This formulation treats the verifier's operational semantics as the transition kernel. The authors prove that under a faithful state abstraction, the optimal MDP success probability coincides exactly with ordinary syntactic provability within the same budget, preserving logical integrity while enabling statistical analysis.

2. Statistical Provability Definition

The core metric is Statistical Provability ($SP^\pi_B(q_0)$), defined as the probability that a prover policy $\pi$ reaches a verified proof within $B$ verifier calls, averaged over an initial theorem distribution $q_0$ and the prover's internal randomness. This is contrasted with the optimal success probability $SP^*_B(q_0)$.

The authors also track the average truncated proof length ($Len^\pi_B(q_0)$), defined as the expected number of verifier calls before success or budget exhaustion. This metric serves as a critical interpretability handle in their bounds.

3. Learning Pipeline Analysis

The paper analyzes a pipeline aligned with current practice:

1. Offline Action-Value Regression: Learning depth-wise action-value functions ($Q^*_t$) from verifier-backed rollouts (simulated proofs) on a training distribution.
2. Greedy Test-Time Proving: Using the learned scores to select the best action greedily at test time.

The analysis relies on Assumption 3.1, which posits:

• Compact concentration sets ($C_t$) where training and testing occur.
• Lipschitz continuity of the optimal value function and the hypothesis class.
• Sufficient coverage of the state-action space by the exploration distribution.
• Availability of multiple independent rollout labels per query to reduce noise.

Key Contributions and Results

1. The Main Theorem (Statistical Provability Bound)

The central result (Theorem 3.1) bounds the gap between the learned prover's success probability and the optimal prover's success probability. The bound is an occupancy-weighted sum of uniform action-value errors:

$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \leq 2 \sum_{s=1}^B P^{\hat{\pi}}_{q_0}(T_G \geq s) \cdot \epsilon_{B-s+1}$$

Where:

• $P^{\hat{\pi}}_{q_0}(T_G \geq s)$ is the probability the learned prover has not yet solved the problem at step $s$ (the unsolved-mass curve).
• $\epsilon_t$ is the uniform error bound on the learned action-value estimator at depth $t$.

Interpretation of the Error Term ($\epsilon_t$):
The error decomposes into three components:

1. Approximation Error: The inability of the hypothesis class to represent the true value function.
2. Coverage/Geometry Error: Dependent on the effective local dimension ($d_t$) and the coverage constant ($c_t$) of the training distribution.
3. Rollout Noise: Variance from the finite number of Monte Carlo labels ($m_t$) used for regression.

2. The Role of Average Proof Length

A key insight is that the leading complexity multiplier in the bound is the learned prover's average truncated proof length ($Len^{\hat{\pi}}_B(q_0)$).
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim \bar{\epsilon}_B \cdot Len^{\hat{\pi}}_B(q_0)$$
This implies that mechanisms which shorten proofs (e.g., effective decomposition, lemma introduction) directly reduce the end-to-end loss, even if the local value estimation error ($\bar{\epsilon}_B$) remains constant.

3. Margin Conditions and Fast Rates

Under a margin condition (where the gap between the best and second-best action values is sufficiently large with high probability), the bound improves to a fast rate:
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim Len^{\hat{\pi}}_B(q_0) \cdot \bar{\epsilon}_B^{\beta+1}$$
This suggests that improving action gaps (making correct moves clearly superior to incorrect ones) significantly accelerates convergence.

4. Scaling Laws

The paper derives sample-complexity heuristics. Ignoring logarithmic factors, the error scales as $n^{-1/(d+2)}$, where $n$ is the verifier-label budget and $d$ is the effective local dimension. This clarifies that "test-time scaling" gains can arise from:

• Reducing the effective horizon (shorter proofs).
• Reducing the effective geometric dimension (better retrieval/representation).
• Increasing the action-gap margin.

Significance and Claims

The paper claims to provide a component-sensitive account of why agentic theorem provers work on biased workloads. It bridges the gap between classical logic and statistical learning by showing that:

1. Verifier Feedback: Improves provability by reducing approximation error, improving coverage, and increasing action gaps.
2. Retrieval and Representation: Help by smoothing the value function, concentrating the state space on lower-dimensional regions, and pruning bad choices to increase margins.
3. Proof Shortening: Mechanisms like decomposition reduce the "occupancy weight" (average proof length), which is the primary multiplier of error in the bound.

The authors emphasize that this theory does not contradict worst-case hardness. Instead, it explains why agentic systems succeed on the specific, structured distributions of theorems found in practice (library theorems, benchmarks) where proofs are short, gaps are large, and coverage is good. The framework treats the verifier as an information channel and the prover as a statistical learner extracting useful information under a limited budget, offering a rigorous justification for the engineering choices (retrieval, decomposition, verifier loops) prevalent in modern agentic systems.