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

Kári Rögnvaldsson, Chenhao Sun, Jasper Dekoninck +1

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 proo…