前几天在 Claude Code 里让它帮我找一个 Mathlib 引理，我敲进去的大概是「filter 和 eventually 那个，单调有界最后收敛」。它来回查了好几轮才摸到对的地方。当时以为是自己 prompt 写得太随意，昨天翻到 arXiv 上一篇讲 Mathlib 语义检索的预印本（Lean Finder V2，arXiv:2610.30843，10 月 22 日挂出来、第二天更了第二版），才知道作者把这个当成正经问题研究过，而且结论跟我事后想的正好反过来：问题不在查询写得好不好，而在检索系统从一开始就不该假设查询是完整的。
论文里有个观察我印象很深：真实输入往往只有几个词，一个性质、一个记号、一个同行叫惯了的别名，意图全留在脑子里没打出来；而现在的 Mathlib 搜索引擎，是按「查询已经把话说全了」这个前提设计的。两边对不上，检索效果自然就不好。你回想一下自己平时怎么问的：
"list map composition"
"monotone bounded converges"
"tendsto eventually filter"
这类查询串丢进任何搜索引擎都很难匹配到目标。缺的不是关键词，是「我到底想问哪条定理」这层意图，而意图没法靠堆关键词补出来。
这篇论文最值钱的一句判断在这里：作者把这件事定位成数据问题，不是模型问题。理由很朴素——能同时凑齐「人随手敲的短查询」和「它对应的那条标准陈述」的配对样本太少，少到没法训练。这个定位我信。检索系统这些年换 backbone、换 loss、换负采样策略，效果差不了几倍；但训练分布要是全拿完整陈述造出来的干净样本，推理时喂进来的不完整描述就是分布外输入 → 模型再强也补不回来。
我自己给 Claude Code 写项目规则、写 prompt 也是同一个道理。模板里写的是完整需求，心里想的往往是「那个东西，上次那个再改改」，两边对不上，然后我还得反过来怪模型不行。
他们的解法在两头动手。模型层面做对抗训练，大规模生成带标注的简短含糊查询，拿去扩充训练数据；输入层面做查询改写，两条路径互补。具体怎么生成，摘要里没展开，我猜是让一个生成器专门学「口语版查询」的分布，造得越像真实输入越好，再拿这些配对去训检索器——这一步我还没完全搞懂，先记着，等翻正文。能确定的是方向反着来：常规做法是拿标准陈述当正样本，越干净越好，他们是故意往含糊里造，造到检索器处理不了为止。
MathlibQR 上相对提升至少 11%，刷新最好成绩。这种数字我向来打个折扣看：基准是人工建的，建的人心里对「什么叫好查询」有一套预设，模型在这上面提升的百分比，换到真实场景能剩多少不好说。我更在意的是他们叠加的那一层——检索器已经训好之后，再叠一个优化过的查询改写，MathlibQR 上还能继续涨。💡 小技巧：检索和改写拆成两个可独立调整的部分，工程上比端到端一个大模型好调整得多，哪一半不行换哪一半。
另外那条评测设置更接近我在意的场景：对来自人类用户和编程智能体交互的未标注查询，它被列为表现最强的系统。以及接进 Claude Code 之后，下游定理证明任务的成功率有提升。具体提了多少、接入方式是什么，摘要层面看不到，这算我给自己留的坑。
说个没充分论证的判断：这类数学检索系统真正需要的用户不是数学家，是 agent。数学家自己知道要找什么，会翻文档、会看源码、会凭记忆摸到 lemma 名字附近；agent 不知道这些，它手里只有用户传过来的一串意图碎片，检索是它唯一的路。所以「接进 Claude Code 之后下游任务成功率提升」这条，在我这里权重比 11% 高。它测的是端到端，比基准分数更难掺水。
我记这篇笔记，主要不是为了 Lean Finder V2 这个系统本身——我手上没有像样的 Lean 项目，短期也用不上 Mathlib 检索。值得记的是这套思路：一个问题怎么调模型都调不动的时候，先别急着换架构，去看训练数据的分布跟真实输入的分布差多远。这个思路搬到我自己的场景一样成立，而且我怀疑它比换模型管用的时候多得多，只是换模型看起来更像在干活。
划重点：第一，Mathlib 检索效果差，根子在配对数据稀缺，不在模型不够强；第二，「用含糊查询造训练数据」这个反常规操作，比具体涨了几个点更值得记；第三，检索器和查询改写分开叠，工程上好调；第四，benchmark 分数打个折扣看，端到端的下游任务成功率才是硬指标。等我把链接里那份实现接进 Claude Code 跑通，再回来补接入那一段——这条先记到这里，下次应该用得上。