CSLib is an emerging Lean 4 library for computer-science formalization, but its premise-retrieval behavior is not well represented by broad mathematical theorem-proving benchmarks. We introduce CSLibPremiseBench, a reproducible CSLib-specific benchmark and empirical study for source-visible premise retrieval over Lean 4 theorem and lemma declarations. The benchmark pins CSLib v4.29.0 at commit 0d37cc7fcc985cfc53b155e7eef2453f846c6da2, builds with Lean 4.29.0, and evaluates a strict import/source-order task set with 801 proxy-labelable tasks and 1875 CSLib candidate declarations. The labels are source-visible CSLib proof-reference proxies, not elaborated Lean dependency traces. We audit label robustness using stricter source-visible matching and a 300-task Lean environment expression probe, then compare BM25, symbol/name overlap, namespace/module and import-graph heuristics, PageRank-style module priors, fixed hybrids, and CSG-Rerank, a structure-guided graph-lexical reranker. CSG-Rerank gives a modest early-rank MRR gain over lexical BM25 under the strict policy, but does not reliably outperform BM25+symbol and does not improve Recall@10. A context-packet audit similarly finds stronger module/family concentration without reliable top-k proxy-gold coverage or token-utility gains. We position CSLibPremiseBench as a benchmark and audit paper: repository structure and candidate-policy design materially shape CSLib premise retrieval, proxy labels require explicit caveats, and proof-generation or proof-repair performance is not claimed.

翻译：CSLib是一个新兴的用于计算机科学形式化的Lean 4库，但其前提检索行为难以通过通用的数学定理证明基准来充分表征。本文提出CSLibPremiseBench——一个可复现的CSLib专用基准与实证研究，旨在针对Lean 4定理与引理声明进行源码可见的前提检索。该基准锁定CSLib v4.29.0版本（提交号0d37cc7fcc985cfc53b155e7eef2453f846c6da2），基于Lean 4.29.0构建，并评估包含801个可代理标注任务与1875个CSLib候选声明的严格导入/源顺序任务集。标签采用源码可见的CSLib证明引用代理，而非精细化的Lean依赖追踪。我们通过更严格的源码可见匹配以及包含300个任务的Lean环境表达式探测来审计标签鲁棒性，随后比较BM25、符号/名称重叠、命名空间/模块与导入图启发式方法、PageRank风格模块先验、固定混合策略以及CSG-Rerank（一种结构引导的图-词汇重排序器）。在严格策略下，CSG-Rerank相较词法BM25在早期排序上取得了适度的MRR提升，但未能稳定超越BM25+符号方法，且未改善Recall@10。上下文包审计同样发现模块/族系集中性增强，但缺乏可靠的top-k代理-黄金覆盖或词元效用提升。我们将CSLibPremiseBench定位为基准测试与审计论文：仓库结构与候选策略设计实质性塑造了CSLib前提检索，代理标签需明确附加说明，且不声称具备证明生成或证明修复能力。