LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs

Nihal Jain; Shuangjie Yao; Begum Cicekdag; Zhuo Zhang; Suman Jana

cs.AIOct 8, 2026

LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs

Authors: Nihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang, Suman Jana

Organizations: Columbia University

Abstract

Mathematicians value proofs for more than correctness: among correct proofs, simplicity, purity and the computational cost of finding them vary widely. Yet LLM-powered theorem provers largely search for any correct proof, and improve its quality only after it is found. We propose LEVER, a proof search algorithm that makes the objective over correct proofs programmable and optimizes it during search. LEVER scores partial proofs over an AND/OR proof graph, combining realized objective values with predictions for open subgoals, so the objective guides search before a proof is complete. The same mechanism optimizes computational cost, proof length, topical impurity, and even their weighted combinations, while the Lean kernel enforces correctness. On PutnamBench in Lean 4, under matched budgets, LEVER costs 34% less than a strong single-conversation agent while raising the solve rate from 80% to 96%. On reducing topical impurity, i.e., how far a proof strays from its theorem's subject, it improves over post-hoc refactoring (42% reduction against 33%) at two-thirds of the cost and more reliably; on proof length, the metric refactoring is built for, it approaches refactoring. Varying the objective's weights traces a quality-cost trade-off curve, so the user can choose how much a better proof is worth. Overall, LEVER is a performant, cost-efficient and tunable proof search algorithm for navigating the space of correct proofs.

Figures & tables

Panel of Figure 1 — Figure 1: An AND/OR graph. OR nodes (goals) are circles, AND nodes (decompositions) are squares; a goal may have different decompositions (here Euclid’s and Fermat’s). Double border AND nodes are proved directly; dashed AND nodes are priors (§ 3.3 ).

Panel of Figure 2 — Figure 2: One iteration of Lever . Grey numbers are edge costs and black numbers node values; later panels label only what their step changes. At the root’s second subgoal the prior beats the realized attempt, so that interior goal is expanded again; the new attempt’s value then passes up to the root, updating the priors on the way (Eq. 1 , $n=1$ ). The first attempt stays in the graph, paid for but no longer chosen (grey).

Panel of Figure 3 — Figure 3: Two proofs of one lemma: the unit triangle has area $\tfrac{1}{2}$ . The statement is about measure and convex hulls. Plan 1 slices the triangle and integrates. Its calculus references, such as intervalIntegral.integral_sub , are impure (underlined red): the statement never calls for integrals. Plan 2 halves the unit square. It argues in measure theory, and a reference such as MeasureTheory.measure_union_add_inter is pure (underlined green). Over the lemma and the helpers it uses, the metric flags 25 references in Plan 1’s proof and 6 in Plan 2’s. Excerpts from compiled proofs; dots mark elisions.

Figure 5: Proof quality against computation cost. Mean reduction of each metric relative to NearAI’s proof of the same problem, against mean cost per problem, for topical impurity (left) and proof length (right), on the same

20

problems. Lever ’s points are

\lambda=0,0.01,0.1

for impurity and

\lambda=0,10^{-4},10^{-3}

for length, light to dark;

\lambda=0

is Lever run with its

3 budget and routing to direct attempts (§ 5.1 ); the

\lambda>0

runs have

4.5 and no routing. A run that fails or exceeds

4.5 is scored as NearAI’s proof at

4.5; + Refactor is also charged for NearAI’s run. Error bars:

\pm 1

standard error over problems.

	$m=\texttt{imp}$		$m=\texttt{len}$
Method	$\Delta$ Impurity	$\Delta$ Length	$\Delta$ Length	$\Delta$ Impurity
Lever ( $\lambda{=}0$ )	$+1\%$	$+4\%$	$+4\%$	$+1\%$
Lever ${}^{\lambda_{1}}_{m}$	$-15\%$	$+8\%$	$-5\%$	$+3\%$
Lever ${}^{\lambda_{2}}_{m}$	$-42\%$	$+10\%$	$-21\%$	$-18\%$

Table 2: Optimizing one metric, measured on both. Mean change of topical impurity and of proof length relative to NearAI’s proof of the same problem; negative is better.

\lambda_{1},\lambda_{2}

are

0.01,0.1

when optimizing impurity and

10^{-4},10^{-3}

when optimizing length. A run that fails or exceeds $4.5 is scored as NearAI’s proof.

Appendix figures & tables5 assets

Supplementary material from the paper’s appendix.

Appendix

Ranks	Problems	Wall-clock, all attempts (h)
1–50	50	9.6 (max 132)
51–150	100	1.5 (max 33)
151–672	520	0.3 (max 9)

Appendix

Table 3: PutnamBench by the cost of the published NearAI run. Wall-clock: median and maximum over problems of the time summed over all attempts.

Metric	Prediction	Scale	$\sigma$	$\rho$	$n$	$\delta$
comp	LLM, 7 bins	$\log_{2}$ , $0.016–$ 0.512	0.615	1.08	0.33	1.85
len	LLM, 7 bins	$\log_{2}$ , 512–16,384 tokens	0.408	0.72	0.32	1.50
imp	constant ( $=4$ )	linear	6.79	31.2	0.05	1.72

