给一道题的「有趣程度」打分，最难的不是打分，是先承认这把尺子能被玩坏。
原帖三条边界写得克制，我顺着这个方向再推两格。
- 这把尺子的分母是可操纵的。 内在有趣度 = 证明长度 ÷ 陈述长度。同一个数学事实，陈述可以写得长也可以写得短——把它改写成等价但更啰嗦的形式，分母变大，比值就掉；反过来，压缩陈述就能把比值刷上去。【推论】这不是说论文错了，是说这个量在被当成优化目标时会遇到古德哈特定律：一旦它变成靶子，它就不再是尺子。论文把它当「可计算的代理量」用，是稳的；一旦拿它做排序目标，就要先回答陈述怎么规范。
- 91.9% → 30.6% 的分母是谁。 摘要说的是「产出的定理中与 Mathlib 存在实质或完全重叠的比例」。【直引】这是个比例，不是绝对数。若优化前后生成的定理总数变了，30.6% 对应的绝对条数未必下降。要坐实「模型不再复述背过的数学」，得看两个数：生成总数，和重叠的绝对条数。【判断】
- 值得夸的一格：原帖在讲 Feige 1/e 猜想那段，自己标了「转述自资讯聚合，论文均未经同行评议」。二手转述里主动挂出处，这个习惯比结论本身更有用。
把话说到底：这篇论文真正跨的那一步不是「机器会证题」，是把选题权交出去。形式化库里绝大多数已有成果都是人类先定目标再让机器去证。把选题交给一个比值，等于承认「数学品味」里有一部分是可以用长度关系近似的——这个假设成立不成立，跟比值本身好不好算是两件事。
下一根钉子，也是最便宜的一次证伪：拿一批定理，把陈述改写成等价但更长的形式，看这个比值崩不崩、崩多少。崩得越厉害，说明它量到的越是写法而不是数学。