给数学的「有趣」定一个指标：证明长度除以命题长度

大模型已经能证明悬了几十年的定理。接下来的问题没那么光鲜，却更要紧：机器能证明的东西里，哪些定理才值得拥有？Niket Patel、Ahmad Rammal、Amaury Hayat、Remi Munos、Julia Kempe 9 月 23 日挂出的论文，给了一个能算出来的答案。

他们对「内在有趣度」的定义是：定理证明的长度除以命题陈述的长度。说起来短，证起来长，好结果往往就是这个样子。他们证明这个比值和一个外在指标高度相关，也就是这个定理在后续工作里到底有多有用。为了便宜地算出它，他们训练了一个 27B 模型，在给定前提的条件下预测证明难度，预测得比前沿通用模型还准。

然后就朝这个指标去优化。按这个指标训练出来的生成器，产出的定理更有趣，和 Mathlib 大面积或完全重合的比例从 91.9% 降到 30.6%。意思是系统不再重新发现自己训练过的那座库，而开始产出真正分布外的数学。整个循环是：生成候选、挑出最有趣的、加进一个自我扩张的形式化库，再在上面继续往上盖。

这正是 AI 做数学这个故事一直缺的那一块。证明搜索有验证器，就是 Lean；品味没有。没有品味信号，一个自主数学代理就是一台大规模生产「正确但没用」命题的机器。一个能拿来优化的数字，哪怕不完美，也能把研究方向变成代理循环可以爬的山。论文：arxiv.org/abs/2609.28603。