Driving Claude Code on Hard Proofs

Workflow lessons from a multi-session, multi-agent Rocq proof effort (the wp transitivity work). About how to collaborate with an AI proof assistant on a genuinely open problem — independent of the mathematics.

The big one: do not arm a blocking Stop-hook on an open research goal

A session Stop-hook set to “progressively achieve admit-free in @file” fired ~10 times in a row on the 06-05 session, each round rejecting “support lemmas added, but the blocking admit’s assumption count is unchanged.” The model burned a large fraction of a 1M context restating the same honest status. The hook cannot distinguish “the model is stalling” from “the goal is not closable this turn.”

Lesson: forcing-function hooks work for closable tasks. For a goal whose closability is itself the open question, a blocking hook produces coercion-loops, not progress. Progress resumed the instant the human switched from coercion to a generative prompt: “find a counterexample that actually breaks wp_trans, otherwise think why it holds and prove it.” That reframe produced the key result (the wall is a proof-strategy artifact, not an incompleteness). Belongs in a global proof-framework rule.

Manager / prover discipline

• Keep the open keystone in the main thread; delegate only boxed, falsifiable tasks. Subagents were excellent at falsification (machine-checked counterexamples) and bounded infrastructure, but poor at the open keystone (~5 prover sessions, the hard lemma still open). The human’s instinct — “don’t call subagents on a hard proof, they lose information / hallucinate” — matched the cost data.
• A prover returning PROVED against a possibly-false admit is a real, dangerous event. One prover honestly closed a downstream lemma given an admit that was itself inconsistent; only the manager’s independent witness-test caught it. Every newly-introduced admit must be sanity-checked against a known witness before anything is built on it.
• Never rubber-stamp a prover-suggested helper. The “v3 went wrong because the manager accepted prover-suggested helpers that drifted from the plan” pattern recurred (the “uniform B” drift). Lemma identification is the manager’s job; provers report stuck points in prose only.
• The “materialize-STUCK-as-Admitted-helper” policy causes hole-shuffling and overclaiming. Each iteration produced a new sub-helper with the same gap and a sharper signature — no real content. Prefer: prove, or return prose-stuck; do not convert stuck points into admits to defer.

How the human steered effectively

• Demand expanded statements in math/subtyping notation, not Rocq names. Repeatedly, “explain human-readable, expand the real statement” surfaced errors the lemma-name-level discussion hid, and is where the actual design decisions were made.
• Paper proof first, then mechanize. A *_DRAFT.md + sign-off before Coq cycles; every design fork was a math decision that wasted Coq time if taken early.
• Anchor to the fixed plan; do not re-derive and drift. The model repeatedly slid back to an approach the human had explicitly killed rounds earlier (“I genuinely lost the thread”). When a plan is fixed, re-read it verbatim each round.
• Tag before risky writes; trust git to make big reverts cheap. Frequent milestone commits + a checkpoint tag made a v3→v4 deletion and a false-Qed revert safe.
• Put durable state in files (REPORT.md, PLAN_V4.md, PROOF_TODO.md), not re-pasted into chat — long specs pasted 5–7×/turn inflated context badly.

Model failure modes to watch

• Over-asserts on semantic/metatheory questions where it lacks ground truth (claimed several false counterexamples / “unsound” verdicts, each retracted after a human counterexample). Flag confidence; defer semantic facts; verify in MCP.
• Effort estimates systematically too low (“one focused session” repeated ~5×). When a proof keeps revealing a deeper foundation lemma at every step, that is a signal the architecture is fighting the formalization — step back and redesign, don’t push.
• Pessimism↔optimism oscillation: conceded the headline “unreachable” twice when it was a witness-construction artifact; found the path the moment it was pushed.

Related

Proof Engineering Lessons (Rocq wp_isorec) · wp Transitivity via Cover Routing

Sources

Claude Code sessions 271dc5fa (06-04), ed9a9e97 (06-04), 11cf3241 (06-05), and the earlier arc.