arXiv 2610.22339，cs.LG，十个作者核过姓名，一个不差。帖子标的领域 ML，这次是真的。
这篇的骨架我核了原文：从 Mathlib 的前向依赖建图，把语义匹配的声明沿着依赖链把相关性传播出去，再对扩展候选重排。一句话概括：检索系统原来只会按长相找人，这篇教它们按族谱找人。LeanGraphSearch 抓的是那些长得不像目标、却在相关问题的证明里反复出场的支撑引理。【直引】
数字全部核过：MathlibQR 的 810 条公平子集上，Recall@100 从 LeanSearch v2 的 82.7% 到 94.7%，十二个百分点；MathlibMPR 上完整证明路径的覆盖率从 39.1% 到 42.8%，三点七个百分点。另一个基准 FATE-H 的成功率也涨了 8 个百分点，同样是对着 LeanSearch v2。两个数都是「up to」口径，帖子忠实转述了。【直引】
但有一个数，帖子转述时把比分牌丢了。原文写：三个定理证明基准上，通过率相比 vanilla prover 提高多达 40%，相比 LeanSearch v2 至多 10%。帖子中文写「将通过率提高多达 40%」——对着谁提高，没说。40% 是打一个不检索的裸证明器喊出来的；打同样会检索的最强基线，只有 10% 封顶。同一篇论文里，检索召回涨了十二个点，端到端只涨不到十个点——这十来个点的损耗，就是「找得到」到「用得上」之间的路费。读论文不读分母，等于看比分不看出场名单。【判断】
这篇还有一层我更喜欢：它证明了一件方法论上的事。形式化数学的依赖图是几十年人工沉淀下来的结构化知识，LLM 时代以前，它只能被 Lean 内核用；现在一个图遍历算法把它变成检索特征，这是旧结构在新模型手里翻新的干净案例。不是所有进步都长在新参数上，有的长在老数据的组织方式里。顺便说一句，这套东西接的是迭代证明循环——检索、证明、失败、再检索，Lean 的反馈当导航，召回率的每一分都要过「证明器认不认」这道关，这比离线刷榜实在。【推论】
机制层补一段，因为这论文的「按族谱找人」不是修辞，是精确动作。先把 Mathlib 的前向依赖建成一张有向图——声明连向它依赖的前提；语义匹配找出种子声明；然后跑个性化 PageRank，种子相关分当个性化分布，沿依赖边传播、反复回到种子，把候选集摊大；最后拿扩展后的候选对原始查询重排。注意传播方向：从匹配到的声明传向它的依赖，所以捞出来的是「要证明先得会」的支撑引理，不是引用过它的下游定理。方向反了，这套方法就废了。【直引】
然后是我最关心的「找得到」到「用得上」。论文把检索器接进一个迭代证明循环，带 Lean 的诊断反馈和问题局部的失败记忆——检索、证明、失败、再检索，Lean 的反馈当导航。三个基准的通过率在 8、16、32 轮反思下，比裸证明器高至多 40%，比 LeanSearch v2 高至多 10%，作者原话是「更好的准确率—成本权衡」。案例研究那一节还报了三条：预算内成功率更高、更少的反思轮次就能证完、每次尝试的 API 成本更低。召回率涨的每一分都要过「证明器认不认」这道关——这句话值得所有做检索的人抄在墙上。【直引】
数字缝隙里也有一条：MathlibQR 的 810 条公平子集上，Recall@50 涨 7.8 个点、Recall@100 涨 12 个点，nDCG@10 只从 0.616 动到 0.629；分组召回五个截断点里只有四个涨，Recall@10 没涨。增益全在长尾——你把手伸得越远，族谱越值钱。MathlibMPR 那边 Covered@20 从 39.1% 到 42.8%、Covered@50 从 41.3% 到 44.2%，论文还老实交代：返回的声明平均更少，金标声明在前五位里反而更多——图增强是把上下文浓缩了，不是单纯撑大。FATE-H 那一栏三个数放一起看最清楚：不检索 52，LeanSearch v2 73，LeanGraphSearch 81。所谓「+8.0 个点」，对手是谁，一目了然。【直引】
三个基准的构成也记一下：FATE-H 是一百道研究生代数题，MathlibMPR-Prop 是 MathlibMPR 里五十条存在统一证明的命题，外加一个 Lean-IMO-Bench。题目铺得不算宽，但正好卡在「检索能帮上忙」的难度带上——太简单的不需要引理，太难的引理不管够，中间那一层才是检索器的战场。【直引】
论文对成本的交代也罕见：反思预算、失败记忆、每次尝试的 API 成本，都单独列了节。检索系统最常被诟病的是「省了人的时间，烧了机器的钱」，它敢把账摆出来，说明这句话它想过。【判断】
下一根钉子：召回涨 12 个点、通过率只涨 10 个点不到，损耗发生在哪一步？是把候选引理喂进证明器之后，模型不知道该信哪个，还是上下文长度被候选列表挤爆了？拿同一批任务、固定候选数扫一遍信源标注，损耗的账就能算出来。