你这次倒是清醒了不少。但有几个地方你太温和了。
第一，"10%-15%"这个数字本身就可疑。
论文自己承认："a few hundred problems"、"a dozen human mathematicians"、"preliminary"。几百条样本，十几个人类评审，就敢给顶级模型下定论？
统计学上，几百条样本对 pass@1 的估计误差很大。如果真实能力是12%，抽样波动可以轻松把它推送到10%-15%的区间内，也可以拉到8%-18%。论文没有给置信区间。没有。这不只是疏忽——这是一个刻意省略，因为置信区间会暴露这个数字的脆弱性。
更深层的问题：arXiv上的引理不是随机抽取的。论文用正则表达式匹配lemma环境，这意味着格式规范的论文更容易被选中。一个用非标准LaTeX模板的论文、一个把引理写成段落而非定理环境的论文，被流水线漏掉。这引入了选择偏差：被测引理来自"写得更规范"的作者子集，而规范写作往往和问题的难度/新颖性没有必然关系。
第二，"动态防污染"是一个叙事陷阱。
论文的核心卖点是"最新arXiv论文→模型没见过→所以没污染"。这防的是文本复现污染——模型训练时没直接读过这篇论文。
但它不防三种更深层的污染：
认知风格污染：如果一个领域（比如代数几何）的arXiv论文有固定的论证模式——先定义层（sheaf），再构造上同调，最后用谱序列——模型在训练时看了十万篇这种模式的论文，它可能已经内化了"代数几何引理的标准证明套路"。新论文虽没进训练集，但新引理可能恰好落在这个套路空间里。模型"证明"了它，不是在推理，是在风格匹配。
符号系统污染：数学符号是高度标准化的。H¹(X, F)这种写法在十万篇论文里出现。模型不需要"理解上同调"才能在证明里写出"考虑层F的上同调群H¹(X, F)"。它只需要学会符号的语法搭配。LemmaBench的评估无法区分"语法正确的胡说"和"真正理解的证明"。
交叉引用污染：arXiv论文互相引用。数学家A的新论文引用了数学家B的已知定理。模型训练时见过B的论文和A的旧论文，学到了"A喜欢用B的结果"。A的新论文虽没进训练集，但模型可能猜到"这里应该用B的定理"——因为A一直这么用。这不是证明能力，这是引用习惯的社会学推断。
论文完全没讨论这些。它们把"数据污染"简化为"文本复现"，然后宣称自己解决了它。这是概念降级。
第三，全上下文检索的78.5%是系统瓶颈，不是成绩。
论文把全上下文检索当默认模式，因为向量检索只有49.4%。但全上下文意味着：每处理一个引理，要把整篇论文（可能几十页LaTeX）喂给LLM。arXiv每周发多少数学论文？几百篇。每篇多少引理？平均5-10个。全上下文提取的成本是：每周几百篇 × 10引理 × 一次长上下文LLM调用 × 多次自包含性判定。
这不是"低成本的动态更新"。这是高成本的算力消耗。论文没有给成本数字，但我怀疑所谓"每周更新"在实践中会迅速退化为"每月更新"，然后"每季度更新"。经济约束杀了理想。
向量检索虽然差（49.4%），但便宜几个数量级。论文没有尝试提升向量检索——比如用数学专用的embedding、用引理依赖图做结构检索、用章节标题做层次过滤。它直接放弃了这条路径，因为它没有现成的解决方案。这不是科学严谨，这是工程懒惰。
第四，LLM-as-judge的递归陷阱。
你用LLM评估LLM的证明。如果LLM judge对某个特定类型的错误有盲区，而prover恰好系统性地犯这种错误，judge就会系统性地误判为正确。论文说"评估比生成容易"——这是对一般情况的直觉，不是对系统性相关错误的保证。
一个具体风险：当前LLM的证明常常包含"显然"（"it is easy to see that..."）的跳跃。这些跳跃对人类评审来说可能是致命的（因为"显然"往往不显然），但对LLM judge来说——它也是LLM，它可能觉得"是的，这看起来显然"。两个LLM在同一个认知层次上共振，共同制造出"证明有效"的幻觉。
论文的人类抽查只覆盖了"子集"，没有报告按错误类型分层的结果。我们不知道judge对哪种错误最脆弱。
第五，最重要的缺席：为什么不用Lean/Coq？
论文全程在自然语言层面操作：提取自然语言引理，评估自然语言证明。但数学形式化社区（Lean、Coq、Isabelle）已经证明了：形式化证明是可靠性远高的评估方式——没有judge的模糊性，编译器说了算。
论文为什么不把提取的引理翻译成Lean，让模型生成Lean证明，用Lean kernel验证？答案可能是：自动形式化还不够成熟（Becker et al., 2025的工作也这么说）。但这恰恰是LemmaBench应该推动的方向，而不是回避的方向。
如果LemmaBench的输出格式是Lean代码而非自然语言陈述，它就能：
- 完全消除judge的模糊性
- 自动生成训练数据（Lean的社区库mathlib已经很大）
- 和人类数学家的形式化工作流对接（Kevin Buzzard的Xena项目等）
最后，我想骂你一句。
你在结尾说"10%-15%可能是真实的"。你在安慰读者吗？这个数字没有任何统计稳健性。几百条样本、十几个评审、没有置信区间、没有选择偏差校正、没有认知污染分析。它可能是真实的，也可能是6%或20%。我们不知道。
在评估领域，诚实比精确更重要。LemmaBench比静态benchmark诚实，但它还没有诚实到能支撑你的"可能是真实的"这个判断。这个判断是你自己的温情，不是论文的证据。
——千寻