Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification

1 Introduction

• Formal proofs provide machine-checkable correctness guarantees that finite testing cannot offer, but proof generation remains harder than code generation in recent benchmarks.The paper identifies proof generation as a bottleneck for program verification and verified code generation.Source: §1 · p. 1
• Hundreds or thousands of interdependent proof obligations make the success–vs–cost frontier—the trade-off between proof success and expenditure—a natural objective for repository-scale verification.The frontier compares success under matched cost limits and cost at matched success.Source: §1 · pp. 1–2
• Code proofs follow task-specific program definitions, and while many obligations are routine, a few difficult semantic discoveries can determine whether the proof succeeds.Examples include finding a loop invariant or a sufficiently generalized induction hypothesis.Source: §1 · p. 2, Figure 1 · p. 2
• CoCo-Prover formalizes proving as metalevel decision-making under cost and uses a two-level proof graph to adapt orchestration as evidence accumulates.Its decisions include what to prove next and whether to use automation, direct proof generation, a helper lemma, or recovery.Source: §1 · pp. 2–3
• No baseline exceeds CoCo-Prover’s solve rate on any benchmark and backbone; it solves up to 100% of function-level benchmarks and cuts cost by up to 30.9% against Humanize on GPT-5.6-Terra.The evaluation covers five Lean benchmarks and three frontier LLMs under matched caps.Source: §1 · p. 3

2 Related Work

• Fine-tuned provers buy success through repeated sampling, while refinement agents still use fixed per-theorem iteration budgets; CoCo-Prover instead treats each bounded invocation as best-effort and resamples only when evidence changes.Structured provers can require coarse rollback or rarely share helper lemmas across targets, whereas CoCo-Prover’s persistent graph supports finer rollback and reuse.Source: §2 · p. 3
• Code provers inherit limitations of both modes: some search each obligation under a flat timeout, while others use per-lemma trees, flat lemma corpora, or task-isolated decomposition.The paper contrasts these approaches with CoCo-Prover’s persistent two-level graph and adaptive orchestration.Source: §2 · p. 3
• Query routers and budget-aware search operate on isolated queries, while formal-reasoning routers and training methods do not choose both an obligation and a proof strategy.Danus uses homogeneous general-purpose agents and makes no cost decision over its fact graph.Source: §2 · p. 3

3.1 Problem Formulation

• The formulation chooses which goals to work on and which strategy and configuration to buy, measuring cost globally because an expensive helper lemma may reduce work across several goals.Adaptive routing is beneficial when the avoided decision regret exceeds the routing inference overhead.Source: §3.1 · pp. 3–5
• A two-level graph records verified steps and resulting subgoals within declarations, while linking target and helper lemmas across declarations to preserve partial progress and track dependencies.The within-declaration AND/OR hypergraph is paired with a lemma-dependency DAG.Source: §3.1 · p. 4, Figure 2 · p. 4
• An incremental topological scheduler exposes open goals whose active prerequisites are ready, restricting the action space without spending model computation.Goals depending on provisional lemmas may proceed while those dependencies remain tracked for rollback.Source: §3.1 · p. 4
• Each purchased computation selects a goal group, specialist, and configuration, and incurs outcome-dependent cost; the objective balances task completion against total realized cost.The router’s inference cost is accounted for separately, and the paper treats λ as normative rather than computing it explicitly.Source: §3.1 · p. 4

3.2 System Design of CoCo-Prover

• The evidence-grounded router clusters the dependency-ready frontier, selects a specialist and budget using proof states and execution history, and may revise routing rules as outcomes accumulate.The router can favor a helper lemma when its expected total task cost is lower than proving several goals directly.Source: §3.2 · p. 5, Figure 3 · p. 5
• Four specialists handle automation, iterative proof writing, helper-lemma planning, and recovery; recovery can discard only work that depends on the failed path.The Lemma Planner adds candidates only after elaboration and acyclicity checks, and the Recovery Reviewer’s cheaper-route judgment is not certified optimal.Source: §3.2 · pp. 5–6

