Summary (Overview)

• LEVER is a novel proof search algorithm for LLM-powered theorem provers that makes the objective over correct proofs programmable and optimizes it during search, rather than finding any correct proof and improving it post-hoc.
• The algorithm scores partial proofs over an AND/OR graph, combining realized costs with predicted values for open subgoals, so the objective (computational cost, proof length, topical impurity, or weighted combinations) guides search from the start.
• On PutnamBench in Lean 4, LEVER reduces computational cost by 34% (from $1.44 to $0.95 per problem) while raising the solve rate from 80.0% to 96.3% under a $3 budget, compared to a strong single-conversation agent.
• For topical impurity, LEVER achieves a 42% reduction vs. 33% for post-hoc refactoring, at two-thirds the cost and with greater reliability; on proof length, it approaches refactoring performance.
• LEVER enables explicit quality–cost trade-off curves via a tunable weight parameter λ, letting users choose how much a better proof is worth.

---

Introduction and Theoretical Foundation

Background and Motivation

Mathematicians value proofs for more than correctness—simplicity, purity, and computational cost vary widely among correct proofs. The paper cites the four-color theorem as an example: a substantially different proof fifty years later exposed new structure in planar graphs and led to a near-linear-time coloring algorithm.

Current LLM-powered theorem provers largely search for any correct proof, and improve quality only afterwards through post-hoc refactoring. The authors argue this separation is suboptimal:

"A post-hoc method revisits a proof already paid for, and possibly inherits a trajectory (mathematical argument) chosen for a different objective."

Key Insight

The central idea of LEVER is to score a proof before it is finished. A partial proof has some goals proved and others open. LEVER scores it as:

$$\text{Partial proof score} = \text{realized score of proved parts} + \sum_{\text{open goals}} \text{predicted value}$$

At any time, only the partial proof with the best score is expanded, so the objective steers search from the beginning.

Theoretical Foundation: AND/OR Graphs

An AND/OR graph is a bipartite DAG $G = (V_{OR} \sqcup V_{AND}, E)$ where:

• OR nodes are goals (theorems/lemmas to prove)
• AND nodes are decompositions of a goal into subgoals
• The root OR node $r$ is the theorem to prove
• An OR node is solved if any child is solved; an AND node is solved if all children are solved

A solution subgraph $S \subseteq G$ satisfies: (i) $r \in S$; (ii) for each OR node in $S$, exactly one AND child is picked; (iii) for every AND node in $S$, all children are picked; (iv) leaves in $S$ are solved.

Cost back-propagation follows the recursive equations:

$$V(n) = \sum_{d \in \operatorname{ch}(n)} c(n, d) + V(d) \quad (n \in V_{AND}), \qquad V(n) = \min_{d \in \operatorname{ch}(n)} c(n, d) + V(d) \quad (n \in V_{OR})$$

with $V = 0$ at a solved leaf and $V = \infty$ at a false goal. $V(r)$ is then the cost of the cheapest solution subgraph.

---

Methodology

Proof Search as an MDP

LEVER models proof search as a Markov Decision Process:

• States: The graph built so far, with statuses and edge costs (fully observed)
• Actions: Which OR node(s) to expand, or STOP
• Transition: Stochastic—expanding the same goal twice may yield different graphs
• Reward: $-s_t$ for expansions at time $t$, and $-V(r)$ at termination ($-\infty$ if unsolved)

The objective is to minimize: $V(r) + \sum_t s_t$

The LEVER Algorithm

Algorithm 1: LEVER
Input: root r, budget B
1  Prior(r)
2  while spent < B do
3     T ← Select(r)
4     if T = ∅ then break
5     foreach g ∈ T do
6        D ← Expand(g)
7        foreach d ∈ D do Prior(d)
8        Backpropagate(g)
9  return the best solution subgraph of r

Each iteration has three steps:

1. Selection: Descend from the root along the current best solution subgraph. When the argmin child is a prior, its goal is expanded (a "redraw" for goals that already have children). A redraw must beat the incumbent by a factor δ to account for noisy values.

2. Expansion: An LLM proposes a new decomposition (AND node), the Lean oracle checks it, and each subgoal becomes a new OR node. Edge costs reflect expansion cost; new subgoals receive priors from the value function.

3. Backpropagation: New costs pass upward through the recursion, updating priors on the path.

Adaptive Prior Updates

The value function's prediction $V_0(g)$ is combined with realized costs $v_1, \ldots, v_k$ via a Bayesian update. Modeling log-cost as normal with unknown mean $\mu_g$:

$$\hat{\mu}_g = \frac{n \log V_0(g) + \sum_{i=1}^{k} \log v_i}{n + k}, \qquad n = \sigma^2 / \rho^2, \tag{1}$$

where $\sigma$ is the spread of repeated draws and $\rho$ is the value function's error. The prior estimate is worth $n$ draws; each realized draw counts as one. The value estimate is the posterior geometric mean: $\tilde{V}(g) = \exp(\hat{\mu}_g)$.

Combined Objective

For any metric $m$ (backed up as $V_m$ with edge costs $c_m$) balanced against computational cost at price $\lambda_m$ dollars per unit:

$$C(n) = V_{comp}(n) + \sum_m \lambda_m V_m(n)$$

With all $\lambda_m = 0$, LEVER minimizes computational cost alone.

