Paper deep dive
LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs
Nihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang, Suman Jana
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%
Last extracted: 10/10/2026, 2:36:08 AM
Summary
The paper introduces LEVER, an adaptive, cost-aware proof search algorithm for LLM-powered theorem provers that operates over AND/OR graphs. Unlike traditional methods that search for any correct proof and optimize quality post-hoc, LEVER optimizes programmable objectives (computational cost, proof length, topical impurity) during the search process by scoring partial proofs. Evaluated on PutnamBench in Lean 4, LEVER reduces computational costs by 34% and increases solve rates from 80% to 96% compared to strong single-conversation agents, while also outperforming post-hoc refactoring in reducing topical impurity.
Entities (10)
Relation Signals (10)
Lean Kernel → enforces → δ-correctness
confidence 95% · while the Lean kernel enforces correctness.
LEVER → increasessolverateto → 96%
confidence 95% · raising the solve rate from 80% to 96%
LEVER → optimizes → Computational Cost
confidence 95% · The same mechanism optimizes computational cost
LEVER → optimizes → Proof Length
confidence 95% · The same mechanism optimizes ... proof length
LEVER → optimizes → Topical Impurity
confidence 95% · The same mechanism optimizes ... topical impurity
LEVER → reducescostby → 34%
confidence 95% · LEVER costs 34% less than a strong single-conversation agent
LEVER → runson → PutnamBench
confidence 95% · On PutnamBench in Lean 4... LEVER costs 34% less
LEVER → uses → AND/OR Graph
confidence 95% · LEVER scores partial proofs over an AND/OR proof graph
LEVER → outperforms → Post-hoc Refactoring
confidence 90% · it improves over post-hoc refactoring (42% reduction against 33%) at two-thirds of the cost
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2610.11862v1
- Canonical: https://arxiv.org/abs/2610.11862v1
Trouble viewing inline? Open PDF directly →
Full Text
92,317 characters extracted from source content.
Expand or collapse full text
Lever: Adaptive Cost-Aware Proof Search Over AND/OR Graphs Nihal Jain Shuangjie Yao Begum Cicekdag Zhuo Zhang Suman Jana Affiliation: Columbia University Affiliation: nihal.jain, sy3437, bc2975, z3474, sj2754@columbia.edu 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%34\% less than a strong single-conversation agent while raising the solve rate from 80%80\% to 96%96\%. On reducing topical impurity, i.e., how far a proof strays from its theorem’s subject, it improves over post-hoc refactoring (42%42\% reduction against 33%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. 1 Introduction Mathematicians have long valued proofs for more than their correctness. A proof may be shorter, more elementary, or reveal structure that another proof obscures. The four-color theorem, for example, was proved in 1976 and formally verified decades later, yet a substantially different proof fifty years on exposed new structure in planar graphs and led to a near-linear-time coloring algorithm (Appel and Haken, 1977; Gonthier, 2008; Inoue et al., 2026). More broadly, the mathematical literature has debated the importance of characteristics like purity, simplicity and explanation (Steiner, 1978; Detlefsen and Arana, 2011; Thiele, 2003; Tao, 2007). The challenge is, therefore, not only to find a correct proof, but to choose among many. This observation is crucial in the context of LLM-powered theorem provers that may generate correct proofs differing sharply in the computation needed to find them, their length, and the machinery they invoke. Yet current systems largely separate these concerns: proof search returns any verified proof (NearAI, 2026; MistralAI, 2026; Rögnvaldsson et al., 2026), sometimes with mechanisms to reduce inference cost, and proof quality is improved only afterwards through post-hoc refactoring (Ahuja et al., 2024; Lu et al., 2026; Fu et al., 2026). We take a different view: the objective over the space of proofs should be programmable, with correctness as a constraint. Optimizing such objectives during search can be both cheaper and more effective than optimizing it afterwards: a post-hoc method revisits a proof already paid for, and possibly inherits a trajectory (mathematical argument) chosen for a different objective. The key idea of Lever is to score a proof before it is finished. A partial proof has some goals proved and others still open. Lever scores it as the realized scored of the proved parts plus a predicted value for each open goal; at any time only the partial proof with the best score is expanded, so the objective steers search from the beginning rather than after the task is complete. We support this mechanism by representing partial proofs as an AND/OR graph: a theorem or a goal (OR node) is proved by any one of its alternative decompositions (AND nodes), and an argument needs all of its subgoals (OR nodes). We demonstrate that objectives such as computational cost, proof length or topical impurity, or a weighted sum of them compose over the proof graphs, allowing us to optimize them. In this process, correctness is never compromised: the Lean kernel checks every decomposition, and the assembled final proof. On PutnamBench (Tsoukalas et al., 2024), with the same model and budget allocation as a strong agent that generates proofs in a single conversation, Lever raises the solve rate under a $3 budget from 80.0%80.0\% to 96.3%96.3\% while reducing average cost from $1.44 to $0.95, a 34%34\% reduction. The gain comes from keeping contexts local: Lever reads less than half the input tokens of the single-conversation agent. We then optimize the proof itself, for length and topical impurity, which we operationalize following work on purity of method (Detlefsen and Arana, 2011; Martinot, 2024): a proof accumulates impurity when it depends on results outside the subject of its theorem. So, length is often amenable to local compression, whereas purity can depend on the argument chosen at the start. Consistent with this, Lever approaches post-hoc refactoring on length, but outperforms both refactoring and direct instruction on impurity, at two-thirds of refactoring’s cost. Finally, varying the weight on quality metrics traces explicit quality–cost trade-off curves. This turns theorem proving from searching for any verified proof into searching for a verified proof under a user-specified objective, using the same search algorithm. Our contributions are: • Objective-guided search over partial proofs. A unified algorithm to optimize computation and proof quality during search by using values that combine realized costs with predictions for open subgoals, propagated through an AND/OR graph; • Cheaper and stronger proof search. On PutnamBench, 34%34\% lower cost and a 96.3%96.3\% solve rate, against 80.0%80.0\% for a strong single-conversation agent under a matched budget; • Proof quality during construction. Search-time optimization outperforms refactoring on topical impurity at two-thirds of its cost, approaches it on length, and admits explicit quality–cost trade-off curves. 2 Related Work LLMs for theorem proving. LLM provers range from tactic generators inside tree search (Polu and Sutskever, 2020; Yang et al., 2023; Xin et al., 2024; Xin et al., 2025) to whole-proof generators refined with compiler feedback (First et al., 2023; Wang et al., 2025; Lin et al., 2025). Decomposition has since become central: an informal draft becomes a formal sketch whose subgoals are proved separately (Jiang et al., 2023; Wang et al., 2024a; Dong et al., 2024; Ren et al., 2025), and agentic systems such as HILBERT (Varambally et al., 2026) and Goedel-Architect (Chung et al., 2026) complete these, while others learn from millions of attempts (Chen et al., 2025; Achim et al., 2025; Hubert et al., 2025; Tsoukalas et al., 2026); LEAP (Kung et al., 2026) maintains an AND/OR graph but explores it depth-first; all these systems search for any correct proof. On cost, Rögnvaldsson et al. (2026) decide when to restart from a new decomposition, and Quarry (Zhang et al., 2026) ranks decompositions by predicted hammer solvability; in either case simple linear models with limited features from Lean structures make predictions. Proof quality is improved by refactoring a finished proof (Ahuja et al., 2024; Gu et al., 2025; Lu et al., 2026; Fu et al., 2026). Lever instead lets an explicit objective over cost and proof quality steer the search using LLM-based value functions. Value-guided search. AO∗ finds the cheapest solution graph of an AND/OR graph under an admissible heuristic (Martelli and Montanari, 1973; Nilsson, 2014), with extensions to cyclic graphs (Hansen and Zilberstein, 2001) and games (Allis et al., 1994). Learned values replaced hand-written heuristics in Monte Carlo tree search (Kocsis and Szepesvári, 2006; Silver et al., 2016; Silver et al., 2018; Guez et al., 2018) and HyperTree Proof Search (Lample et al., 2022); closest in spirit, Retro* (Chen et al., 2020) learns the cost-to-go of AND/OR trees for retrosynthesis. LLM search over partial solutions (Yao et al., 2023; Hao et al., 2023; Zhou et al., 2024; Snell et al., 2024) is typically guided by self-evaluation or process rewards that score correctness (Lightman et al., 2023; Wang et al., 2024b). Lever differs in three ways: its expansions are stochastic, so a goal can be redrawn; its priors learn from the draws already paid for; and its objective composes the remaining computational cost, the concern of rational metareasoning and costly search (Russell and Wefald, 1991; Sabbata et al., 2025; Weitzman, 1979), with arbitrary proof metrics. 3 Lever 3.1 Background infinitely many primespriorEuclidFermatN>1N>1p|Np Np≠pip≠ p_i(Fm,Fn)=1(F_m,F_n)=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). AND/OR graphs. An AND/OR graph is a bipartite DAG G=(VOR⊔VAND,E)G=(V_OR V_AND,E) whose edges alternate between OR and AND nodes. An OR node is a goal, a theorem or lemma to prove; an AND node is a decomposition of a goal into subgoals, whose validity an oracle (here the Lean kernel) checks. The root OR node r is the theorem to prove. An OR node is solved if any child is, and an AND node if all its children are; an AND node with no children, a goal proved without new lemmas, is solved. Solution subgraphs. A proof or solution subgraph is a subgraph S⊆GS G such that: (i) r∈Sr∈ S; (i) for each OR node in S, exactly one AND child is picked; (i) for every AND node in S, all its children are picked; (iv) the leaves in S are solved. Then each S maps to a unique proof written in Lean. Costs. Every edge carries a nonnegative cost c. A decomposition needs to pay for all its subgoals whereas a goal takes the cheapest way to prove it, so values back up as: V(n)=∑d∈ch(n)c(n,d)+V(d)(n∈VAND),V(n)=mind∈ch(n)c(n,d)+V(d)(n∈VOR),V(n)= _d (n)c(n,d)+V(d) (n∈ V_AND), V(n)= _d (n)c(n,d)+V(d) (n∈ V_OR), with V=0V=0 at a solved leaf and V=∞V=∞ at a false goal. V(r)V(r) is then the cost of the cheapest solution subgraph, and the argmin at each OR node reconstructs it. 3.2 Proof Search The problem of proof search can be modeled as an MDP with the following description: • States. The graph built so far, with statuses and edge costs; fully observed. • Actions. OR node(s) to expand, i.e., which goals to decompose next or STOP if nothing to expand. • Transition. Transformation of the graph that adds decompositions (and the corresponding subgoals) to the graph; transitions are stochastic: expanding the same goal twice may not result in the same resulting graph. • Reward. Score of −st-s_t for the expansions at time step t, and −V(r)-V(r) at termination (−∞-∞ if unsolved). Episodes end when the policy decides to STOP or if the budget is exhausted. The objective of proof search is to maximize the sum of rewards at the end of the episode or minimize the cost objective: V(r)+∑tstV(r)+ _ts_t. At any step, the spend so far is sunk and cannot be changed, so a good policy minimizes the cost-to-go: the expected remaining spend plus V(r)V(r). 3.3 Adaptive Proof Search with Lever Algorithm 1 shows how Lever searches for proofs. The AO∗ algorithm (Nilsson, 2014) assumes a deterministic expansion function, but here the expander is an LLM: expanding a goal returns one decomposition drawn from an effectively unbounded set, and drawing again may return a cheaper one. Hence a goal that already has children can still be worth expanding, i.e., any interior OR node is a candidate. To decide when, every OR node g carries one additional child, its prior: an AND node p that is never expanded, holding an estimate V~(g) V(g) of the cost of finishing g with a fresh decomposition. Each iteration has three steps (Figure 2): Algorithm 1 Lever. Each iteration selects goals along the current best solution subgraph, expands them, attaches a prior to each new subgoal, and backpropagates values, until selection returns nothing or the budget is spent. Input: root r, budget B 1 Prior(r) 2 while spent<Bspent<B do 3 T←T← Select(r) 4 if T=∅T= then break 5 foreach g∈Tg∈ T do 6 D←D← Expand(g) 7 foreach d∈Dd∈ D do Prior(d) 8 Backpropagate(g) 9 return the best solution subgraph of r 23414100713selectmin(12,14) (12,14)selectmin(17,7) (17,7)1Selectionfollow the min down to anopen goal or a prior152Expansion & scoringdraw a new attempt;price its new subgoals1113.4966.63Backpropagation & updatesum at AND, min at OR;update the priors 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=1n=1). The first attempt stays in the graph, paid for but no longer chosen (grey). 1. Selection. Descend from the root along the current best solution subgraph, taking the argmin child at an OR node and all children at an AND node. When the argmin is a prior, its goal is expanded; for a goal that already has children, this is a redraw. Values are noisy, so a small gap is no evidence that a fresh draw would be cheaper: a redraw must beat the incumbent by a factor δ. When selection returns nothing, the policy STOPs. 2. Expansion. An LLM expands each selected goal: it proposes a new decomposition (an AND node), the oracle checks it, and each subgoal it introduces is attached as a new OR node. The edge from the goal to the decomposition is scored with the cost of the expansion, and each new subgoal receives a prior from the value function (§4.4). Edges from a decomposition to its subgoals cost nothing: the subgoals are simply parsed from the compiled proof. 3. Backpropagation. New costs pass upward through the recursion of §3.1, updating every prior on the path. We model the log cost of a fresh decomposition of g as normal around an unknown mean μg _g with spread σ (draws of the same goal differ) and the value function’s prediction V0(g)V_0(g) (§4.4) as off from μg _g by ρ. After k decompositions with costs v1,…,vkv_1,…,v_k, the posterior μg _g is normal with: μ^g=nlogV0(g)+∑i=1klogvin+k,n=σ2/ρ2, μ_g\;=\; n V_0(g)+ _i=1^k v_in+k, n=σ^2/ρ^2, (1) so the prior estimate is worth n draws and each realized draw, one. The value estimate is the posterior geometric mean, V~(g)=exp(μ^g) V(g)= ( μ_g). Realized costs thus correct the value function’s errors: this is how the search learns from what it has paid for. A failed attempt leaves no cost to learn from, and instead raises the estimate by one σ. Metrics on a linear scale use the same form without logarithm. Objective. The steps above hold for any cost that composes over the algebra of §3.1, which metrics such as proof length do. The spend term ∑tst _ts_t in the MDP objective of §3.2 does not: it accumulates over the whole search, including draws the final proof never uses. We therefore split it into what has been spent (sunk; cannot be optimized) and what remains (can be optimized). The remaining part does compose over the graph, and we call it Vcomp(n)V_ comp(n): the computational cost still needed to finish n, where realized edges add nothing and open goals add their prior’s estimate. With this adjustment, any metric m, backed up as VmV_m with edge costs cmc_m, can be balanced against computational cost at a price of λm _m dollars per unit: C(n)=Vcomp(n)+∑mλmVm(n).C(n)\;=\;V_ comp(n)+ _m _mV_m(n). With every λm=0 _m=0, Lever minimizes computational cost alone. Exactness under exact priors. With exact priors, the backed-up values are exact: for any nonnegative cost that adds along edges, V(n)V(n) is the cost of the cheapest solution subgraph rooted at n (counting a subgoal once per use), and V(n)=∞V(n)=∞ exactly when none exists. We also share a formally verified proof of this in Lean (Appendix D). Real value functions are noisy, which the update of Equation 1 and the margin δ account for; their theoretical analysis is left for future work. When a subgoal is shared by several decompositions, paying for it once instead makes the cheapest solution subgraph NP-hard to find in general (Sahni, 1974); Lever instead charges each shared subgoal to a single owner (Appendix A). 4 Implementing Lever with Lean 4.1 Setup Model and Pricing. We use DeepSeek-V4-Flash-0731 (DeepSeek-AI et al., 2026) for every LLM call, in Lever and in all baselines, to match the baseline’s original setting. We price tokens at the official rates of $0.22, $0.007 and $0.66 per million input, cached input and output tokens (DeepSeek-AI, 2026). Cost therefore depends heavily on the cache-hit rate. Served through multiple providers, API calls experience mean hit rate per call at 93.7% for NearAI (2026), whose single long conversation re-reads its own history, and 86.2% for Lever, which starts many shorter conversations. To compare the searches rather than the caching, we fixed one 90% rate, between the two, before the evaluation runs. All costs in this paper are re-priced at this rate, and a problem counts as solved within a budget B only if its re-priced cost is at most B; Appendix C.3 reports the observed costs. Data. We use PutnamBench (Tsoukalas et al., 2024), originally containing 672672 competition problems formalized in Lean 4 (v4.31.0). Most are easy for a strong agent, while the hardest can take days of repeated attempts, too long for controlled comparisons. Hence, we rank the problems by what the published run of NearAI (2026) spent to solve them and take ranks 5151–150150, a slice that is hard but tractable; Appendix C.1 gives the full procedure and its biases. 2020 of these calibrate the value functions (§4.4), and the other 8080 form the evaluation set (§ 5). 4.2 Agentic System Design We discuss salient aspects of Lever’s agent for goal expansion, leaving detailed descriptions in Appendix A. Expanding a goal. Each expansion is one conversation of an LLM agent (Yao et al., 2022) with a Lean workspace, with tools for Lean compilation (Santos et al., 2025), Mathlib retrieval (Lu et al., 2025), Python, and file I/O; it ends by submitting a file or reporting the goal false. To decompose a goal, the agent writes a Lean proof that relies on open subgoals; small lemmas are proved in place and larger ones are left open. Each open helper becomes a subgoal, to be closed in a future iteration. It annotates dependencies among open subgoals with the sorry_using tactic of LeanArchitect (Zhu et al., 2026; Chung et al., 2026), so that subgoals can share work. To prove a goal directly, the agent writes a complete proof with no open subgoals; §5 states when this is enforced. Context. Before the search, a planner writes an informal proof of the problem, following Varambally et al. (2026) and Chung et al. (2026). Every expansion carries this plan in its system prompt, and the planner’s cost is included in every cost we report for Lever. A subgoal’s conversation starts from its parent’s compacted output, or its full transcript if short, so the agent knows why the subgoal was introduced without carrying its parent’s work (Appendix A). Every LLM inference call is made with 3232K completion tokens at temperature 1.01.0; planning with high-effort reasoning and expansion with low-effort reasoning. Disproofs and soundness. The agent may report a goal false, with an informal reason (formal disproofs as in Lin et al. (2025) are not integrated for simplicity; these can wander into their own long trajectories). This ends the decomposition, and values are updated as in §3.3. When the root is solved, the solution subgraph is assembled into one Lean file and checked by the kernel. A problem counts as solved only if this file compiles using only the standard axioms, without sorry, admit, axiom or native_decide. Plan 1: slice the triangle and integrate ⬇ lemma std_tri_volume : (MeasureTheory.volume (convexHull ℝR ⋯·s)).toReal = 1 / 2 := by . . . rw [← intervalIntegral.integral_of_le ⋯·s] rw [intervalIntegral.integral_sub] ⋅· rw [intervalIntegral.integral_const, ⋯·s] ⋅· exact Continuous.intervalIntegrable ⋯·s Plan 2: halve the unit square ⬇ lemma std_tri_volume : (MeasureTheory.volume (convexHull ℝR ⋯·s)).toReal = 1 / 2 := by . . . have hvol_union : MeasureTheory.volume (stdTri ∪ stdTri') = ⋯·s := by have hia := MeasureTheory.measure_union_add_inter ⋯·s Figure 3: Two proofs of one lemma: the unit triangle has area 12 12. 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. 4.3 Cost Objectives Correctness and computational cost. Correctness is enforced as a constraint: an unsolved goal costs ∞, so every objective is minimized over proofs that Lean type-checks. Computational cost, comp, is the dollars spent on LLM calls at the rates of §4.1. Spend already incurred cannot be recovered, so the search never optimizes it: each decision minimizes the remaining cost of finishing the proof, as estimated by the value function (§4.4), and every expansion replaces part of that estimate with what it actually cost (§3.3). Proof length. We count the Lean tokens (len) a proof adds to its theorem statement, helper lemmas and definitions included and comments excluded, tokenized as in Gu et al. (2025). It is easy to measure but also easy to game, e.g., a goal closed by one call to nlinarith is short while saying nothing about the mathematics behind it. Topical impurity. (imp) instead measures the source of content in a proof. A proof is pure when it uses only what its theorem is about (Detlefsen and Arana, 2011). Purity is not computable in general, since a human must decide what a theorem’s content is (Martinot, 2024), so we read the content off Mathlib’s structure (Community Mathlib, 2020). Every library name has a namespace and a directory, e.g., ZMod.wilsons_lemma is about ZMod and lives in Mathlib/NumberTheory. A theorem’s subject is the namespaces and directories of the names its statement uses. A referenced library theorem is impure when it falls outside the subject on both accounts; a generic lemma with no namespace, such as mul_pos, is impure only if it also lies outside a fixed set of infrastructure directories (e.g., Mathlib/Data/Nat) that proofs of every topic use. Overall, we measure impurity as the number of impure references. See Figure 3 for an illustration of pure and impure proofs. We note here that this is a proxy for measuring mathematical (im)purity; further discussion and limitations of this metric are in Appendix B. 4.4 Value Functions Predicting comp and len. For comp and len, an LLM reads the open goal and picks one of seven bins on a log2 _2 scale ($0.016–$0.512 and 512–16,384 Lean tokens), and the goal is priced at its bin’s geometric center. Further, for len, the estimate is 0.20.2 times the bin’s center, deliberately underestimating length so that shorter proofs get explored. The prompt carries 4040 in-context examples from offline runs on the calibration problems. Using an LLM as a value function prior is inexpensive: these calls make up only 0.89%0.89\% of Lever’s spend, and are always included in the reported costs. Predicting impurity. Impurity has a real floor, since a proof can cite nothing outside its subject, so the natural estimate for an open goal is 00. In practice this made search unstable: every open goal looked pure, so redrawing always beat keeping a decomposition, and graphs grew huge. We instead score every open goal at a constant 44 references, the 2525th percentile of impurity over calibration goals. Calibration. On the calibration problems only, we measure ρ, the value function’s error against realized values, and σ, the spread of a goal’s realized value across repeated draws: in log space for comp and len, and in references for imp. For comp and len, the redraw margin is one spread, δ=eσδ=e^σ. Appendix C.2 documents every constant and how it is measured. 5 Experiments We focus on two main questions: First, can Lever optimize computational costs during proof search (§ 5.1)? Second, how effective is Lever at recovering high quality proofs during search (§ 5.2)? All runs share the setup of § 4.1: one model, one Lean version and one price table, for Lever and every baseline alike. 5.1 Optimizing Computational Cost Baseline. Our main baseline is the open-source agent of NearAI (2026), the top entry on the PutnamBench leaderboard at the time of writing. It is a single-conversation agent: one conversation holds the whole proof and every compiler message. We run the released agent with its documented 1M-token context and compaction, under the same model, prices and Lean version as Lever (§4.1). Setup. We compare Lever with this agent. Lever uses the comp value function (§4.4) during decomposition. In our exploration, we found that the LLM used here tends to over-decompose, even on simple problems. So, a goal five levels below the root is always proved directly, and Lever uses its value function to force a direct proof for any goal priced under bin 5 (§4.4). Each problem has a budget of $3 at the re-priced rate (§4.1), and a problem not solved within it is charged the full $3. We evaluate on the 8080 evaluation problems of §4.1. Decomposition makes proof search cheaper. Table 1 compares the two systems at $3. Lever solves 96.3%96.3\% of the problems, against 80.0%80.0\% for NearAI, and costs 34%34\% less. This is not a trade-off between solving and saving: Lever does better on both. Further, the failure charge is real spend: 94%94\% of NearAI’s failures spent the full $3 without producing a complete proof. Figure 4 shows that this holds at almost every budget: from $0.25 on, Lever solves more problems than NearAI. The savings come from how Lever manages context. NearAI writes fewer tokens than Lever (357357K against 621621K per problem), but it carries the context of the full problem on every turn, and reads 42.042.0M input tokens per problem. Lever works on each subgoal in its own local context and reads 17.917.9M, less than half. At the cost each run actually incurred, with its own cache hits, Lever still solves more problems than NearAI (0.9630.963 vs. 0.8630.863) and costs 16%16\% less (Appendix C.3). Tokens (M) Method Solved Cost ($) In Out NearAI 0.800 1.44 42.0 0.36 Lever 0.963 0.95 17.9 0.62 Table 1: Cost of proof search at a $3 budget per problem. N=80N=80. Cost and tokens are per problem. Solved problems contribute the cost to finish; unsolved problems are charged the full budget with tokens spent up to the call when cut-off. Figure 4: Solve rate against budget. A problem solved at cost c counts as solved at every budget ≥c≥ c. Identifying cheaper strategies. Lever’s algorithm uses the value function to reject decompositions whose subgoals sum up to be more expensive than the goal itself, and draw a new decomposition. On putnam_1972_a3, for example, Lever rejects its first decomposition from the value predictions alone, before working on any of its subgoals, and proves the theorem through a second decomposition predicted to be cheaper (Appendix C.4.1). However, such cases are rare, and not every redraw leads to savings: every subgraph that is given up on represents a sunk cost that is deducted from the global budget. 5.2 Proof Quality Optimization Setup. We optimize the two metrics of §4.3, topical impurity and proof length, on N=20N=20 problems drawn from successful runs of NearAI in §5.1. We write Leverλm_m^λ for Lever minimizing the objective C=comp+λ⋅mC= comp+λ· m with m∈imp,lenm∈\ imp, len\. Further, Lever0m_m^0 is always written as Lever (i.e., the run from § 5.1). Unlike Lever, which enforces no decomposition under a certain value, Leverλm_m^λ runs impose no such restriction to allow greater exploration during search. We run each metric m at two weights, and each run (including all baselines; see below) is with budget $4.5 (50% higher than in § 5.1 to accommodate cost of quality optimization on top of correctness). Baselines. Existing proof refactoring methods that target length, such as Lean Refactor (Lu et al., 2026) and ProofOptimizer (Gu et al., 2025) are not publicly available, while ImProver (Ahuja et al., 2024) targets a much older Lean version (v4.9) and model; none can be run in our controlled setup, with the same model, Lean version and budget. To our knowledge, no existing method optimizes topical impurity, and none optimizes proof quality during search. We therefore build baselines atop the strong agent from NearAI (2026). + Instruct steers the agent during its search: the end of its prompt states the metric and asks for a proof that minimizes it. + Refactor improves the proof after the search, as post-hoc refactoring does: it is handed NearAI’s finished baseline proof (§ 5.1) and asked to improve the proof. Together they cover the two alternatives to optimizing during search: steering by instruction and repairing afterwards. See Appendix C.5 for details. Reporting. We use the proofs delivered by NearAI from § 5.1 as a common anchor: we report relative reduction of metric m relative to this baseline proof, averaged over all problems. A run that fails or exceeds its budget is scored at the same metric as the baseline and charged at $4.5. Finally, because + Refactor starts from the NearAI proof baseline, its cost is the original cost plus the cost to refactor. 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 2020 problems. Lever’s points are λ=0,0.01,0.1λ=0,0.01,0.1 for impurity and λ=0,10−4,10−3λ=0,10^-4,10^-3 for length, light to dark; λ=0λ=0 is Lever run with its $3 budget and routing to direct attempts (§ 5.1); the λ>0λ>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: ±1± 1 standard error over problems. m=impm= imp m=lenm= len Method Δ Δ Δ Δ Lever (λ=0λ=0) +1%+1\% +4%+4\% +4%+4\% +1%+1\% Levermλ1 _1_m −15%-15\% +8%+8\% −5%-5\% +3%+3\% Levermλ2 _2_m −42%-42\% +10%+10\% −21%-21\% −18%-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 _1, _2 are 0.01,0.10.01,0.1 when optimizing impurity and 10−4,10−310^-4,10^-3 when optimizing length. A run that fails or exceeds $4.5 is scored as NearAI’s proof. Length optimization. We run Leverλlen_ len^λ for λ∈0.0001,0.001λ∈\0.0001,0.001\ and plot the results in Figure 5 (right). The proof length objective is well optimized by refactoring: previous works have independently reported trained refactoring models shorten PutnamBench proofs by 57% (Gu et al., 2025) and competition proofs by over 70% (Lu et al., 2026), in their respective settings. Our + Refactor baseline agrees: it shortens NearAI’s proofs by 31%31\% at $1.83 per problem. At λ=10−3λ=10^-3, Lever approaches + Refactor: its proofs are 21%21\% shorter, though at a higher cost of $2.59, indicating that searching for short proofs may be more challenging than searching for a correct proof first followed by refactoring. Impurity optimization. We run Leverλimp_ imp^λ for λ∈0.01,0.1λ∈\0.01,0.1\ with results in Figure 5 (left). Unlike length, refactoring is not built for topical impurity because removing an out-of-subject reference usually means changing the argument rather than tidying it. Our + Refactor baseline reduces impurity by 33%33\% at $2.88 per problem. At λ=0.1λ=0.1, Lever’s proofs are 42%42\% purer, at $1.85, about two-thirds of + Refactor’s cost. Lever is also more reliable: the standard deviation of its per-problem reduction is 3232 points, against 101101 for + Refactor, whose rewrites can backfire badly (on putnam_2007_a2, from 2929 out-of-subject references to 132132). Instructing the agent to look for pure proofs does not help either: + Instruct’s proofs are, on the contrary, 11%11\% less pure than the baseline, indicating that the agent loses context of the search objective in its single long session. This indicates that, when a metric depends on the proof strategy itself, optimizing it during search and treating it locally, works best. Trade-offs among metrics. As shown in Figure 5, Lever allows tracing a cost-quality trade-off curve: as λ rises, proof quality improves and the search costs more. Since λ is a conversion rate between metrics, a user can choose how much quality is worth paying for, and move smoothly along this frontier. In contrast, any fixed policy, such as the baselines considered here, admits only single points in this space. We observe that Lever’s search also reveals relationships among various quality metrics (Table 2). Shortening a proof makes it purer: as proofs get shorter (+4%→−21%+4\%→-21\%), impurity reduces as well (+1%→−18%+1\%→-18\%). This is likely because as a proof is shortened, impure references are removed for free. However, the reverse does not hold: optimizing for impurity alone (+1%→−42%+1\%→-42\%) makes proofs longer (+4%→+10%+4\%→+10\%); this supports our observation that optimizing impurity requires a different strategy than what works for length reduction. 6 Conclusion We presented Lever, a proof search algorithm that treats correctness as a constraint and makes the objective over correct proofs programmable. By valuing partial proofs over an AND/OR graph, combining realized costs with predictions for open goals, Lever optimizes that objective during search rather than repairing a proof afterwards. On PutnamBench, it is 34%34\% cheaper than a strong single-conversation agent while solving more problems (96%96\% against 80%80\%). On topical impurity, search-time optimization removes more out-of-subject references than post-hoc refactoring at two-thirds of its cost, and on proof length it approaches refactoring. A single weight trades quality against cost, letting a user choose how much a better proof is worth. Generative AI Use Statement Beyond the LLMs that are the object of our experiments, we used generative AI tools to write code, run and monitor experiments, survey the literature, check ideas, draft proofs, and polish the writing. AI tools had no or minimal involvement in developing the main ideas of the paper, or in interpreting and iterating on experimental results. We have reviewed AI-assisted work to our best ability, and we take responsibility for the final content of this paper, including text, claims and artifacts produced with the aid of generative AI. Acknowledgments We gratefully acknowledge use of the research computing resources of the Empire AI Consortium, Inc, with support from Empire State Development of the State of New York, the Simons Foundation, and the Secunda Family Foundation (Bloom et al., 2025). References Achim et al. (2025) T. Achim, A. Best, A. Bietti, K. Der, M. Fédérico, S. Gukov, D. Halpern-Leistner, K. Henningsgard, Y. Kudryashov, A. Meiburg, M. Michelsen, R. Patterson, E. Rodriguez, L. Scharff, V. Shanker, V. Sicca, H. Sowrirajan, A. Swope, M. Tamas, V. Tenev, J. Thomm, H. Williams, and L. Wu Aristotle: IMO-level automated theorem proving. External Links: 2510.01346, Link Cited by: §2. Ahuja et al. (2024) R. Ahuja, J. Avigad, P. Tetali, and S. Welleck ImProver: agent-based automated proof optimization. External Links: 2410.04753, Link Cited by: §1, §2, §5.2. Allis et al. (1994) L. V. Allis, M. van der Meulen, and H. J. van den Herik Proof-number search. Artif. Intell. 66 (1), p. 91–124. External Links: ISSN 0004-3702, Link, Document Cited by: §2. Appel and Haken (1977) K. Appel and W. Haken Every planar map is four colorable. Part I: discharging. Illinois Journal of Mathematics 21 (3), p. 429–490. Cited by: §1. Bloom et al. (2025) S. Bloom, J. C. Brumberg, I. Fisk, R. J. Harrison, R. Hull, M. Ramasubramanian, K. V. Vliet, and J. Wing Empire AI: a new model for provisioning AI and HPC for academic research in the public good. In Practice and Experience in Advanced Research Computing (PEARC ’25), Columbus, OH, USA, p. 4. External Links: Document, Link Cited by: §6. Chen et al. (2020) B. Chen, C. Li, H. Dai, and L. Song Retro*: learning retrosynthetic planning with neural guided A* search. In Proceedings of the 37th International Conference on Machine Learning, Cited by: §2. Chen et al. (2025) L. Chen, J. Gu, L. Huang, W. Huang, Z. Jiang, A. Jie, X. Jin, X. Jin, C. Li, K. Ma, C. Ren, J. Shen, W. Shi, T. Sun, H. Sun, J. Wang, S. Wang, Z. Wang, C. Wei, S. Wei, Y. Wu, Y. Wu, Y. Xia, H. Xin, F. Yang, H. Ying, H. Yuan, Z. Yuan, T. Zhan, C. Zhang, Y. Zhang, G. Zhang, T. Zhao, J. Zhao, Y. Zhou, and T. H. Zhu Seed-Prover: deep and broad reasoning for automated theorem proving. External Links: 2507.23726, Link Cited by: §2. Chung et al. (2026) J. Chung, Z. Cai, Z. Li, Q. Yin, R. Agarwal, S. Park, R. Porto, N. Ri, Z. Yang, S. Tang, X. Dang, H. Lin, M. Wang, D. Chen, C. Jin, L. H. Fowl, and S. Arora Goedel-Architect: streamlining formal theorem proving with blueprint generation and refinement. External Links: 2606.06468, Link Cited by: §2, §4.2, §4.2. Community Mathlib (2020) Community Mathlib The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20, p. 367–381. External Links: Link, Document Cited by: §4.3. DeepSeek-AI et al. (2026) DeepSeek-AI, A. Xu, B. Lin, B. Xue, B. Wang, B. Xu, B. Wu, B. Zhang, C. Lin, C. Dong, C. Ling, C. Lu, C. Zhao, C. Deng, C. Hou, C. Xu, C. Shao, C. Ruan, C. Sun, D. Dai, D. Guo, D. Yang, D. Chen, D. Li, D. Ji, E. Li, F. Wei, F. Lin, F. Yuan, F. Xia, F. Dai, G. Hao, G. Chen, G. Cao, G. Meng, G. Li, H. Yu, H. Zhang, H. Xu, H. Li, H. Liang, H. Zhang, H. Luo, H. Wei, H. Yuan, H. Zhang, H. Luo, H. Chen, H. Ji, H. Zhang, H. Ding, H. Tang, H. Cao, H. Gao, H. Qu, H. Zeng, J. Yang, J. Zhu, J. Luo, J. Song, J. Yu, J. Huang, J. Cai, J. Liang, J. Zhou, J. Ye, J. Li, J. Xu, J. Hu, J. Yang, J. Chen, J. Yan, J. Chen, J. Zhou, J. Xiang, J. Yuan, J. Cheng, J. Zhou, J. Zhu, J. Yu, J. Sun, J. Ran, J. Jiang, J. Qiu, J. Li, J. Zheng, J. Song, K. Dong, K. Gao, K. Guan, K. Zhou, K. Huang, K. Yu, L. Wang, L. Zhang, L. Wang, L. Xia, L. Zhang, L. Zhao, L. Guo, L. Luo, L. Ma, L. Zhu, L. Wang, L. Cai, L. Zhang, L. Chen, M. Di, M. Xu, M. Mei, M. Wang, M. Zhang, M. Zhang, M. Tang, M. Li, M. Zhou, M. Han, N. Wang, P. Huang, P. Wang, P. Cong, P. Wang, P. Zhang, Q. Wang, Q. Zhu, Q. Li, Q. Chen, Q. Du, Q. Jiang, R. Tian, R. Xu, R. Lu, R. Xu, R. Ge, R. Zhang, R. Pan, R. Wang, R. Chen, R. Yin, R. Xu, R. Shen, R. Zhang, R. Chen, S. Liu, S. Lu, S. Sun, S. Zhou, S. Chen, S. Cai, S. Nie, S. Wu, S. Chen, S. Hu, S. Liu, S. Hu, S. Ma, S. Wang, S. Yu, S. Zhou, S. Pan, S. Yu, S. Zhou, T. Ni, T. Yun, T. Jin, T. Pei, T. Ye, T. Lin, T. Ji, T. Cui, T. Yue, T. Yu, T. Wang, W. Zhang, W. Xiao, W. Zeng, W. An, W. Zhao, W. Liu, W. Liang, W. Pang, W. Luo, W. Yao, W. Gao, W. Yang, W. Huang, W. Hou, W. Zhang, W. Ma, X. Gao, X. He, X. Wang, X. Wang, X. Bi, X. Liu, X. Wang, X. Chen, X. Zhang, X. Nie, X. Sun, X. Wang, X. Cheng, X. Liu, X. Xie, X. Liu, X. Liu, X. Yu, X. Li, X. Yang, X. Zhang, X. Chen, X. Wang, X. Su, X. Chen, X. Lin, X. Fu, Y. Yan, Y. Wang, Y. Ma, Y. Luo, Y. Zhang, Y. Xu, Y. Ma, Y. Huang, Y. Li, Y. Li, Y. Xu, Y. Zhao, Y. Sun, Y. Wang, Y. Qian, Y. Shao, Y. Yu, Y. Zhang, Y. Ding, Y. Shi, Y. Wu, Y. Xiong, Y. Ma, Y. He, Y. Tang, Y. Zhou, Y. Luo, Y. Zhong, Y. Piao, Y. Wang, Y. Zhang, Y. Chen, Y. Tan, Y. Wei, Y. Ma, Y. Liu, Y. Yang, Y. Guo, Y. Wu, Y. Wu, Y. Li, Y. Cheng, Y. Ou, Y. Xu, Y. Li, Y. Wang, Y. Yang, Y. Xu, Y. Wu, Y. Meng, Y. Zou, Y. Zha, Y. Xiong, Y. Chen, Y. Lin, Y. Cao, Y. Wang, Y. Zhang, Y. Yan, Y. Lin, Y. Gu, Y. Luo, Y. You, Y. Liu, Y. Zhou, Y. Zhou, Y. Huang, Z. Wu, Z. Wang, Z. Zhao, Z. Ren, Z. Zhang, Z. Sha, Z. Fu, Z. Ju, Z. Xu, Z. Xie, Z. Zhang, Z. Gao, Z. Hao, Z. Gou, Z. Ma, Z. Yan, Z. Shao, Z. Huang, Z. Chen, Z. Wu, Z. Ren, Z. Wu, Z. Li, Z. Zhang, Z. Xu, Z. Wang, Z. Qu, Z. Gu, Z. Zhu, Z. Li, Z. Zhang, Z. Xie, Z. Gao, Z. Wan, Z. Pan, and Z. Yao DeepSeek-V4: towards highly efficient million-token context intelligence. External Links: 2606.19348, Link Cited by: §4.1. DeepSeek-AI (2026) DeepSeek-AI DeepSeek-V4-Pro GA Release. Note: https://api-docs.deepseek.com/news/news260813Accessed: 2026-09-21 Cited by: §4.1. Detlefsen and Arana (2011) M. Detlefsen and A. Arana Purity of methods. Philosophers’ Imprint 11. Cited by: §1, §1, §4.3. Dong et al. (2024) K. Dong, A. V. Mahankali, and T. Ma Formal theorem proving by rewarding LLMs to decompose proofs hierarchically. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, External Links: Link Cited by: §2. First et al. (2023) E. First, M. N. Rabe, T. Ringer, and Y. Brun Baldur: whole-proof generation and repair with large language models. External Links: 2303.04910, Link Cited by: §2. Fu et al. (2026) Y. Fu, P. Liu, Z. Wang, and K. Yuan Proof-Refactor: refactoring generated formal proofs into modular artifacts. External Links: 2606.03743, Link Cited by: §1, §2. Gonthier (2008) G. Gonthier Formal proof—the four-color theorem. Notices of the AMS 55 (11), p. 1382–1393. Cited by: §1. Gu et al. (2025) A. Gu, B. Piotrowski, F. Gloeckle, K. Yang, and A. H. Markosyan ProofOptimizer: training language models to simplify proofs without human demonstrations. External Links: 2510.15700, Link Cited by: §2, §4.3, §5.2, §5.2. Guez et al. (2018) A. Guez, T. Weber, I. Antonoglou, K. Simonyan, O. Vinyals, D. Wierstra, R. Munos, and D. Silver Learning to search with MCTSnets. External Links: 1802.04697, Link Cited by: §2. Hansen and Zilberstein (2001) E. A. Hansen and S. Zilberstein LAO∗^*: a heuristic search algorithm that finds solutions with loops. Artificial Intelligence 129 (1), p. 35–62. External Links: ISSN 0004-3702, Document, Link Cited by: §2. Hao et al. (2023) S. Hao, Y. Gu, H. Ma, J. Hong, Z. Wang, D. Wang, and Z. Hu Reasoning with language model is planning with world model. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, p. 8154–8173. External Links: Document, Link Cited by: §2. Hubert et al. (2025) T. Hubert, R. Mehta, L. Sartran, M. Z. Horváth, G. Žužić, E. Wieser, A. Huang, J. Schrittwieser, Y. Schroecker, H. Masoom, O. Bertolli, T. Zahavy, A. Mandhane, J. Yung, I. Beloshapka, B. Ibarz, V. Veeriah, L. Yu, O. Nash, P. Lezeau, S. Mercuri, C. Sönne, B. Mehta, A. Davies, D. Zheng, F. Pedregosa, Y. Li, I. von Glehn, M. Rowland, S. Albanie, A. Velingker, S. Schmitt, E. Lockhart, E. Hughes, H. Michalewski, N. Sonnerat, D. Hassabis, P. Kohli, and D. Silver Olympiad-level formal mathematical reasoning with reinforcement learning. Nature 651 (8106), p. 607–613. External Links: Document, Link, ISSN 1476-4687 Cited by: §2. Inoue et al. (2026) Y. Inoue, K. Kawarabayashi, A. Miyashita, B. Mohar, C. Thomassen, and M. Thorup The four color theorem with linearly many reducible configurations and near-linear time coloring. External Links: 2603.24880 Cited by: §1. Jiang et al. (2023) A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y. Wu Draft, sketch, and prove: guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, External Links: Link Cited by: §2. Kocsis and Szepesvári (2006) L. Kocsis and C. Szepesvári Bandit based Monte-Carlo planning. In Machine Learning: ECML 2006, J. Fürnkranz, T. Scheffer, and M. Spiliopoulou (Eds.), Berlin, Heidelberg, p. 282–293. External Links: ISBN 978-3-540-46056-5 Cited by: §2. Kung et al. (2026) P. Kung, L. Song, D. Hwang, J. Yoon, C. Li, S. Severini, M. Olšák, E. Lockhart, Q. V. Le, B. Gokturk, et al. LEAP: supercharging LLMs for formal mathematics with agentic frameworks. arXiv preprint arXiv:2606.03303. Cited by: §2. Lample et al. (2022) G. Lample, M. Lachaux, T. Lavril, X. Martinet, A. Hayat, G. Ebner, A. Rodriguez, and T. Lacroix HyperTree proof search for neural theorem proving. External Links: 2205.11491, Link Cited by: §2. Lightman et al. (2023) H. Lightman, V. Kosaraju, Y. Burda, H. Edwards, B. Baker, T. Lee, J. Leike, J. Schulman, I. Sutskever, and K. Cobbe Let’s verify step by step. External Links: 2305.20050, Link Cited by: §2. Lin et al. (2025) Y. Lin, S. Tang, B. Lyu, Z. Yang, J. Chung, H. Zhao, L. Jiang, Y. Geng, J. Ge, J. Sun, J. Wu, J. Gesi, X. Lu, D. Acuna, K. Yang, H. Lin, Y. Choi, D. Chen, S. Arora, and C. Jin Goedel-Prover-V2: scaling formal theorem proving with scaffolded data synthesis and self-correction. External Links: 2508.03613, Link Cited by: §2, §4.2. Lu et al. (2025) J. Lu, K. Emond, K. Yang, S. Chaudhuri, W. Sun, and W. Chen Lean Finder: semantic search for Mathlib that understands user intents. arXiv preprint arXiv:2510.15940. Cited by: §4.2. Lu et al. (2026) J. Lu, S. Kong, R. Stehling, K. Yang, Z. Wang, W. Sun, and W. Chen Lean Refactor: multi-objective controllable proof optimization via agentic strategy search. External Links: 2605.20244, Link Cited by: §1, §2, §5.2, §5.2. Martelli and Montanari (1973) A. Martelli and U. Montanari Additive AND/OR Graphs. In International Joint Conference on Artificial Intelligence, p. 1–11. External Links: Link Cited by: §2. Martinot (2024) R. Martinot Ontological purity for formal proofs. Review of Symbolic Logic 17 (2), p. 395–434. External Links: Document Cited by: §1, §4.3. MistralAI (2026) MistralAI LeanStral. Note: https://github.com/mistralai/LeanstralSafeVerify/blob/main/LeanstralReport.pdf Cited by: §1. NearAI (2026) NearAI Putnambench-deepseek: an autonomous DeepSeek-driven agent that solved PutnamBench in Lean 4. GitHub. Note: https://github.com/nearai/putnambench-deepseekAccessed 14 September 2026 Cited by: §C.1, §C.5, §1, §4.1, §4.1, §5.1, §5.2. Nilsson (2014) N. J. Nilsson Principles of artificial intelligence. Morgan Kaufmann. Cited by: §2, §3.3. Polu and Sutskever (2020) S. Polu and I. Sutskever Generative language modeling for automated theorem proving. External Links: 2009.03393, Link Cited by: §2. Ren et al. (2025) Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, Z. F. Wu, Z. Gou, S. Ma, H. Tang, Y. Liu, W. Gao, D. Guo, and C. Ruan DeepSeek-Prover-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. External Links: 2504.21801, Link Cited by: §2. Rögnvaldsson et al. (2026) K. Rögnvaldsson, C. Sun, J. Dekoninck, and M. Vechev Optimizing the cost-quality tradeoff of agentic theorem provers in Lean. External Links: 2606.04883, Link Cited by: §1, §2. Russell and Wefald (1991) S. Russell and E. Wefald Principles of metareasoning. Artificial Intelligence 49 (1), p. 361–395. External Links: ISSN 0004-3702, Document, Link Cited by: §2. Sabbata et al. (2025) C. N. D. Sabbata, T. R. Sumers, B. AlKhamissi, A. Bosselut, and T. L. Griffiths Rational metareasoning for large language models. External Links: 2410.05563, Link Cited by: §2. Sahni (1974) S. Sahni Computationally related problems. SIAM Journal on Computing 3 (4), p. 262–279. External Links: Document Cited by: Appendix A, §3.3. Santos et al. (2025) M. D. Santos, H. de Saxcé, H. Wang, R. Wang, M. Baksys, M. Unsal, J. Liu, Z. Liu, and J. Li Kimina Lean Server: a high-performance Lean server for large-scale verification. External Links: 2504.21230, Link Cited by: §4.2. Silver et al. (2016) D. Silver, A. Huang, C. J. Maddison, A. Guez, L. Sifre, G. van den Driessche, J. Schrittwieser, I. Antonoglou, V. Panneershelvam, M. Lanctot, S. Dieleman, D. Grewe, J. Nham, N. Kalchbrenner, I. Sutskever, T. Lillicrap, M. Leach, K. Kavukcuoglu, T. Graepel, and D. Hassabis Mastering the game of Go with deep neural networks and tree search. Nature 529 (7587), p. 484–489. External Links: Document, Link, ISSN 1476-4687 Cited by: §2. Silver et al. (2018) D. Silver, T. Hubert, J. Schrittwieser, I. Antonoglou, M. Lai, A. Guez, M. Lanctot, L. Sifre, D. Kumaran, T. Graepel, T. Lillicrap, K. Simonyan, and D. Hassabis A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play. Science 362 (6419), p. 1140–1144. External Links: Document, Link, ISSN 1095-9203 Cited by: §2. Snell et al. (2024) C. Snell, J. Lee, K. Xu, and A. Kumar Scaling LLM test-time compute optimally can be more effective than scaling model parameters. External Links: 2408.03314, Link Cited by: §2. Steiner (1978) M. Steiner Mathematical explanation. Philosophical Studies: An International Journal for Philosophy in the Analytic Tradition 34 (2), p. 135–151. Cited by: §1. Tao (2007) T. Tao What is good mathematics?. Bulletin of the American Mathematical Society 44 (4), p. 623–634. Cited by: §1. Thiele (2003) R. Thiele Hilbert’s twenty-fourth problem. The American Mathematical Monthly 110 (1), p. 1–24. Cited by: §1. Tsoukalas et al. (2026) G. Tsoukalas, A. Kovsharov, S. Shirobokov, A. Surina, M. Firsching, G. Bérczi, F. J. R. Ruiz, A. Suggala, A. Z. Wagner, E. Wieser, L. Yu, A. Huang, M. Z. Horváth, A. Ferraiuolo, H. Michalewski, E. Lockhart, C. Grosu, T. Hubert, M. Balog, P. Kohli, and S. Chaudhuri Advancing mathematics research with AI-driven formal proof search. External Links: 2605.22763, Link Cited by: §2. Tsoukalas et al. (2024) G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri PutnamBench: evaluating neural theorem-provers on the Putnam mathematical competition. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, External Links: Link Cited by: §1, §4.1. Varambally et al. (2026) S. Varambally, T. Voice, Y. Sun, Z. Chen, R. Yu, and K. Ye Hilbert: recursively building formal proofs with informal reasoning. External Links: 2509.22819, Link Cited by: §2, §4.2. Wang et al. (2025) H. Wang, M. Unsal, X. Lin, M. Baksys, J. Liu, M. D. Santos, F. Sung, M. Vinyes, Z. Ying, Z. Zhu, J. Lu, H. de Saxcé, B. Bailey, C. Song, C. Xiao, D. Zhang, E. Zhang, F. Pu, H. Zhu, J. Liu, J. Bayer, J. Michel, L. Yu, L. Dreyfus-Schmidt, L. Tunstall, L. Pagani, M. Machado, P. Bourigault, R. Wang, S. Polu, T. Barroyer, W. Li, Y. Niu, Y. Fleureau, Y. Hu, Z. Yu, Z. Wang, Z. Yang, Z. Liu, and J. Li Kimina-Prover preview: towards large formal reasoning models with reinforcement learning. External Links: 2504.11354, Link Cited by: §2. Wang et al. (2024a) H. Wang, H. Xin, C. Zheng, Z. Liu, Q. Cao, Y. Huang, J. Xiong, H. Shi, E. Xie, J. Yin, Z. Li, and X. Liang LEGO-Prover: neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, External Links: Link Cited by: §2. Wang et al. (2024b) P. Wang, L. Li, Z. Shao, R. Xu, D. Dai, Y. Li, D. Chen, Y. Wu, and Z. Sui Math-Shepherd: verify and reinforce LLMs step-by-step without human annotations. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), p. 9426–9439. External Links: Document, Link Cited by: §2. Weitzman (1979) M. L. Weitzman Optimal search for the best alternative. Econometrica 47 (3), p. 641–654. Cited by: §2. Xin et al. (2024) H. Xin, Z. Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Q. Du, W. Gao, Q. Zhu, D. Yang, Z. Gou, Z. F. Wu, F. Luo, and C. Ruan DeepSeek-Prover-V1.5: harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. External Links: 2408.08152, Link Cited by: §2. Xin et al. (2025) R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y. Sun, S. Zheng, and K. Shen BFS-Prover: scalable best-first tree search for LLM-based automatic theorem proving. External Links: 2502.03438, Link Cited by: §2. Yang et al. (2023) K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar LeanDojo: theorem proving with retrieval-augmented language models. External Links: 2306.15626, Link Cited by: §2. Yao et al. (2023) S. Yao, D. Yu, J. Zhao, I. Shafran, T. Griffiths, Y. Cao, and K. Narasimhan Tree of thoughts: deliberate problem solving with large language models. In Advances in Neural Information Processing Systems 36, NeurIPS 2023, p. 11809–11822. External Links: Document, Link Cited by: §2. Yao et al. (2022) S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao ReAct: synergizing reasoning and acting in language models. arXiv preprint arXiv:2210.03629. Cited by: §4.2. Zhang et al. (2026) N. Zhang, N. Di, Z. Li, Y. Yao, and X. Ma Planning to hammer: difficulty-aware decomposition for automating Rocq proofs. External Links: 2606.17981, Link Cited by: §2. Zhou et al. (2024) A. Zhou, K. Yan, M. Shlapentokh-Rothman, H. Wang, and Y. Wang Language agent tree search unifies reasoning acting and planning in language models. External Links: 2310.04406, Link Cited by: §2. Zhu et al. (2026) T. Zhu, P. Monticone, J. Avigad, and S. Welleck LeanArchitect: automating blueprint generation for humans and AI. External Links: 2601.22554, Link Cited by: §4.2. Appendix A Lever: System Design Planner. Before the search, one planner conversation per problem writes an informal proof. It has search_mathlib and python, runs at high reasoning effort, and is capped at $0.20. The plan is written once per problem and reused by every Lever run on that problem. Every expansion carries it in its system prompt, and is told that the plan is a guide, which the task in hand supersedes where the two disagree. Tools. An expansion edits the goal’s Lean file in a buffer (view, replace, replace_all, delete_lines), and any edit can compile the file in the same step. It can also check a Lean snippet without touching the buffer (lean_check), search Mathlib (search_mathlib), run Python (python), compile the file against every submission rule (lean_compile), and submit the last file that compiled (submit_proof). A subgoal’s conversation may instead report its goal false (disprove). Decomposing a goal. The agent writes the proof of the target in the file it is given, and may add two kinds of helper lemmas above it. Closed helpers are small steps proved in place. Open helpers are large steps left as sorry_using […], where the list names the declarations in the file that the helper’s own proof will use; each becomes a subgoal, proved in a later conversation. Every declaration it adds carries a LeanArchitect blueprint attribute, an informal statement and proof in words, so a subgoal’s conversation knows what its lemma is for. A file is accepted only if its header, the declarations it was handed and the target’s signature are unchanged; the target is its last declaration, with no sorry in its body; every helper lemma is either proved or open with exactly sorry_using […] as its body; and it uses none of native_decide, axiom, admit, or search tactics ending in ?. Shared subgoals. A subgoal’s identity is its Lean file with the blueprint annotations stripped: the lemma, together with the open helpers it depends on through sorry_using. Two decompositions that introduce the same lemma, or a subgoal whose proof uses a sibling it depends on, therefore reach the same OR node, which is proved once. A proof should then pay for a shared subgoal once, not once per use as the recursion of §3.1 does, and under that accounting finding the cheapest solution subgraph is NP-hard (Sahni, 1974). Lever instead charges each shared subgoal to one goal, the one whose decomposition first introduced it (or the next, if that decomposition dies). Every alternative decomposition of that goal pays for the subgoal, not only the one that introduced it, so the goal compares its alternatives on what each would cost; decompositions of other goals use the subgoal free, since it is proved once for all of them. Ownership depends only on the order in which nodes were created, not on which alternatives are chosen, so values cannot oscillate; the cost is that a shared subgoal’s price drops out of the root’s value when its owner chooses an alternative that does not use it. Proving directly. The direct arm uses the same plan, context and tools, but may leave no helper open. Context inheritance. A subgoal’s conversation starts from its parent’s: from the full transcript if the parent’s conversation is under 2020K tokens, and otherwise from the parent’s compacted output. Any conversation that reaches 128128K tokens is likewise replaced by its compacted output. Redraws. When a goal is expanded again, its new conversation is told what the earlier attempts found: which of their helpers were proved, which were reported false and why, which were never proved, and what the value function priced the rest at. Disproofs and failures. A disproof is a claim about the goal rather than the attempt: the goal is closed as false, its value becomes ∞, and later decompositions of its parent are told the statement is false and why. An attempt that ends without an accepted file is a failure. Its spend is charged, and its goal’s estimate rises by one σ (§3.3). Parallelism and budget. Each iteration expands up to 2525 selected goals concurrently, one attempt each. The spend of every LLM call, whether expansion, value function or planner, is charged to the problem’s budget as it is made, and running conversations read that spend between calls, so the search stops once the budget is reached rather than after the attempts in flight return. Prompts. Listings 1–3 give, verbatim, the planner’s prompt, the system prompt of every expansion, and the prompt of a decomposition. <statement> stands for the goal’s Lean file, <target> for the declaration to prove, and <plan> for the planner’s output. A subgoal’s conversation, which continues from its parent’s, opens instead with “The buffer now holds <target>, a lemma you left open above, as its own file, shown below. Your task is to write the proof of <target> in it.” The direct arm’s prompt has the same structure, but requires every new helper to be proved. ⬇ Your task is to write a natural language proof of the goal `<target>` found in the Lean 4 file below. ## File ```lean4 <statement> ``` Your final submission should be the complete mathematical argument that proves `<target>`, written in natural language prose. ## Instructions - **Pick a strategy that is easy to formalize**: A later stage will write your plan out in Lean 4 against Mathlib, and that is what your plan is judged on. So the approach to submit is the one that can be implemented using Mathlib machinery that already exists. Every approach may need results Mathlib lacks: for each candidate, list what is missing, and pick the one whose missing pieces are smallest and most elementary. - **Survey Mathlib before you commit to an approach**: Use `search_mathlib` to investigate what exists in Mathlib, and explicitly name the Mathlib declarations that your argument depends on. - **No Lean proofs, but do name Lean results**: Do NOT write proof tactics or segments of a Lean proof. However, you should name the Mathlib declarations your steps rest on. Every name you give must be one a search actually returned. - **Verify each step**: Make sure that each step in your argument is logically sound and follows from the previous steps. The full proof that you submit should be complete and correct, and should not rely on any unproven claims or assumptions. Each intermediate claim must be true as a Lean statement using Mathlib, not just informally. - **A missing theory is a reason to change route**: If a step needs a general theorem Mathlib does not have, do NOT plan to build that theorem. Look for an argument that uses the specific hypotheses you have to prove only the special case you need. Build a missing result only when no route avoids it, and then build the SMALLEST version your argument uses. ## Tools You have access to the following tools: * `search_mathlib`: Use this tool to search for Mathlib declarations that may be useful in your proof. Submit queries that describe a Mathlib proposition or make a guess at the declaration name (e.g., "the product of two continuous functions is continuous" or "Continuous.mul"). Do not describe the problem you are solving itself; the index does not hold the answer to the problem. * `python`: Runs a Python 3 snippet and returns what it printed. The standard library, numpy, sympy and scipy are available. Use it to check a claim on small cases, or confirm a value before you build the argument on it. Use this tool sparingly. * `submit_plan`: Submits your plan and finishes the task. ## Output Format Your output should contain one section as follows: ``` # Plan A step-by-step outline of the argument that proves the statement, each step justified. Name the Mathlib results the steps rest on. When a step has no Mathlib result behind it, say so there, and say what you would build it from. ``` ## Recommended Workflow 1. Work out how the statement is proved mathematically, and note the two or three approaches that could work. Do not commit to one yet. 2. Investigate using `search_mathlib` which approach would be the easiest to formalize in Lean. 3. Work the chosen argument out in full, with each step justified. 4. Verify that each step is sound, then submit it with `submit_plan`. Listing 1: The planner’s prompt. ⬇ Your goal is to help formalize the solution to the following problem in Lean 4: ```lean4 <statement> ``` Here is the originally constructed plan to solve this problem: <plan> Use the above plan to guide your responses for the task shown below. NOTES: - The task may have deviated from the plan; in this case the task description supersedes the plan. - If something in the plan is false or unclear, you should work out a fix, ignore the plan and complete the task using your own reasoning. The plan is only a guide, not a rule. Your response to the task below should help formalize the solution to the above problem as easily as possible. Listing 2: The system prompt of every expansion. ⬇ Your task is to write the proof of `<target>` in the Lean 4 file below. The proof may use helper declarations above `<target>`, of two kinds: - Closed helpers: new theorems/lemmas that you prove here. These represent small pieces of the argument that are used in the main proof body of `<target>`. You should prove these here. - Open helpers: new theorems/lemmas that you leave open using the `sorry_using` tactic. These represent large pieces of the argument that are used in the main proof body of `<target>`. These are proved in a later session, so they are expensive. The hardest open helper you introduce should be much easier than `<target>`. If it is not, an AI grader will reject your submission. You should be able to judge the quality of your decomposition by how much work you do in the current file. ## File ```lean4 <statement> ``` ## What you submit The file as it stands when `lean_compile` last accepted it. All of these should hold, else the file is rejected: - The header, all declarations above `<target>` and `<target>`'s signature are left exactly as given (including the blueprint attributes). You may insert new declarations above `<target>`; do not edit or delete the ones already there. - `<target>` is the last declaration in the file. Its body contains no `sorry` or `sorry_using`. If you use `sorry` or `sorry_using` in the main proof body, it will be rejected but return the open goal(s) as feedback. - All helper declarations you add and `<target>` carry a blueprint attribute: ```lean4 @[blueprint (statement := /-- what it says, in words -/) (proof := /-- the mathematical argument, worked out in detail -/)] ``` - Each `lemma` and `theorem` helper is either proved in full (closed), or left open with exactly `:= by sorry_using [...]` as its whole body, where `[...]` lists other declarations in the file that the helper will use in its own proof (even transitively). Do not include Mathlib names or tactics. `[]` if none. When in doubt whether to add a declaration from this file in the list of dependencies, include it, aiming for recall. - All other helpers (like `def` or `abbrev`) should have a complete body and also carry the blueprint attribute. - These tactics are not allowed anywhere in the file: `native_decide`, `axiom`, `admit`, or search tactics ending in `?`. - Names may collide with a global namespace you cannot see. Rename if told to. ## How to proceed: - Work out a mathematical argument that can be easily formalized in lean. Ensure each step in your argument is sound and can be proven in Lean. Consider different formalization strategies. Your goal is to pick one that is the simplest to formalize in Lean. - Search before you commit to an approach. Investigate the Mathlib machinery that you can reuse instead of doing it yourself. If you are in doubt about a declaration, use the `search_mathlib` tool to look it up. - Write the complete proof in the main body, introducing open/closed helpers as necessary. You should prefer closed helpers and reserve open helpers for only the hard parts of the proof that are still much easier than `<target>`. If `<target>` can be proved in this session, prove it HERE. - Edit the file, compile it, and fix what the compiler reports. - Never state that the task is too complex or too long to finish. Solve the task in an iterative manner guided by the compiler feedback. - When to stop. Use `submit_proof` to finish. It submits the file your last `lean_compile` ACCEPTED. So if your final revision failed, fix the errors and compile it successfully before finishing. ## Tools The file above is open in an editing buffer. You always change it in place: - `view`/`replace`/`replace_all`/`delete_lines` - use these for interfacing with the buffer. Every edit takes `compile: true`, which compiles the file right after the edit, exactly as `lean_compile` would, and reports the result in the same reply. Set it on the edit that finishes a revision. - `lean_check` — compiles Lean 4 code you pass to it. This is to be used as a probe for quick checks of Lean code. Do NOT submit your proof to this tool; use `lean_compile` for that. Use `lean_check` sparingly. This tool does NOT write to the buffer. - `python` — runs a Python 3 snippet and returns what it printed. The standard library only. Use it to check a claim on small cases, or confirm a value before you formalise it. Use this tool sparingly. - `search_mathlib` — describe a proposition, or guess a name ("the product of two continuous functions is continuous", "Continuous.mul"). You should look for known mathematical facts that are likely to be present in Mathlib. - `lean_compile` — checks the file as it now stands against every requirement above. Reports PASSED, or the failures. Proofs with `sorry` are considered failures but reveal the goal state where `sorry` occurs, which may be useful for the next attempt. Run this on your own RARELY. Prefer running compilation after edit as described above. - `submit_proof` — submits the file your last `lean_compile` accepted, and ends the task. IMPORTANT: every response costs a turn, and a turn re-sends the whole conversation, so put as many tool calls as you can into one response. Calls run in the order you list them: a later call sees an earlier one's effect (an edit with `compile: true`, then a `view` of the result, in ONE response) but not its result. Batch probes together (`lean_check`, `search_mathlib`, `python`, `view`); make a call on its own only when its arguments depend on a result you have not seen yet. Batching tools together is BEST practice and you should practice it as much as possible. Listing 3: The prompt of a decomposition, as the first expansion of a goal. Appendix B Topical Impurity Implementation. Listing 4 computes a proof’s impurity. Its input uses comes from #lever_uses, a Lean command that elaborates the proof file and reports, for each declaration in order, its kind, whether it rests on sorry, the constants in its statement (type), the library constants in explicit argument positions of its proof (mathlib_refs), and the file’s own declarations its proof references (own_refs). The last declaration is the theorem being proved. TABLE maps every Mathlib name to its directory, three levels deep, and whether it is a theorem. ⬇ ROOT = "<root>" # the concept of a generic lemma, which belongs to no subject LOGIC = "Eq", "Ne", "HEq", "And", "Or", "Iff", "Not", "Exists", "True", "False", "Classical", "congrArg", "congrFun", "cast", "id" INFRASTRUCTURE = "Init", "Batteries", "Mathlib/Data/Nat", "Mathlib/Logic/Basic", "Mathlib/Order/Basic", "Mathlib/Order/Defs", "Mathlib/Algebra/BigOperators", "Mathlib/Algebra/Group", "Mathlib/Algebra/GroupWithZero", "Mathlib/Algebra/NeZero", "Mathlib/Algebra/Order", "Mathlib/Algebra/Ring" def concept(name): # the namespace; a bare definition is its own concept head, _, rest = name.partition(".") if rest: return ROOT if head in ("Left", "Right") else head return ROOT if TABLE[name].is_theorem else name def machinery(name): # tactics, meta code, logical connectives, instances where = TABLE[name].location return ((name.startswith("inst") and name[4:5].isupper()) or where.startswith(("Mathlib/Tactic", "Mathlib/Util", "Mathlib/Lean")) or where.split("/")[0] in ("Lean", "Aesop", "Qq", "Plausible") or concept(name) in LOGIC) def subject(uses): # what the statement is about, on both readings stated = list(uses.values())[-1]["type"] named = [n for n in stated if n not in uses and n in TABLE and not machinery(n)] return (concept(n) for n in named | ROOT, TABLE[n].location for n in named) def through(uses, helpers, seen): # library names in the helpers' statements out = [] for h in helpers: if h in seen: continue seen.add(h) stated = uses[h]["type"] out += [n for n in stated if n not in uses] out += through(uses, [n for n in stated if n in uses], seen) return out def references(uses): # once per proved theorem that reaches for a name out = [] for decl in uses.values(): if decl["kind"] != "theorem" or decl["sorry"]: continue out += decl["mathlib_refs"] + through(uses, decl["own_refs"], set()) return out def impurity(uses): concepts, locations = subject(uses) count = 0 for n in references(uses): if n not in TABLE or not TABLE[n].is_theorem or machinery(n): continue where = TABLE[n].location if concept(n) == ROOT: pure = where in INFRASTRUCTURE or where in locations else: pure = concept(n) in concepts or where in locations count += not pure return count Listing 4: Topical impurity of a compiled proof, condensed from our implementation (logging and error handling removed). Example. putnam_1964_b4 asks how many regions n great circles cut a sphere into. NearAI’s proof cites 4444 impure theorems, from topology, convexity and group actions (e.g., isOpen_lt, convex_iff_forall_pos). Lever’s proof at λ=0.1λ=0.1 cites 88, mostly from the linear algebra of the circles’ planes (e.g., Submodule.finrank_sup_add_finrank_inf_eq). Can the metric be gamed? A proof could lower its count by re-proving an out-of-subject library lemma as a local helper: the helper’s statement names only definitions, which are not charged, and its proof may cite nothing impure. We checked for this on the 2020 problems of §5.2, counting the helpers whose statements name something outside the subject. At λ=0.1λ=0.1, Lever writes more helpers than at λ=0λ=0 (36.136.1 against 25.925.9 per proof), but only slightly more off-subject ones (11.211.2 against 10.110.1; NearAI: 14.114.1). Charging every off-subject helper as one more impure reference lowers Lever’s mean impurity reduction at λ=0.1λ=0.1 by under one point. Limitations. Topical impurity is a proxy for purity of method. It takes Mathlib’s organization as a stand-in for mathematical subject, and namespace and directory boundaries do not always match a mathematician’s; the infrastructure set is a judgment, measured on one pilot corpus. It counts references rather than weighing them, so an essential detour through another field counts the same as a routine lemma from it. And, as above, it charges a local re-proof of an out-of-subject lemma only through the library theorems that re-proof cites. Appendix C Experimental Details C.1 Problem Selection We rank PutnamBench with the published run of NearAI (2026), which solves all 672672 problems and records every attempt’s tokens and wall-clock time. Each problem is ranked by the token cost of its cheapest solving attempt, most expensive first, priced at a fixed rate table of $0.15, $0.003 and $0.60 per million input, cached input and output tokens (prices from NearAI (2026) originally; these rates are no longer available). Most problems are easy for this agent: below rank 150150, the median problem is solved in 0.30.3 hours (Table 3). The hardest are impractical for controlled comparisons that run every method on every problem: in the top 5050, 2020 problems needed more than one attempt and one took 5.55.5 days. We therefore take ranks 5151–150150, hard for the agent but solved in a median of 1.51.5 hours, and split them at random into 2020 calibration and 8080 evaluation problems. 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) 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. C.2 Value Functions Table 4 lists the constants of §3.3 for each metric. Metric Prediction Scale σ ρ n δ comp LLM, 7 bins log2 _2, $0.016–$0.512 0.615 1.08 0.33 1.85 len LLM, 7 bins log2 _2, 512–16,384 tokens 0.408 0.72 0.32 1.50 imp constant (=4=4) linear 6.79 31.2 0.05 1.72 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/ρ2n=σ^2/ρ^2: the prediction’s weight in draws; δ: the factor a redraw must promise. Bins and prompt. For comp, the seven bins are: under $0.016, factor-of-two bins from $0.016 to $0.512, and over $0.512; a goal is priced at its bin’s geometric center, and the open top bin at $0.72. For len, they are: under 512512 tokens, factor-of-two bins up to 16,38416,384, and over 16,38416,384. The value function may also answer that the goal is false, which prices it at ∞. We use the same model as the prover, DeepSeek-V4-Flash, at low reasoning effort, prompted with the goal’s Lean statement and 4040 worked examples: goals from runs on the calibration problems, each labelled with the bin its realized value fell in. comp labels are priced at the 90%90\% cache rate of §4.1, and len labels count tokens as the metric does. Prediction error ρ. We split the calibration problems by problem: the worked examples come from 1212 of them for comp and 1111 for len, and ρ is the root-mean-square of log(predicted/realized) (predicted/realized) over 6464 goals of the remaining 88 or 77. For comp, 34%34\% of predictions fall in the right bin and 75%75\% within one bin, and predictions are low by a factor of 1.531.53 on average. For len, 40%40\% fall in the right bin and 89%89\% within one, with no systematic bias. For imp, ρ is the root-mean-square impurity of the 125125 solved goals of the 1818 solved calibration problems, i.e., the error of predicting 00. Spread between draws σ. Measuring σ requires drawing the same goal repeatedly: on 162162 goals from a held-out set, each redrawn 66 times, gives σ=0.615±0.039σ=0.615± 0.039 in log dollars and 0.4080.408 in log tokens. Redraw margin δ and scaling. For comp and len, a redraw must beat the incumbent by one spread, δ=eσδ=e^σ. For imp, eσe^σ in references is meaningless (e6.79≈890e^6.79≈ 890), so we read the spread off the same draws proportionally: the median ratio of a goal’s standard deviation to its mean is 0.720.72, giving δ=1.72δ=1.72. The len estimate is 0.20.2 times the bin’s center, so the search expects shorter proofs than typical and keeps looking for them; the constant 44 for imp is the 2525th percentile of impurity over the calibration goals (§4.4). C.3 Cache-Hit Rates and Actual Cost All costs in the main text are re-priced at one common cache-hit rate of 90% (§4.1). Here we report the rates we observed and the costs they imply. Method Per call Per token NearAI 93.7% 96.2% Lever 86.2% 91.4% Table 5: Observed cache-hit rates on the 8080 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. Why the rates differ. Calls went through OpenRouter and InferX, which spread calls over several providers. Further, NearAI carries a single long conversation whereas Lever works on each goal in its own smaller context, reducing cache hit rate. 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 Actual 0.863 1.07 0.963 0.90 Table 6: Table 1 under other pricings. N=80N=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. Costs under other pricings. Table 6 repeats Table 1 under each pricing. At any common rate from 90% to 97%, Lever solves more problems than NearAI and costs 2929–34%34\% less. Priced at its own rates, Lever still solves more and costs less: 12%12\% less at its per-call rate, and 16%16\% less at actual cost. C.4 Case Studies C.4.1 Rejecting a Costly Decomposition: putnam_1972_a3 putnam_1972_a3prior $0.72$0.03rejected: $1.54>> 1.85 × $0.72continuous$0.72midpoint$0.72continuous &midpoint ⇒ affine$0.09$1.29kept: $0.91bounded above$0.18bounded ⇒ $0.72$0.26$0.11 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. The problem asks for every function on [0,1][0,1] that preserves Cesàro limits (Figure 6). The root is priced at $0.72. The first decomposition leaves three subgoals priced at $1.54 in total, more than δ=1.85δ=1.85 times the root’s prior, so the search draws the root again without attempting any of them. The second leaves two subgoals priced at $0.91; it is kept, both are proved, and the run costs $1.75. C.5 Quality Baselines Both baselines run the agent of NearAI (2026) unchanged, with the model, prices and Lean version of §4.1, and append an objective to the end of its system prompt. So that they are asked for exactly what Lever optimizes, the objective is Lever’s own text, word for word: what Lever tells a goal it redraws for that metric. Listing 5 shows the impurity objective, where <concepts> is the statement’s subject, read off by the same probe as the metric (Appendix B). The length objective has the same form: it defines a Lean token as the metric counts it, and asks for the shortest complete proof. + Instruct solves the problem from its statement, with the objective in its system prompt, and is capped at $4.5. + Refactor starts from NearAI’s finished proof of the problem (§5.1), which replaces the statement in the agent’s workspace, and is asked to rewrite it for the objective while keeping it a proof of the same theorem. Its objective adds what Lever tells a redraw about the attempt in hand: for impurity, how many times the proof leaves the subject and which lemmas do, grouped by field; for length, the proof’s token count. The run is capped at $4.5 minus what NearAI’s run cost, so that the pipeline as a whole has the same budget as every other method, and its reported cost includes NearAI’s. ⬇ # Optimization Objective `<problem>` is stated in terms of: ``` <concepts> ``` Those are its *subjects*. A proof stays inside the subject when every library fact it applies is about one of them, or is general enough to belong to general Mathlib infrastructure; it leaves the subject when it uses declaration(s) belonging to some other field. HINTS: - Revise the proof to keep it inside the subject the theorem is stated in. A proof leaves it when it reaches for a declaration in some other field; - If a helper leaves the subject, you should restate the helper so that it stays within the subject; - Change any open helper that you believe cannot be closed completely without leaving the subject; - You may have to consider a new formalization strategy for the full proof to stay within the subject. Listing 5: The impurity objective, appended to the baseline agent’s system prompt. Appendix D Theoretical Justification for Lever Listing 6 proves the exactness claim of §3.3 in Lean 4, without Mathlib. If V satisfies the backup equations on an acyclic AND/OR graph with nonnegative additive costs, then at every node n, V(n)=kV(n)=k exactly when k is the least cost of a solution subgraph rooted at n, and V(n)=∞V(n)=∞ exactly when none exists (lemma1_exact_values). A solution’s cost sums edge costs over its tree unfolding, so a shared subgoal counts once per use, and a prior with an exact estimate enters as a childless AND node whose edge costs that estimate. Costs are natural numbers in the formalization. ⬇ /-! # LEVER, Lemma 1 (Exact values) "For any nonnegative cost that adds along edges, the backed-up value `V(r)` is exactly the cost of the cheapest solution subgraph of the graph built so far." Formalization (core Lean 4, no Mathlib): * Costs are natural numbers (nonnegative by construction); `∞` is `none : Option Nat`. * The graph is a finite-branching AND/OR DAG; acyclicity is witnessed by a `rank` that strictly decreases along every edge. * A solution subgraph is defined inductively; its cost adds edge costs along every occurrence (the tree unfolding), which is what the backup of §3.1 computes. * `V` is *any* function satisfying the backup equations of §3.1. We prove it equals the optimal solution cost at every node (so the backup is also unique), and that a backed-up `∞` means no solution subgraph exists. -/ namespace Lever inductive Kind where | or | and deriving DecidableEq structure Graph (N : Type) where kind : N → Kind ch : N → List N cost : N → N → Nat rank : N → Nat acyclic : ∀ n d, d ∈ ch n → rank d < rank n /-! ### Extended naturals `Option Nat` (`none = ∞`) -/ def addE (a : Nat) : Option Nat → Option Nat | none => none | some b => some (a + b) /-- Binary sum on `Option Nat`; `∞` absorbs. -/ def add2 : Option Nat → Option Nat → Option Nat | some a, some b => some (a + b) | _, _ => none /-- Binary min on `Option Nat`; `∞` is the identity. -/ def min2 : Option Nat → Option Nat → Option Nat | none, r => r | some a, none => some a | some a, some b => some (min a b) /-- Sum; empty sum is `0`: a childless AND node is solved. -/ def sumE : List (Option Nat) → Option Nat | [] => some 0 | x :: xs => add2 x (sumE xs) /-- Minimum; empty min is `∞`: a childless OR node is unsolved. -/ def minE : List (Option Nat) → Option Nat | [] => none | x :: xs => min2 x (minE xs) def sumN : List Nat → Nat | [] => 0 | x :: xs => x + sumN xs /-! ### Solution subgraphs and backed-up values -/ /-- `Sol G n k`: a solution subgraph rooted at `n` exists with total cost `k`. -/ inductive Sol N : Type (G : Graph N) : N → Nat → Prop where | or n d : N k : Nat : G.kind n = .or → d ∈ G.ch n → Sol G d k → Sol G n (G.cost n d + k) | and n : N (k : N → Nat) : G.kind n = .and → (∀ d ∈ G.ch n, Sol G d (k d)) → Sol G n (sumN ((G.ch n).map fun d => G.cost n d + k d)) /-- The backup equations of §3.1. -/ structure IsBackup N : Type (G : Graph N) (V : N → Option Nat) : Prop where or_eq : ∀ n, G.kind n = .or → V n = minE ((G.ch n).map fun d => addE (G.cost n d) (V d)) and_eq : ∀ n, G.kind n = .and → V n = sumE ((G.ch n).map fun d => addE (G.cost n d) (V d)) /-! ### Auxiliary lemmas -/ theorem minE_mem : ∀ (l : List (Option Nat)) (k : Nat), minE l = some k → some k ∈ l | [], k, h => by simp [minE] at h | x :: xs, k, h => by cases x with | none => simp only [minE, min2] at h; exact List.mem_cons_of_mem _ (minE_mem xs k h) | some a => cases hr : minE xs with | none => simp [minE, min2, hr] at h; simp [h] | some b => simp only [minE, min2, hr, Option.some.injEq] at h by_cases hab : a ≤ b ⋅· simp only [Nat.min_def, if_pos hab] at h; simp [h] ⋅· simp only [Nat.min_def, if_neg hab] at h; subst h exact List.mem_cons_of_mem _ (minE_mem xs b hr) theorem minE_le : ∀ (l : List (Option Nat)) (a : Nat), some a ∈ l → ∃ k, minE l = some k ∧ k ≤ a | [], a, h => by simp at h | x :: xs, a, h => by rcases List.mem_cons.mp h with h | h ⋅· subst h cases hr : minE xs with | none => exact ⟨ , by simp [minE, min2, hr], Nat.le_refl _⟩ | some b => exact ⟨ a b, by simp [minE, min2, hr], Nat.min_le_left _ _⟩ ⋅· obtain ⟨ , hk, hka⟩ := minE_le xs a h cases x with | none => exact ⟨ , by simp [minE, min2, hk], hka⟩ | some c => exact ⟨ c k, by simp [minE, min2, hk], Nat.le_trans (Nat.min_le_right _ _) hka⟩ theorem sumE_some_all : ∀ (l : List (Option Nat)) (k : Nat), sumE l = some k → ∀ x ∈ l, ∃ j, x = some j | [], _, _, x, hx => by simp at hx | y :: ys, k, h, x, hx => by cases y with | none => simp [sumE, add2] at h | some a => cases hr : sumE ys with | none => simp [sumE, add2, hr] at h | some b => rcases List.mem_cons.mp hx with hx | hx ⋅· exact ⟨ , hx⟩ ⋅· exact sumE_some_all ys b hr x hx theorem sumE_map_of_all N : Type (c : N → Nat) (V : N → Option Nat) : ∀ l : List N, (∀ d ∈ l, ∃ j, V d = some j) → sumE (l.map fun d => addE (c d) (V d)) = some (sumN (l.map fun d => c d + (V d).getD 0)) | [], _ => rfl | d :: ds, h => by obtain ⟨ , hj⟩ := h d (List.mem_cons_self ..) have ih := sumE_map_of_all c V ds (fun e he => h e (List.mem_cons_of_mem _ he)) rw [List.map_cons, List.map_cons, sumE, sumN, ih, hj]; rfl theorem sumN_mono N : Type (f g : N → Nat) : ∀ l : List N, (∀ d ∈ l, f d ≤ g d) → sumN (l.map f) ≤ sumN (l.map g) | [], _ => Nat.le_refl _ | d :: ds, h => by simp only [List.map, sumN] exact Nat.add_le_add (h d (List.mem_cons_self ..)) (sumN_mono f g ds (fun e he => h e (List.mem_cons_of_mem _ he))) /-! ### Main results -/ section variable N : Type G : Graph N V : N → Option Nat /-- Soundness: a finite backed-up value is realized by some solution subgraph. -/ theorem backup_sound (hV : IsBackup G V) : ∀ (r : Nat) (n : N), G.rank n < r → ∀ k, V n = some k → Sol G n k | 0, _, hr, _, _ => absurd hr (Nat.not_lt_zero _) | r + 1, n, hr, k, hk => by have ih : ∀ d ∈ G.ch n, ∀ j, V d = some j → Sol G d j := fun d hd => backup_sound hV r d (Nat.lt_of_lt_of_le (G.acyclic n d hd) (Nat.le_of_lt_succ hr)) cases hkind : G.kind n with | or => rw [hV.or_eq n hkind] at hk obtain ⟨ , hd, hdk⟩ := List.mem_map.mp (minE_mem _ _ hk) cases hVd : V d with | none => simp [hVd, addE] at hdk | some j => simp only [hVd, addE, Option.some.injEq] at hdk subst hdk exact Sol.or hkind hd (ih d hd j hVd) | and => rw [hV.and_eq n hkind] at hk have hall : ∀ d ∈ G.ch n, ∃ j, V d = some j := by intro d hd obtain ⟨ , hx⟩ := sumE_some_all _ k hk _ (List.mem_map_of_mem hd) cases hVd : V d with | none => simp [hVd, addE] at hx | some j => exact ⟨ , rfl⟩ rw [sumE_map_of_all (G.cost n) V _ hall, Option.some.injEq] at hk subst hk refine Sol.and (fun d => (V d).getD 0) hkind (fun d hd => ?_) obtain ⟨ , hj⟩ := hall d hd exact ih d hd _ (by simp [hj]) /-- Optimality: every solution subgraph costs at least the backed-up value (in particular the backed-up value is finite whenever a solution exists). -/ theorem backup_le (hV : IsBackup G V) n : N k : Nat (h : Sol G n k) : ∃ v, V n = some v ∧ v ≤ k := by induction h with | @or n d k hkind hd _ ih => obtain ⟨ , hv, hvk⟩ := ih obtain ⟨ , hm, hmk⟩ := minE_le ((G.ch n).map fun d => addE (G.cost n d) (V d)) (G.cost n d + v) (List.mem_map.mpr ⟨ , hd, by simp [hv, addE]⟩ ) exact ⟨ , (hV.or_eq n hkind).trans hm, Nat.le_trans hmk (Nat.add_le_add_left hvk _)⟩ | @and n k hkind _ ih => have hall : ∀ d ∈ G.ch n, ∃ j, V d = some j := fun d hd => let ⟨ , hv, _⟩ := ih d hd; ⟨ , hv⟩ refine ⟨ _, (hV.and_eq n hkind).trans (sumE_map_of_all (G.cost n) V _ hall), ?_⟩ apply sumN_mono intro d hd obtain ⟨ , hv, hvk⟩ := ih d hd simpa [hv] using Nat.add_le_add_left hvk (G.cost n d) /-- **Lemma 1 (Exact values).** If `V` satisfies the backup equations on an acyclic AND/OR graph with nonnegative additive costs, then at every node `n` (in particular the root `r`): `V n = some k` iff `k` is the minimum cost of a solution subgraph rooted at `n`, and `V n = ∞` iff no solution subgraph rooted at `n` exists. -/ theorem lemma1_exact_values (hV : IsBackup G V) (n : N) : (∀ k, V n = some k ↔ (Sol G n k ∧ ∀ k', Sol G n k' → k ≤ k')) ∧ (V n = none ↔ ∀ k, ¬ Sol G n k) := by have sound := fun k => backup_sound hV (G.rank n + 1) n (Nat.lt_succ_self _) k refine ⟨ k => ⟨ hk => ⟨ k hk, fun k' h' => ?_⟩ , fun ⟨ , hmin⟩ => ?_⟩ , ⟨ hn k hs => ?_, fun hno => ?_⟩ ⟩ ⋅· obtain ⟨ , hv, hvk⟩ := backup_le hV h' rw [hk, Option.some.injEq] at hv; exact hv ⊳ hvk ⋅· obtain ⟨ , hv, hvk⟩ := backup_le hV hs have := hmin v (sound v hv) rw [hv, Nat.le_antisymm hvk this] ⋅· obtain ⟨ , hv, _⟩ := backup_le hV hs; rw [hn] at hv; cases hv ⋅· cases hVn : V n with | none => rfl | some v => exact absurd (sound v hVn) (hno v) end end Lever Listing 6: Exact values, verified in Lean 4 (Lemma1.lean).