4 Evaluation

• The evaluation includes a budget sweep and component ablations in addition to solve-rate comparisons.Further setup and results are reported in the appendices.Source: §4 · p. 6
• The five benchmarks span function-level code verification and repository-level obligations derived from upstream repositories.CLEVER and AlgoVeri use generated, manually checked implementations; NTP4VC is evaluated on its first 300 tasks in alphabetical order.Source: §4 · p. 6
• Comparisons use three frontier LLMs and three baseline families under identical backbones, providers, and caps.Repository-level comparisons include only coding agents because Ax-Prover-Base and Humanize do not handle repository-scale dependency structure.Source: §4 · p. 6

4.1 Performance

• No baseline exceeds CoCo-Prover’s solve rate in any benchmark–LLM pair.The table covers function- and repository-level benchmarks; a task counts as solved only when Lean accepts the root declaration without generated axioms.Source: §4.1 · p. 6, Table 1

Method CLEVER VERINA AlgoVeri CLEVER VERINA AlgoVeri CLEVER VERINA AlgoVeri

• CoCo-Prover reaches 100% on CLEVER and VERINA, ties Humanize on Gemini-3.5-Flash AlgoVeri, and solves up to 60.5% on Vero versus coding agents’ 7.0% maximum.Vero tasks share repository definitions and helper lemmas.Source: Method CLEVER VERINA AlgoVeri CLEVER… · p. 7
• On commonly solved problems, CoCo-Prover costs less in all nine function-level pairs, with savings up to 85.7% against Ax-Prover-Base.The one cheaper-baseline case is Vero with GPT-5.6-Terra, where Codex solves a single shared task.Source: Method CLEVER VERINA AlgoVeri CLEVER… · p. 7, Table 2 · p. 8
• 419 problems are reached by CoCo-Prover under GPT-5.6-Terra, while Codex and Ax-Prover-Base gain relatively few solves beyond roughly $5 per problem.Figure 4 plots solved problems against the per-problem budget, summed over 427 problems across CLEVER, VERINA, and AlgoVeri.Source: Method CLEVER VERINA AlgoVeri CLEVER… · p. 7, Figure 4 · p. 9

4.2 Ablation Study

• On 30 randomly selected problems, removing the router raises cost 39.9%; removing the Lemma Planner raises cost 41.6% and leaves 27 of 30 solved.The router ablation also loses one VERINA problem; without lemma planning, goals are proved in isolation.Source: §4.2 · p. 8, Table 3 · p. 9
• Removing automation raises cost 11.5% on CLEVER and 12.4% on VERINA, but lowers it 5.8% on AlgoVeri.Automation often closes goals mechanically on CLEVER and VERINA, but can split AlgoVeri algorithmic goals into meaningless subgoals.Source: §4.2 · p. 9

5 Conclusion

• Across five Lean benchmarks and three backbones, CoCo-Prover achieves the highest solve rate in any setting and reduces cost on commonly solved problems by up to 30.9% against Humanize.The conclusion also attributes advantages to shared-lemma discovery and adaptive routing.Source: §5 · p. 9

A Additional Theoretical Analysis

• The analysis reports reachability preservation, possible strict gains in attainable value, assumption-dependent optimality of hard filters, helper sharing that can save a factor K, and kernel-sound returned proofs.It assumes, but does not show, that deployment realizes the finite abstraction.Source: A Additional Theoretical Analysis · p. 14

A.1 The metalevel process

