LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs
Nihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang, Suman Jana
cs.AI
Oct 8, 2026 · v1
TL;DR
LLM agents decompose goals into Lean 4 subgoal files checked by the Lean kernel, evaluated on PutnamBench; includes a Lean-verified proof of an algorithmic property.
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.
Problem
LLM-based theorem provers usually search for any correct proof and improve its quality only afterwards through post-hoc refactoring. The cost of the search and properties of the proof such as length or topical impurity are not optimized while the search runs.
Approach
LEVER represents partial proofs as an AND/OR graph in which goals are OR nodes and decompositions are AND nodes. Each partial proof is scored by combining the realized objective values of solved parts with LLM-predicted values for open subgoals, and the best-scoring partial proof is expanded. Each expansion is an LLM agent conversation in a Lean workspace, with tools for compilation and Mathlib retrieval. The Lean kernel checks every decomposition and the assembled final proof.
Results
On 80 hard PutnamBench problems in Lean 4 with a $3 budget, LEVER solves 96.3% of problems against 80.0% for the NearAI agent, at 34% lower cost. Optimizing for topical impurity reduces impurity by 42%, against 33% for post-hoc refactoring, at two-thirds of the cost. On proof length, LEVER comes close to refactoring.
| Method | Solved | Cost ($) | Tokens In (M) | Tokens Out (M) |
|---|
| NearAI | 0.800 | 1.44 | 42.0 | 0.36 |
| Lever | 0.963 | 0.95 | 17.9 | 0.62 |
Cost of proof search at a $3 budget (90% common cache rate)