Agentic System Design

• Expansion: Each expansion is one conversation of an LLM agent with a Lean workspace (compilation tools, Mathlib retrieval, Python, file I/O)
• Planning: A planner writes an informal proof before search; this plan is carried in every expansion's system prompt
• Context management: Each subgoal's conversation starts from its parent's compacted output, keeping contexts local
• Soundness: The Lean kernel checks every decomposition; final proofs must compile without sorry, admit, axiom, or native decide

Metrics

• Computational cost (comp): Dollars spent on LLM calls
• Proof length (len): Lean tokens added by the proof (helpers included, comments excluded)
• Topical impurity (imp): Count of references to library theorems outside the theorem's subject (determined by namespaces/directories of the statement's names)

Value Functions

• comp and len: LLM picks one of seven bins on a $\log_2$ scale; the goal is priced at the bin's geometric center. For len, the estimate is 0.2× the bin center (deliberate underestimation to encourage exploration of shorter proofs).
• imp: Constant prior of 4 references (25th percentile of calibration impurity)
• Value function calls comprise only 0.89% of LEVER's spend

---

Empirical Validation / Results

Setup

• Model: DeepSeek-V4-Flash-0731 for all LLM calls (LEVER and baselines)
• Data: PutnamBench problems ranked 51–150 by difficulty (80 evaluation + 20 calibration)
• Budget: $3 per problem for cost optimization; $4.5 for quality optimization
• Cache rate: Fixed at 90% for fair comparison

Result 1: Computational Cost Optimization

Table 1: Cost of proof search at a $3 budget per problem ($N = 80$).

Key findings:

• LEVER solves 96.3% vs. 80.0% for NearAI, at 34% lower cost
• LEVER reads less than half the input tokens (17.9M vs. 42.0M) due to local contexts
• The advantage holds at almost every budget from $0.25 upward

Result 2: Proof Quality Optimization

Topical Impurity (Figure 5, left; Table 2):

• LEVER at λ=0.1 achieves 42% impurity reduction vs. 33% for + Refactor, at $1.85 vs. $2.88 (about two-thirds the cost)
• LEVER is more reliable: per-problem reduction std. dev. is 32 points vs. 101 for + Refactor (whose rewrites can backfire badly—e.g., putnam 2007 a2 went from 29 to 132 out-of-subject references)
• • Instruct makes proofs less pure (11% worse), showing the agent loses the search objective in a long session

Proof Length (Figure 5, right; Table 2):

• LEVER approaches + Refactor (21% vs. 31% reduction) but at higher cost ($2.59 vs. $1.83)
• Cross-metric effects: Shortening proofs also reduces impurity (likely because impure references are removed for free), but optimizing impurity alone makes proofs longer (+10%)

Quality–Cost Trade-offs

LEVER traces explicit trade-off curves: as λ rises, quality improves and cost increases. Any fixed policy (baselines) admits only single points in this space.

---

Theoretical and Practical Implications

Theoretical Contributions

1. Objective-guided search over partial proofs: A unified algorithm that optimizes computation and proof quality during search, using values that combine realized costs with predictions for open subgoals, propagated through an AND/OR graph.

2. Exactness under exact priors: With exact priors, the backed-up values are exact—$V(n)$ is the cost of the cheapest solution subgraph rooted at $n$, and $\dot{V}(n) = \infty$ exactly when none exists. The authors share a formally verified proof in Lean (Appendix D).

3. Stochastic expansion handling: Unlike classical AO* (which assumes deterministic expansion), LEVER handles stochastic LLM expansions via the redraw margin δ and Bayesian prior updates.

Practical Implications

1. Cheaper and stronger proof search: The 34% cost reduction and 96.3% solve rate demonstrate that decomposition with local contexts is fundamentally more efficient than single-conversation agents.

2. Search-time optimization beats post-hoc refactoring for strategy-dependent metrics: Topical impurity depends on the proof strategy chosen at the start; refactoring cannot easily change the argument, while LEVER can.

3. Tunable quality–cost frontier: The single weight λ converts between metrics, letting users choose how much a better proof is worth—a capability no existing system provides.

4. Shared subgoal handling: When a subgoal is shared by several decompositions, paying once makes finding the cheapest solution subgraph NP-hard (Sahni, 1974); LEVER charges each shared subgoal to a single owner (Appendix A).

---

Conclusion

LEVER treats correctness as a constraint and makes the objective over correct proofs programmable. Key takeaways:

• Performance: 34% cheaper than a strong single-conversation agent while solving more problems (96% vs. 80%)
• Quality: 42% impurity reduction vs. 33% for post-hoc refactoring, at two-thirds the cost; approaches refactoring on length
• Tunability: A single weight trades quality against cost, letting users choose how much a better proof is worth
• Generalization: The same mechanism optimizes computational cost, proof length, topical impurity, and weighted combinations thereof

Future directions include theoretical analysis of noisy value functions (the current update of Equation 1 and margin δ are heuristic), and extending the framework to other proof-quality metrics and domains beyond Lean.

---

Note on limitations: The impurity metric is acknowledged as a proxy for mathematical purity, since true purity requires human judgment about a theorem's content. The evaluation set (PutnamBench ranks 51–150) is a tractable but hard slice, which may introduce selection bias.