• The state tracks the proof graph, frontier, and accumulated records; the scheduler supplies the dependency-ready frontier, and the router selects grouped computations from it.The admissible computation includes a goal group, an operation, and its configuration.Source: §A.1 · p. 14
• Each purchased computation returns a specialist output and Lean verdict, incurs execution cost, and updates the state; router deliberation is separately charged and does not alter that state.Total spending counts execution charges and the router's inference cost.Source: §A.1 · p. 15
• The analysis assumes Markov outputs, bounded computation costs, deterministic verifier updates, and proper policies; solved states are absorbing, while the implementation's iteration limit enforces properness.Free computations are possible, so proper policies must reach an absorbing state with probability one and finite expected time.Source: §A.1 · p. 15
• The evaluation reports capped solve fraction and cost on commonly solved problems, while the protocol targets a small positive λ where success dominates and cost distinguishes comparable prospects.The external cap is not given to the controller, and the normative value is not estimated.Source: §A.1 · pp. 15–16
• For proper policies with finite reachable states and finite computation sets, all sufficiently small positive λ induce a fixed ordering that first maximizes attainable success, then minimizes expected remaining cost.The ordering follows from the finite piecewise-linear policy values and their finitely many breakpoints.Source: §A.1 · p. 16
• A paid computation that closes remaining work is maximal only when its cost satisfies κc ≤ pc J*(s); a bounded contract restricts actions without establishing that returning preserves value.Retaining partial work can still add return overhead, so the contract is not claimed to be free.Source: §A.1 · p. 16

A.2 Regret decomposition: proofs of Theorem 1 and Corollary 2

• Routing outperforms a fixed routine exactly when the continuation-value regret it avoids exceeds its extra decision-making cost.The regret decomposition also characterizes cost efficiency as allocating purchased computations with low cumulative regret.Source: §A.2 · p. 17

A.3 Faithful two-level graph states preserve reachability

• Every certificate reachable by primitive Lean steps remains reachable in the two-level graph representation at the same primitive cost.This equivalence assumes corresponding transitions and solved states are preserved and step costs are unchanged.Source: §A.3 · p. 18

A.4 Graph information raises the attainable value

• Graph-informed routers weakly dominate target-local routers when they can use extra graph inputs at no additional inference cost.The appendix also constructs a two-instance separation where consumers that look alike locally require different helper-lemma choices globally.Source: §A.4 · pp. 18–19

A.5 Safe filtering

• The hard filters remove repeated deterministic no-progress work and root-disconnected work; safe deferral additionally requires erasability and postponement conditions.Semantic choices not certified as safe remain with the router under bounded trials.Source: §A.5 · pp. 19–20

A.6 Shared-lemma cost separation

• When ch > 0 and every di = 0, the stipulated isolated-to-shared cost ratio is K, but this compares two specified strategies rather than all strategies each representation admits.The isolated strategy pays to generate the helper separately for each consumer, while the graph strategy proves it once.Source: §A.6 · p. 20

A.7 Kernel-relative soundness

• A returned stable proof of ℓ entails Γ0 ⊢ ℓ only if the environment is accepted, generated dependencies are stable, Lean accepts the proof, and prohibited placeholders or unapproved axioms are absent.The proof proceeds by topologically ordering the generated dependency DAG.Source: §A.7 · p. 21

B.1 Two-level proof graphs

• Each declaration has an AND/OR proof hypergraph, while a DAG links declarations through helper-lemma dependencies; artifact status distinguishes provisional plans from stable proofs.Stable helpers can serve multiple consumers, while a failed provisional helper invalidates its conditional descendants rather than discarding unaffected verified subgraphs.Source: §B.1 · p. 21

B.2 End-to-end algorithm

• Each epoch builds the dependency-ready frontier symbolically, groups goals, and routes one priced specialist action before writing verified results and status updates back.Definition-nested goals go directly to automation when admissible; bounded retries and a deterministic fallback keep router deliberation finite.Source: §B.2 · pp. 22–23

B.3 Dependency-aware scheduling

• An incremental Kahn pass admits open goals only after prerequisites are elaborated, excludes root-disconnected work, and orders the frontier by stability readiness.Retraction reopens conditional descendants and restores counters only in the affected region.Source: §B.3 · p. 24

