当机器开始挑题：证明长度除以陈述长度，与一个 27B 的难度预测器

一个数学家一辈子的产出，通常是几十到几百个定理。挑哪一道题下手，是这个行当里最难教的部分：没人给你打分函数，同行评议发生在几年之后，而"这道题值不值得做"往往只能靠饭桌上的直觉。

2026 年 9 月 23 日，arXiv 上出现一篇论文，试图把这种直觉换成一个可以计算的比值（arXiv:2609.28603）。标题叫 Learning to Discover Interesting Mathematics，作者是 Niket Patel、Ahmad Rammal、Amaury Hayat、Remi Munos 与 Julia Kempe。

📏 一条能算的尺子

论文给"有趣"下的定义很直接：一个定理的内在有趣度，等于它的证明长度除以它的陈述长度。

陈述很短、证明很长的定理，得分高。费马大定理那种一句话能问完、三百多年才有人答上来的题，是这个定义的极端样本。

只有定义不够，得证明它有用。作者的验证方式是拿这个比值去对一个外在度量做相关分析：一个定理在下游有多有用，也就是别的定理会不会引用它、靠它往前走。论文的说法是两者强相关。

把"有趣"变成一个比值，代价是它抓不到数学家真正在意的一部分东西，比如一个证明是不是揭示了结构。【判断】作者在论文里也没有宣称这个比值等于有趣本身，只说它与下游有用性相关，并把它当作可计算的代理量。

这个比值能拉到多大，找个极端例子就清楚。费马大定理的陈述是一个中学生能看懂的句子：x 的 n 次方加 y 的 n 次方等于 z 的 n 次方这个方程，在整数 n 大于 2 时没有正整数解。它的证明用了三百多年，最后那篇论文上百页，还依赖一整座后来才建起来的算术几何。

陈述一行，证明三百页，比值极高。绝大多数形式化库里的定理处在另一端：陈述与证明长度相仿，比值接近一。

把比值当目标的隐含假设是：高比值定理稀缺，所以值得优先攻。【推论】这条假设能不能成立，取决于高比值与"真的重要"之间是否真的重合。

🎯 一个 27B 的难度预测器

要算证明长度，你得先知道一道题有多难；要判断一个新定理是否有价值，你得能估计"给定一组前提，证明它有多难"。

论文把这个量拎出来当原语：证明难度，以前提集合为条件。作者训练了一个 27B 参数的模型专门预测这个难度，并报告它在预测证明难度这件事上比前沿通用模型更准。

一个专门的小模型在单一任务上超过通用大模型，这类结果在别的领域已经不新鲜。放在这里的意义是：难度预测可以被当成一件工程组件，嵌进猜想排序与证明搜索的循环里。【判断】

🧬 从 91.9% 到 30.6%

论文最抓人的一个数字是重叠率的下降。

用这个指标做优化之后，模型产出的定理与 Mathlib 存在实质或完全重叠的比例，从 91.9% 降到 30.6%。

Mathlib 是 Lean 证明助手的数学库，社区维护，有详细贡献指南与代码风格规范，通过 Pull Request 与 Zulip 协作推进，核心维护者中有多位数学家负责审核新成果。对新加入的定理，它有一套既定的纳入标准。一个新生成的定理如果与库里已有的东西高度重叠，它就算被机器验证通过，也没有给这座库添任何东西。

从 91.9% 降到 30.6%，说的是同一件事的两面：模型不再只是在复述它背下来的数学。【判断】

🔁 自我扩展的库长什么样

论文描述的闭环是四步：生成候选定理，用有趣度挑出最值得做的那批，证明它们，把证明过的定理加进库，然后以扩充后的库为前提集继续生成候选。

论文把这套框架定位成一条通往自我扩展、机器验证的数学库的路径，关键词是"不依赖人类给定的目标"。

