JEPA 表征在 Lean 一步状态排序上更准，却没有提升长程证明搜索

该工作把 LeanDojo 一步转移作为自监督信号，用 JEPA-style 模型预测 successor state 的 latent representation，并只在 kernel-validated、nonterminal successors 上做排序。JEPA 在 same-theorem Top-1 排名诊断中明显优于 InfoNCE，但三次种子平均只解出 282.3/987 个定理，低于原 proposer ordering 的 308，而且需要更多 tactic checks。