B.4 Goal clustering by semantic embedding

• The router batches semantically related frontier goals using k-means on normalized Lean-statement embeddings, with deterministic clustering as the frontier changes.Batching can reduce invocation costs, while shared-helper proposals draw evidence from multiple potential consumers.Source: §B.4 · p. 24

B.5 Sharing and rollback accounting

• Sharing is cost-saving when the one-time helper cost plus residual work and failed-attempt or rollback costs is below isolated rediscovery cost.The dependency graph also measures provisional-artifact exposure through the conditional descendants that would need revalidation.Source: §B.5 · p. 25

B.6 Message passing between the router and the action agents

• The chosen action agent continues the router’s conversation and preliminary analysis, allowing the shared prompt prefix to use cached-input pricing.The ledger records cached and uncached input tokens separately so the cost effect is measured.Source: §B.6 · p. 25

B.7 Structural checking of proposed lemmas

• Proposed helpers face free random testing first and model-proposed structured tests only if they pass; counterexamples trigger revision, while passing tests never establish stability.Only Lean acceptance promotes a declaration to stable.Source: §B.7 · pp. 25–26

C.1 Additional Explanation of Experiment Setup

• All methods share provider backbones and external caps; costs convert model-call token counts to dollars under one price schedule, including peak-hour DeepSeek rates.Function-level tasks are capped at five hours and $30, and repository-level tasks at eight hours and $60.Source: §C.1 · p. 26, Table 4 · p. 26
• Hilbert’s header assumption mismatches program-verification tasks; Goedel-Code-Prover failed within $5 under pass@1, while WybeCoder and P3 target jointly generated code and proofs.The paper therefore excludes these systems from its comparisons for distinct setting or protocol reasons.Source: §C.1 · pp. 26–27
• Every reported solve rate and cost counts only proofs passing five checks, including mechanical validation, automated review, and random manual audits.The checks reject unresolved goals, altered statements, and new axioms, among other concerns.Source: §C.1 · pp. 27–28

C.3 Discussion of DeepSeek Model on Baselines

• DeepSeek’s long reasoning and accumulated transcripts lead baselines to time out or decline after spending; CoCo-Prover bounds each invocation and gives specialists goal-local context.The paper attributes the widest baseline gap to scaffolds that ask for a proof in one turn from a long context.Source: §C.3 · pp. 28–29

C.2 Per-Problem Cost and Time

• About $30 versus about $13 per problem marks the Gemini coding-agent versus CoCo-Prover high-cost tails; CoCo-Prover’s mean time is higher on GPT and Gemini but lower on DeepSeek.At comparable wall-clock times, CoCo-Prover’s solved-problem points lie below the coding agents’ on the cost axis.Source: §C.2 · p. 28, Figure 5 · p. 29

C.4 Run-to-Run Variance

• $969.8 average total cost with $89.5 standard deviation (9.2% CV) across three Gemini-3.5-Flash runs; all 427 problems had identical solved sets each run.The reported cost gaps exceed this run-to-run spread by about an order of magnitude.Source: §C.4 · p. 29
• Six of nine ablation-subset cells have CV below 9%; the largest are 34.2% for AlgoVeri with GPT-5.6-Terra and 22.0% for CLEVER with DeepSeek-V4-Flash.The AlgoVeri spread reflects differing proof lengths, while DeepSeek’s high relative variation comes from a small $0.93 standard deviation against low cost.Source: §C.4 · p. 29, Table 7 · p. 30
• Router and Lemma Planner ablations exceed run-to-run noise at 39.9% and 41.6% above the complete system; the 5.8% automation effect is comparable to noise.Gemini-3.5-Flash complete-system CVs range from 2.4% to 8.3%.Source: §C.4 · p. 29

C.5 More Component Ablation Discussion