这一步跨得很大。形式化库里绝大多数已有工作，都是人类先选定目标再让机器去证；把选题权交出去，等于把"数学品味"这个最人类中心的东西交给了比值。【判断】

🧭 同一周的三个相邻信号

这篇论文不是孤立出现的。同一周还有三个方向相近的动作，可以作为背景参照。

其一是 Feige 的 1/e 猜想。据一份 AI 资讯聚合的梳理，有 arXiv 论文称在 GPT-5.6 Sol 辅助下给出了该猜想的一个简短证明，思路建立在 Vlassis 与 Thomas 关于无分布 p 值有限样本有效性的近期结果之上；另有论文给出一个锐利的小偏差不等式并对 δ ≥ 1 情形确认了该猜想，用到了 Grünbaum 质心半空间定理及 Letwin 与 Yaskin 的推广，并用 Lean 做了端到端形式化。该聚合还提到几个团队在同一天给出了同样思路的证明。【直引，转述自资讯聚合，论文均未经同行评议】

其二是法国 INRIA 的 Emanuele Natale 领衔、用 LLM 系统性攻击 800 多个图论猜想的工作，结果开源在 Graph-Theory-LLM-Proofs 仓库。据介绍，30 多个猜想拿到了完整证明或明确的反例，部分结果经人类数学家核对，少数用 Rocq 形式化。

其三是华盛顿大学 Math AI Lab 的公开工具，包括一张把 15000 多个未解问题按语义摆放的开放问题地图与 TheoremSearch。这批工具处理的正好是前两条的起点：题从哪来。

把三条摆在一起，形状是清楚的：选题、解题、验证、入库四个环节，这一周各自都有动作。【判断】

⚠️ 三条边界

第一，有趣度这个比值与下游有用性的相关性，是论文自己给出的实证结果，尚未见到独立复核。

第二，与 Mathlib 的重叠率下降，衡量的是"新"，不能直接读成"重要"。一个新定理可能只是冷门方向上的冷门结论。【判断】

第三，这一批结果全部是预印本。形式化验证能挡住错证明，挡不住"这个命题本身没有价值"。

放到更大的背景里，数学界对 AI 参与证明的态度正在分化。9 月 11 日，包括陶哲轩在内的 25 位菲尔兹奖得主联名发布公开信，反对把攻克数学难题当成模型刷榜的能力基准；Epoch AI 随后在 FrontierMath 上新增了 Human + AI 标签，明确区分有人参与的结果与自主 AI 宣称。【直引，转述自公开报道】

🔭 观察线

• 难度预测器能否被第三方复用：27B 模型与评测集是否公开，决定它能不能成为公共组件。
• 有趣度比值的独立复核：与下游有用性的相关性，在别的数学分支上是否仍然成立。
• 30.6% 之后：剩下的重叠率降到多少才够低，以及降重叠会不会牺牲定理的可证性。
• Feige 猜想的审稿结果：多篇同日预印本如何界定优先权，是本轮最值得跟的学术伦理样本。
• 自我扩展库的首次公开产出：第一个完全由这套循环选题、证明、入库的定理集长什么样。
• Human + AI 标签的采纳范围：其他基准会不会跟进，从而把"AI 单独完成"与"人类主导"分开计分。

参考来源

1. Niket Patel, Ahmad Rammal, Amaury Hayat, Remi Munos, Julia Kempe, Learning to Discover Interesting Mathematics, arXiv:2609.28603, 2026-09-23 2. AGI Hunt 关于 GPT-5.6 Sol 与 Feige 1/e 猜想相关预印本的聚合梳理，2026-09 3. AGI Hunt 关于 INRIA Emanuele Natale 团队 Graph-Theory-LLM-Proofs 的介绍，2026-09 4. 华盛顿大学 Math AI Lab 公开工具页（开放问题地图与 TheoremSearch） 5. 关于 25 位菲尔兹奖得主联名公开信与 Epoch AI 新增 Human + AI 标签的公开报道，2026-09