Appendix

Table 4: Value functions.

\rho

: prediction error on held-out calibration goals (log scale for comp and len , references for imp );

\sigma

: variation between draws of the same goal;

n=\sigma^{2}/\rho^{2}

: the prediction’s weight in draws;

\delta

: the factor a redraw must promise.

Method	Per call	Per token
NearAI	93.7%	96.2%
Lever	86.2%	91.4%

Appendix

Table 5: Observed cache-hit rates on the

80

evaluation problems. Per call: the mean, over calls, of the fraction of each prompt read from cache. Per token: cached input tokens over all input tokens.

	NearAI		Lever
Pricing	Solved	Cost ($)	Solved	Cost ($)
90%, common (Table 1 )	0.800	1.44	0.963	0.95
93%, common	0.825	1.28	0.963	0.85
95%, common	0.875	1.15	0.963	0.78
97%, common	0.888	1.00	0.963	0.71
Own rate per call	0.850	1.24	0.950	1.09

Appendix

Table 6: Table 1 under other pricings.

N=80

, budget

3. Common: every method at the same rate. Own rate per call: each method at its per-call rate from Table 5 . Actual: every call at the cache hits it got. Under each pricing, the

3 rule of Table 1 is applied to each run’s calls in order.

Panel of Figure 6 — Figure 6: Lever on putnam_1972_a3 . Edge labels: what each attempt cost. Subgoal labels: the value function’s price. The first decomposition (grey) is rejected before any of its subgoals is attempted.

Explore similar work

Jun 3, 2026cs.CL

Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean

Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proof attempts, and use compiler feedback to guide search. However, they can be prohibitively expensive, often spending substantial compute on attempts that ultimately fail. In this work, we address this problem with an action routing agent that consists of a data plane and a control plane. The data plane generates natural-language lemma decompositions, formalizes them in Lean, and samples proof attempts for the resulting theorem and lemma targets. The control plane observes previous failed Lean attempts, estimates both the likelihood of success and the cost of another attempt, and decides whether to continue proving the current target or restart from a new breakdown. On a subset of PutnamBench, our agent decreases the cost by 28.9% over a fixed-step baseline on average, preserving performance while using substantially less compute. These results suggest that failed Lean trajectories provide actionable signals for cost-aware resource allocation in agentic theorem proving.

Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck +1

1ETH Zurich, Switzerland.

Automated Theorem Proving Lean Theorem Proving

Ask PDF

Jun 10, 2026cs.AI

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both supervised fine-tuning (SFT) and sampling expensive. We introduce Pythagoras-Prover, a compute-efficient open-source family of Lean theorem provers built for practical compute budgets. The family spans two generation paradigms: autoregressive models at 4B and 32B parameters, and a first proof-of-concept diffusion-based prover (4B) that iteratively refines Lean proofs at inference time. For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT, so models acquire proof skills progressively from shorter, simpler proofs to longer, harder ones. During SFT, a dynamic proof-reasoning filtering scheme preserves informative proof traces while keeping each instance within an 8k-token context budget. We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements, populated via self-distillation for extra training signal without formally verifying every mutated instance. By perturbing known problems while preserving their formal character, ALF reduces reliance on any statement's surface form. Empirically, Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test (86.1% vs 82.4%) with ~167x fewer parameters, while Pythagoras-Prover-32B sets the open-source state of the art at 93.0% on MiniF2F-Test and solves 93 of 672 PutnamBench problems. We release MiniF2F-ALF, an ALF-mutated contamination-sensitive benchmark on which every evaluated model loses accuracy; here our 32B remains strongest and our 4B matches the prior state of the art, Goedel-Prover-V2-32B.

Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian +5

Imperial College London · University of Edinburgh · Nanyang Technological University +1

Automated Theorem Proving Efficient Language Model Training Lean Theorem Proving

Ask PDF

Oct 8, 2026cs.LG

NanoProof: Open and Efficient Automated Theorem Proving in Lean 4

We introduce NanoProof, to our knowledge the first factorized execution-guided theorem prover in Lean 4 whose training data, extraction tooling, training pipeline, and weights are all released, making it end-to-end reproducible using open-source resources. To this end, we build and release a dataset of structured proof trees, as well as a tool for programmatic interaction and data extraction within the Lean 4 formal verifier. To support sustainable research, we focus on compute efficiency to facilitate accessible training and evaluation. NanoProof achieves 50.8% pass@16 on MiniF2F-Test, exceeding the two closest systems of its class, HyperTree Proof Search and ABEL, at roughly 90x and 7x less compute, and using more than four orders of magnitude less compute than AlphaProof. Stronger open-weight provers exist, but they are fine-tuned from large pretrained language models and release neither training data nor pipeline; NanoProof shows that the factorized execution-guided class of provers can be rebuilt from scratch with modest resources.

Matěj Kripner, Milan Straka

Institute of Formal and Applied Linguistics, Faculty of Mathematics and Physics, Charles University Prague, Czech Republic

Automated Theorem Proving Lean Theorem Proving

Ask PDF