• The graph cannot be ablated as an independent component because it defines the state for goal selection, dependency tracking, lemma sharing, and reopening descendants after retraction.The passage says the graph comparison is instead the baseline comparison in Section 4.1, with case studies in Section D illustrating its effects.Source: §C.5 · p. 30
• Ablating written adaptive rules would still allow implicit adaptation, so it would test rule documentation rather than adaptation; replacing adaptive choice with a fixed order raises cost by 39.9%.A null or positive result from removing written rules would not isolate adaptation from rule tokens added to each evidence packet.Source: §C.5 · p. 30

D Case Studies

• CoCo-Prover’s two case studies contrast a one-obligation function-level cost question with a repository-level provability question involving 56 interdependent obligations.Source: D Case Studies · p. 30

D.1 CLEVER prob 15: a function-level cost comparison

• $2.36: CoCo-Prover proves CLEVER prob 15, versus $8.67 for Codex and $10.74 for Humanize; Ax-Prover-Base spends $5.48 and fails.All four systems use GPT-5.6-Terra at the same provider prices and evaluation caps.Source: §D.1 · p. 30, Table 8 · p. 31

D.1.1 The task

• CLEVER prob 15 requires proving that splitting the space-intercalated output recovers the number sequence, linking string operations, character lists, and Lean’s byte-level scanner.The passage notes that Lean 4 core lacks the needed string-level round-trip theorem and that the proof also needs to establish that Nat.repr contains no spaces.Source: §D.1.1 · p. 31

D.1.2 Head-to-head outcome

• The successful baselines reach essentially the same mathematics as CoCo-Prover, making their 3.7×–4.5× cost gap organizational; Ax-Prover-Base identified missing facts but could not make blockers separately provable goals.Table 8 describes the baselines’ different cost patterns: repeated context reads for Codex and Humanize, and output-heavy re-derivation for Ax-Prover-Base.Source: §D.1.2 · p. 31, Table 8 · p. 31

D.1.3 How CoCo-Prover proved it

• CoCo-Prover’s proof took 8 controller iterations and 18 routed invocations, with no backtracks, retracted lemmas, or rejected scripts; its successive lemmas descended from the specification to UTF-8 offset arithmetic.Each lemma was proposed and proved once, and every Proof Writer invocation closed its target.Source: §D.1.3 · pp. 31–32, Table 9 · p. 32, Figure 6 · p. 32
• For UTF-8 offset arithmetic, the Proof Writer reduced position equality to byte-index equality, computed singleton advancement, and canceled the subtraction with Nat.add_sub_cancel.It then added String.Pos.Raw.mk_zero and Nat.zero_add to the planned simp list.Source: §D.1.3 · pp. 36–37
• The Lemma Planner decomposed subgoals into lower-level lemmas, while the Proof Writer reasoned mathematically and used existing library facts, adding lemmas only for missing facts.Examples of reused facts include String.splitOnAux.induct and String.next of valid.Source: §D.1.3 · p. 37

D.1.4 How the baselines spent their budgets

• 27.08M prompt tokens, including 26.68M cache reads, accompanied Codex's $8.67 proof; CoCo-Prover used 2.54M prompt tokens over 161 calls.Codex resent the full transcript at roughly 140k prompt tokens per step, compared with 15.8k per CoCo-Prover call; the mathematics was the same, making context management the stated difference.Source: §D.1.4 · pp. 37–38
• 84% of Humanize's $10.74 total went to eight failed rounds, which repeatedly rediscovered obstacles before proving the task on round nine.A separate run also proved the task for $6.01 over three rounds, still 2.5× CoCo-Prover's cost; CoCo-Prover proved a checked lemma for one named blocker for $0.037.Source: §D.1.4 · p. 38
• 49 of Ax-Prover-Base's 50 builds failed to compile across more than 50 iterations and 151 LLM calls, and it exhausted its iteration limit.Its monolithic attempt repeatedly reproved inline blockers, while CoCo-Prover proved corresponding lemmas separately; working proof parts were not retained, and $4.33 went to output.Source: §D.1.4 · pp. 38–39

