Lever: Online Optimization of Quality During Proof Search

We propose Lever, a proof search algorithm that optimizes proof quality objectives, including and beyond mathematical correctness. We model the space of proofs as an AND/OR directed acyclic graph, where OR and AND nodes represent theorems (goals) and their decomposition into sub-goals (plans) respectively. Starting from a target theorem, Lever incrementally grows this graph using LLMs, preferring modifications that are likely to reduce a chosen objective. Our framework is general: any objective that composes over the graph can be optimized during search rather than repaired afterwards. This optimization uses guidance from per-metric value functions that are initialized from LLM priors and updated online as evidence accumulates during search. We first show that graph-based proof search is competitive with LLM agents performing flat proof search. We then show that Lever optimizes proof-quality metrics such as computational cost, proof size, and topical purity, more effectively than agentic and post-hoc refactoring baselines. Finally, Lever can be steered along the trade-off between conflicting objectives, tracing a Pareto frontier rather than committing to a single proof strategy.