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
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 ).
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).
Figure 3: Two proofs of one lemma: the unit triangle has area 21 . 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 4
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 λ=0,0.01,0.1 for impurity and λ=0,10−4,10−3 for length, light to dark; λ=0 is Lever run with its 3budgetandroutingtodirectattempts(§5.1);the\lambda>0runshave4.5 and no routing. A run that fails or exceeds 4.5isscoredasNearAI’sproofat4.5; + Refactor is also charged for NearAI’s run. Error bars: ±1 standard error over problems.
m=imp
m=len
Method
Δ Impurity
Δ Length
Δ Length
Δ Impurity
Lever ( λ=0 )
+1%
+4%
+4%
+1%
Lever mλ1
−15%
+8%
−5%
+3%
Lever mλ2
−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. λ1,λ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
σ
ρ
n
δ
comp
LLM, 7 bins
log2 , 0.016–0.512
0.615
1.08
0.33
1.85
len
LLM, 7 bins
log2 , 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. ρ : prediction error on held-out calibration goals (log scale for comp and len , references for imp ); σ : variation between draws of the same goal; n=σ2/ρ2 : the prediction’s weight in draws; δ : 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:everymethodatthesamerate.Ownratepercall:eachmethodatitsper−callratefromTable5.Actual:everycallatthecachehitsitgot.Undereachpricing,the3 rule of Table 1 is applied to each run’s calls in order.
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.