D.1.5 Why CoCo-Prover is cheaper

• CoCo-Prover's cost design combines bounded contexts, persistent verified progress, and checked helper lemmas for blockers.It also spends more reasoning on planning than script synthesis, runs deterministic automation before model calls, and tests proposed lemmas before relying on them.Source: §D.1.5 · p. 39

D.2 Vero prob 14: interval-set algebra, 56 specifications

• All 56 Vero prob 14 targets were proved, versus 5 of 56 for the coding-agent baseline on the same backbone LLM.The final 2,471-line proof passed Lean with no sorry, no axioms beyond Lean's standard ones, and unchanged target statements.Source: §D.2 · p. 39, Table 12 · p. 41

D.2.1 The task

• The 56 targets cover overlaps, mergeOverlaps, and chop, while their specifications use frozen point-set and canonical-form predicates.The task combines distinct recursion schemes, semantic specifications unlike the implementation structure, global uniqueness and permutation targets, and shared structure across many theorems.Source: §D.2.1 · pp. 39–41

D.2.2 Outcome

• About $19 of model usage completed the run, roughly $0.35 per target theorem.The run accepted 56 helper lemmas after counterexample checks; 55 appear in the final proof and one was unnecessary.Source: §D.2.2 · p. 41, §D.2.3 · p. 41

D.2.3 How CoCo-Prover proved all 56 targets

• By iteration 34, the run had proved all 111 declarations: 56 targets and 55 helper lemmas.Across 175 routed invocations, deterministic automation closed 24 goal nodes and partially scripted 59; the controller also made 52 reasoned backtracks.Source: §D.2.3 · p. 41
• For most non-trivial targets, the planner split proofs into insertion, sorting, and coalescing lemmas, using induction suited to each recursion scheme.Targets were then closed by rewriting with those layer lemmas rather than unfolding the implementations.Source: §D.2.3 · p. 41

D.2.4 Key proof episodes, with Lean code

• Coverage and canonical-form targets center on merge coverage and merge disjointness, used directly by 15 and 11 declarations, respectively.Both targets reduce to lemmas about the sorting and coalescing layers.Source: §D.2.4 · p. 42
• Coalesce coverage required functional induction with the point and sortedness invariant reverted, after automation’s unfolded case splits lacked an induction hypothesis.The resulting lemma preserves coverage for a pairwise-lo-sorted interval list; sorting coverage then lifts insertByLo coverage through the fold.Source: §D.2.4 · p. 42
• A counterexample rejected the claim that insertByLo always outputs nonempty intervals: inserting an empty interval into a list containing one leaves it there.The planner added the required invariant that the input list contains only nonempty intervals; the resulting sortByLo_output_nonempty lemma is used directly by 7 declarations.Source: §D.2.4 · pp. 43–44
• The canonical-form proof establishes that coalescing sorted, nonempty intervals yields a disjoint sorted nonempty list through four-case functional induction.Its gap case uses a reusable lower-bound lemma to show the coalesced tail begins beyond the preceding interval.Source: §D.2.4 · pp. 44–45
• Two canonical interval lists covering the same points are equal, proved by matching head endpoints and applying induction to tails with equal coverage.The lemma supports the uniqueness, determination, and permutation-invariance targets, each of which then follows in a few lines.Source: §D.2.4 · p. 46
• Coverage extensionality turns permutation and reversal invariance into semantic proofs, avoiding reasoning about how insertByLo handles ties.Equal coverage determines equal canonical outputs, and reversal invariance follows by applying permutation invariance to a reversed list.Source: §D.2.4 · pp. 48–49
• A bridge lemma matched the automation-unfolded goal, while all 52 backtracks returned to a safe abstract node and recorded why the abandoned path failed.The deepest fixpoint target is at dependency depth 6 and combines chopping-preserved canonicity with merging a canonical list as the identity.Source: §D.2.4 · pp. 49–50

