Reproduce “Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Shuangjie Yao, Nikolaus Holzer, Mark Paul Santolucito, Baishakhi Ray, Suman Jana, Dongdong She
CoCo-Prover allocates proof work across software verification obligations while retaining progress and reusable helpers. It tracks open goals and dependencies, then routes ready goals to automation, proof-writing, lemma-planning, or recovery agents; Lean accepts proofs. On CLEVER with GPT-5.6-Terra, it and Humanize solved 157 shared tasks, at $94.4 versus $136.6 total model-call cost; this excludes tasks either system failed.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.