Before Lean Checks: Candidate Exposure in Proof-Action Ranking

Formal proof agents do not fail only when they cannot finish a theorem; they can fail earlier, when ranking hides the tactics Lean would have accepted. This paper studies that pre-check handoff: which proof-state representations and family priors keep useful candidate tactics inside the short list sent to Lean? We separate inputs visible before the next action from future-tactic metadata, then compare unguided retrieval, hard family routing and a soft family prior on a curated mathlib4 subset. Trace matches suggest that soft family guidance is competitive with unguided retrieval and that hard routing loses alternatives. A 500-state Lean check gives the more consequential picture: unguided retrieval has the strongest top-five Lean acceptance, while soft guidance is close but not better. The result reframes family prediction as a ranking-control problem: useful proof agents should surface several legal next moves for Lean, not merely imitate one recorded trace step.