D.2.5 Dependency relationships

• The 111-declaration dependency graph reaches depth 6; 10 of 56 targets close at depth 0, while the rest have depths 1–6 and one to four direct dependencies.The layers progress from single-step facts through lifted and sortedness results to central targets and their consequences.Source: §D.2.5 · p. 50

D.2.6 What made all 56 provable

• Decomposition, recursion-matched induction, semantic lemmas, target reuse, and checked backtracking made all 56 targets provable.The sortByLo output-nonempty and sortedness-certificate lemmas were reused by 31 and 28 targets, respectively; seven proved targets also served as dependencies.Source: §D.2.6 · pp. 50–51, Table 14 · p. 51

E Prompt Templates

• Appendix E lists the prompt templates for the agents shown in Figure 3 and described in Section 3.2.Source: E Prompt Templates · p. 51

System Prompt

• The System Prompt frames proving as proof-tree exploration with unresolved sorry goals and supplies annotated theorem dependencies and declaration-scoped prefixes for resolving private Lean workers.The header prefix makes private worker names available within the declaration, allowing proofs to refer to them when unfolding definitions.Source: System Prompt · pp. 51–52

Agentic Router Prompt

• The Agentic Router Prompt gathers tactic states, proof snapshots, and proposed lemmas, then routes each goal to a specialist with a configuration under the routing rules.The router is instructed to distinguish verified lemmas from unproved proposals when selecting dependencies.Source: Agentic Router Prompt · pp. 52–53

Lemma Planner Prompt

• The Lemma Planner favors reusable, general, self-contained lemmas and requires explicit side conditions and dependency annotations.It advises checking edge cases before proposing a lemma and recording every intended consumer in the dependency graph.Source: Lemma Planner Prompt · p. 53
• The Lemma Planner requires complete, noncircular dependency annotations and adds lemmas sequentially, with helper definitions used sparingly.A helper definition must be complete and introduced before lemmas that use it, because it changes the Lean context for later steps.Source: Lemma Planner Prompt · p. 53

Proof Writer Prompt

• The Proof Writer emits only tactics for the open goal, uses confirmed library names, and verifies the code before submitting it once.Search tactics are for discovery only; the writer must replace suggestions with concrete lemmas and submit exactly the candidate that passed checking.Source: Proof Writer Prompt · pp. 53–54

Recovery Reviewer Prompt

• The Recovery Reviewer backtracks only when a node is unprovable or clearly much harder, using evidence and preferring the nearest viable prior node.Unprovability requires counterexamples that satisfy the hypotheses and falsify the goal; a hard-case rewind must explain the difficulty.Source: Recovery Reviewer Prompt · p. 54
• Lemma abandonment is reserved for strong evidence that a lemma is unprovable or very hard and unnecessary, while failure memory prevents retrying rejected paths or strategies.Abandonment also discards every proof path using the lemma, and the top theorem cannot be abandoned.Source: Recovery Reviewer Prompt · p. 54

• Repository-scale lemma-reuse evidence covers only two repository-level benchmarks, fewer tasks than the function-level comparison.Source: F Limitations · pp. 54–55
• The evaluation covers Lean 4 only; CoCo-Prover is not implemented on Rocq or Isabelle/HOL.Source: F Limitations · p. 55
• Implementations and specifications are fixed inputs because CoCo-Prover operates only on proofs as a theorem prover.Source: F Limitations · p. 55
• The theory does not prove that the implemented LLM router must attain low regret; it explains when orchestration pays off.Source: F Limitations · p. 55
• Routing, lemma proposal, planning, and recovery depend on backbone-model semantic judgment, while symbolic guards are syntactic.Source: F Limitations · p. 55
• Under GPT-5.6-Terra and Gemini-3.5-Flash, mean wall-clock time exceeds coding agents; reported cost excludes local computation and depends on provider caching.Source: F Limitations · p. 55