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

arXiv: https://arxiv.org/abs/2606.04883 · HTML: https://mlsanity.com/paper/2606.04883/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 24 of its 31 references that are in the map.
- First posted on arXiv 3 Jun 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 24 of 24)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [FrugalGPT: How to Use Large Language Models While Reducing Cost and Improving Performance](https://mlsanity.com/paper/2305.05176/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Hybrid LLM: Cost-Efficient and Quality-Aware Query Routing](https://mlsanity.com/paper/2404.14618/) (2024)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [AutoMix: Automatically Mixing Language Models](https://mlsanity.com/paper/2310.12963/) (2023)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [MasRouter: Learning to Route LLMs for Multi-Agent Systems](https://mlsanity.com/paper/2502.11133/) (2025)
- [A Unified Approach to Routing and Cascading for LLMs](https://mlsanity.com/paper/2410.10347/) (2024)
- [Learning to Route LLMs with Confidence Tokens](https://mlsanity.com/paper/2410.13284/) (2024)
- [When Does Confidence-Based Cascade Deferral Suffice?](https://mlsanity.com/paper/2307.02764/) (2023)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Optimizing Model Selection for Compound AI Systems](https://mlsanity.com/paper/2502.14815/) (2025)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [Optimising Calls to Large Language Models with Uncertainty-Based Two-Tier Selection](https://mlsanity.com/paper/2405.02134/) (2024)
- [Tryage: Real-time, intelligent Routing of User Prompts to Large Language Models](https://mlsanity.com/paper/2308.11601/) (2023)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [ACAR: Adaptive Complexity Routing for Multi-Model Ensembles with Auditable Decision Traces](https://mlsanity.com/paper/2602.21231/) (2026)

## Built on by (most cited first, 3 of 3)

- [BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://mlsanity.com/paper/2607.28110/) (2026)
- [Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification](https://mlsanity.com/paper/2610.09681/) (2026)
- [LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs](https://mlsanity.com/paper/2610.11862/) (2026)

## Abstract (arXiv)

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 the 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 28.9% 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.