Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean

A new action routing agent for the Lean theorem prover cuts computational costs by 25.8% without sacrificing accuracy, according to research posted to arXiv. The system uses a lightweight control plane to decide when to abandon unpromising proof attempts, preserving performance while using substantially less compute. Large language models are increasingly deployed in workflows that generate formal proofs in Lean, a proof assistant used to verify mathematical theorems [1]. These workflows typically decompose problems into smaller lemmas, sample many proof attempts, and rely on compiler feedback to guide the search [1]. The approach, while effective, is often prohibitively expensive because substantial compute is spent on attempts that ultimately fail [1]. To address this, the researchers designed an agent architecture that separates proof generation from resource allocation [1]. A data plane generates natural-language lemma decompositions, formalizes them in Lean, and samples proof attempts for the resulting theorem and lemma targets [3]. A control plane observes the prior proof trajectory and uses a lightweight model to estimate both the success probability and the cost of the next attempt [3]. Based on a target cost-quality tradeoff, it dynamically determines whether allocating further compute is worthwhile [3]. The work adapts and extends existing research in the routing and cascading literature to the setting of Lean theorem proving with agentic workflows [3]. By learning to identify low-value attempts early, the agent can stop early or restart, significantly reducing unnecessary computation while preserving performance [3]. The architecture is conceptually inspired by prior work, including Chen et al. (2025c), which informed the data plane’s lemma-style proof generation [3]. On an 85-problem subset of PutnamBench, a benchmark for mathematical reasoning, the dynamic routing approach significantly outperformed a fixed-step baseline across multiple cost-quality metrics [3]. On average, the agent reduced the required budget by 25.8% at parity accuracy and achieved a 7.8% improvement in accuracy at parity cost [3]. The results indicate that fixed-step policies leave considerable room for efficiency improvements [3]. The routing strategy builds on principles from mechanism design, a branch of economics and game theory that studies how to construct rules that produce good outcomes according to a predefined metric, even when the designer does not know the players’ true preferences [6]. Mechanism design has broad applications, including in networked systems and online auctions, and has been recognized with the 2007 Nobel Memorial Prize in Economic Sciences [6]. In the context of automated theorem proving, the control plane acts as a mechanism that allocates computational resources based on observed signals from failed Lean trajectories [1]. Separate research on Lean refactoring has explored complementary efficiency gains. Lean Refactor, a retrieval-augmented agentic framework, externalizes refactoring knowledge into a structured database annotated with metadata such as expected compilation-cost reduction and Lean version compatibility [5]. By dynamically filtering and reranking strategies at inference time, that framework steers proof optimization toward user-specified objectives without model fine-tuning [5]. The action routing agent’s focus on cost-aware resource allocation represents a parallel path toward making agentic theorem proving more practical [1].