Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
2026-06-03 • Computation and Language
Computation and LanguageLogic in Computer Science
AI summaryⓘ
The authors studied how large language models can help prove math theorems in the Lean system by breaking problems into smaller parts and trying many solutions. They created an agent with two parts: one that generates and attempts proofs, and another that learns from failed attempts to decide whether to keep trying or try a new approach. This method saves about 25.8% of computing effort without reducing success rates. Their work shows that information from failed proof attempts can help smartly manage proof search resources.
Large Language ModelsLean Theorem ProverFormal ProofLemma DecompositionProof SearchFailed Proof AttemptsCost-aware SearchAgentic Theorem ProvingPutnamBenchNatural Language Formalization
Authors
Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck, Martin Vechev
Abstract
Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proof attempts, and use compiler feedback to guide search. However, they can be prohibitively expensive, often spending substantial compute on attempts that ultimately fail. In this work, we address this problem with an action routing agent that consists of a data plane and a control plane. The data plane generates natural-language lemma decompositions, formalizes them in Lean, and samples proof attempts for the resulting theorem and lemma targets. The control plane observes previous failed Lean attempts, estimates both the likelihood of success and cost of another attempt, and decides whether to continue proving the current target or restart from a new breakdown. On a subset of PutnamBench, our agent decreases the cost by $25.8\%$ over a fixed-step baseline on average, preserving performance while using substantially less compute. These results suggest that failed Lean trajectories provide actionable signals for cost-aware resource allocation in agentic theorem proving.