Mathematicians value proofs for more than mere correctness; simplicity, purity, and the computational cost of finding a proof matter as well. Current LLM‑driven theorem provers typically search for any correct proof and improve its quality only after it is found. LEVER introduces a programmable objective that is optimized during the search itself. It scores partial proofs on an AND/OR proof graph by merging realized objective values with predictions for open subgoals, allowing the objective to guide the search before a full proof is assembled. The same mechanism can minimize computational cost, proof length, topical impurity, or any weighted combination, while the Lean kernel guarantees formal correctness. On the Lean 4 PutnamBench suite, under equal budgets, LEVER reduces computational cost by 34% compared to a strong single‑conversation agent and raises the solve rate from 80% to 96%. When reducing topical impurity—how far a proof strays from its theorem’s subject—LEVER achieves a 42% reduction versus 33% for post‑hoc refactoring, at two‑thirds of the cost and with greater reliability; for proof length, the metric it is built for, LEVER approaches the performance of refactoring. Varying the objective’s weights traces a quality‑cost trade‑off curve, letting users decide 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.
Review