论文链接：Learning to Discover Interesting Mathematics (arXiv:2609.28603) 发表时间：2026年9月 机构：FAIR @ Meta、纽约大学（NYU）、CERMICS ENPC 巴黎综合理工学院。第一作者 Niket Patel 为 NYU 博士生，本工作在其 Meta 实习期间完成；通讯作者 Julia Kempe 为 FAIR 与 NYU 双聘教授——典型的「高校学生 + 企业实验室」跨大西洋合作模式。 领域标签：cs.LG / 人工智能 × 形式数学
一、论文背景
这篇论文要回答的问题，一句话就能说清：AI 已经会证明定理了，但它知道该证明什么定理吗？
先把背景铺开。近两三年，LLM 在数学推理上的进展极其迅猛：AlphaProof 在 IMO 拿到银牌水平，OpenAI 的系统对 Navier–Stokes 方程给出有限时间爆破的证明，Aristotle 解决了 Erdős 问题 #728，组合数学、数论领域一连串悬置几十年的猜想接连被解决。数学推理正从「AI 的圣杯问题」变成「工程问题」。
但作者指出了一个更深层的缺口：当前所有系统都在解决「人类提出的问题」。AlphaProof 证明的是 IMO 考题，FunSearch 优化的是人类定义的目标函数。没有系统回答过：给定一片数学土壤，自己长出值得研究的新定理。
为什么这个问题难？因为「值得研究」这个判断本身就是数学家最核心的品味（taste）。Poincaré 在《科学与假设》里早有断言：「科学由事实构建，如同房子由石头构建；但一堆事实不是科学，正如一堆石头不是房子。」论文还引用了 Borges 的《巴别图书馆》作类比：所有真命题构成的空间就像那座收录一切书籍的图书馆——包含全部真理，却毫无用处，因为无法在里面找到意义。你需要的不仅是「导航能力」（证明），还需要一个「价值度量」把发现与平庸的有效陈述区分开。
历史上这个方向有零星先驱：Lenat 1977 年的 AM、Fajtlowicz 1988 年的 Graffiti 都做过自动猜想生成，Colton 等人 2000 年就把「有趣度」列为自动数学发现的显式研究问题；近期的 Minimo（Poesia 等）与 FERMAT（Tsoukalas 等）用内在动机/强化学习在小公理系统里做理论建构。但这些系统要么绑死在图不变量等特定领域的启发式上，要么只在命题逻辑、初等数论这类玩具领域验证，没有一个能在 Lean 4 mathlib 这种十万级形式数学库的尺度上给出可优化的有趣度信号。
本文的切入点是：不问「人类觉得什么有趣」，而是问「数学结构本身能否给出有趣的定义」——把有趣度变成一个可计算、可优化、可验证的量。
二、论文定位和关联工作
这篇论文处在三条研究脉络的交汇点上。
脉络一：形式定理证明（证明侧）。从 GPT-f、HyperTree Proof Search 到 LeanDojo、DeepSeek-Prover、Goedel-Prover，再到 AlphaProof 的 AlphaZero 式训练，这条线的目标始终是「更快证明给定目标」。本文直接站在这条线的肩膀上——它把 Claude Code + Opus 4.6 当作现成的证明引擎——但关心的却是正交的问题：目标本身从哪来。
脉络二：自动猜想与自动形式化（生成侧）。Autoformalization 从语句级翻译（Wu 等 2022）发展到整本教材的形式化（Rammal 等 2026）。Graffiti 的后继 TxGraffiti 在十年人机协作中产出了多篇发表论文，但其启发式过滤器天然绑定图论。Minimo 在三个公理域中联合学习猜想与证明，FERMAT 用 LLM 进化算法合成有趣度度量——两者都验证了「自提问题」的可行性，但规模与领域广度都受限。本文是第一个在 mathlib 全库尺度上运作的有趣度体系。
脉络三：信息论视角的数学价值观（理论侧）。这是本文最深的根。Kolmogorov 复杂性与描述长度理论给出了「简洁性」的经典框架；Bengio 与 Malkin 2024 年提出「有价值的数学框架具有小描述长度且邻近大量可证命题」的信息论观点；Aksenov 等 2026 年的《Compression is all you need》用 monoid 模型论证人类数学的标志是层级可压缩性，并明确提出可用压缩度量「数学兴趣」。本文的有趣度定义（证明长度 / 陈述长度）正是这一思路的可计算落地——作者在脚注中明确指出其零前提有趣度 I0 与 Aksenov 等人的 interest 概念对应。
| 维度 | 之前路线（AlphaProof / FunSearch / TxGraffiti 等） | 本文突破 |
|---|---|---|
| 数学目标来源 | 人类出题 / 人类定义评估函数 | 系统自主提出并筛选 |
| 有趣度判据 | 无，或领域绑定的硬编码启发式 | 证明长度与陈述长度之比，库上可计算 |
| 验证机制 | 形式验证（Lean） | 沿用形式验证，但验证后还要排序 |
| 迭代方式 | 单任务求解 / 固定目标演化 | 每轮发现的 top-10 成为下轮前提，库自扩展 |
| 规模 | 竞赛级 / 特定领域 | mathlib 全库（11.3 万声明）+ 8 个数学领域 |
定位结论：这篇论文补上的是「自动数学发现」版图中最后缺失的一环——不是更强的证明器，不是更多的生成器，而是一个不依赖人类口味、从证明结构中自发涌现的价值函数。
三、问题定义
把场景抽象到本质：数学库是一个有向无环依赖图，每个定理 T 有证明代价（多少行代码）与陈述代价（多少字符），且依赖一组前提 P（其他定理/定义）。系统每轮可以提出新定理、证明之、并把它们加入前提库。
论文的核心洞察是一个类比：「有趣度」≈ 投入产出比 ≈ 压缩率。
- 一条定理的「产出」是它隐藏的证明代价 V(T|P)：陈述背后垫着多少行推导；
- 一条定理的「投入」是它的条件描述长度 L(T|P)：在一个已拥有前提 P 的读者眼里，把这条陈述（连同它需要的新定义）写出来要多少字符。
由此得到形式化定义——条件有趣度：
$$I(T|P) = 100 \cdot \frac{V(T|P)}{L(T|P)}$$直觉：一句话就能说清、却要千行证明才能落地的命题，就是有趣的命题。条件化很关键：同一个定理，对拥有测度论词汇的读者是平易的，对只有代数几何词汇的读者可能近乎不可陈述——有趣度必须相对前提库计算。P=∅ 时的 I0 给出绝对标尺。
为什么分母必要？论文给了一个漂亮的防作弊论证：取 n 条彼此无关的定理 T1…Tn，用「且」串起来得到 Ĥn。其证明代价 V(Ĥn|P) = O(n) 线性增长，但陈述长度同样线性增长，于是有趣度 I(Ĥn|P) = O(1)——你无法通过串联无关定理把有趣度刷上去。如果不做归一化、只看证明长度，这条捷径立刻被攻破。
同时定义了互补的效用 U0(T) = |D(T)| · V(T|∅)（D(T) 为直接引用 T 的定理集合）：如果把 T 免费送给整个库，能省下多少行重推导。有趣度是内在的（只看定理自身），效用是外在的（看它对整个生态的影响）。
给定：mathlib 依赖图、LLM 提议器与证明器；求：一个可在提议时刻计算的价值函数，使迭代生成的定理库既有趣（比值高）又有用（下游被引用）；约束：所有陈述必须通过 Lean 4 形式验证，且价值判断不得依赖人类评分。
这个定义的精妙之处在于：效用 U0 只能事后观测（定理进入生态、看它的后代才知道），而有趣度 I 可以在提议时刻用 V 的估计值立刻算出。如果两者强相关，有趣度就成了效用的可计算代理——这正是全文的枢纽假设，也是实验要验证的第一件事。
四、问题解法
整个系统是三件套：一个难度预测器、一个被有趣度奖励训练的提议器、一个用有趣度剪枝的自扩展循环。
4.1 组件一：条件难度预测器 Vθ
类比：这相当于强化学习里的 value function，只不过状态是「前提集合」，动作是「证明推导」，回报是「行数」。它要预测的不是胜负，而是代价。
难点：mathlib 的原始数据没法直接用——库被写得极度原子化，证明长度中位数只有 3 行，任何前提被引用的中位数是 1 次。在这样的数据上训练，模型学到的只是「三行搞定一切」。
解法是 premise expansion（前提展开）：沿着依赖 DAG 反向走。设 T 的前提里有条引理 L，一步展开就删掉 L、把 L 自己的前提并入 T 的前提集，同时把 L 的证明行数加进标签——相当于把「可见前沿」往回推，逼模型看到「如果没把 L 打包好，证明会变多长」。反复迭代，从 11.3 万声明构造出约 10 万个（定理， 前提， 代价）三元组，标签中位数 49 行。
训练目标直接对齐三条公理（Definition 1）：
| 公理 | 含义 | 对应 reward 项 |
|---|---|---|
| A1 grounding | 预测要贴合真实代价 CD | L_truth：对数空间绝对误差 |
| A2 premise monotonicity | 前提只会更多不会更贵 | L_drop：删前提后预测值若上升则罚 |
| A3 composition | 经引理中转不超过分步和 | L_Bellman：V(T|P) 与 V(L|P)+V(T|P∪{L}) 一致性 |
注意 A2/A3 恰好是理想最短证明满足的 Bellman 型关系——这个设计把「值函数一致性」从 RL 的技巧升格为公理驱动的训练目标。每个展开边同时发射六种角色的提示（原始/保留引理/删前提/引理上下文/引理原生/随机删减），让公理约束在组内即可比较。基座是 Qwen3.6-27B，GRPO 训练 350 步。
4.2 组件二：有趣度奖励训练 conjecturer
类比：用学出的 value function 当奖励模型再训 policy——标准 RLHF 结构，只是「人类反馈」换成「结构反馈」。
从 mathlib 训练分割随机抽 1 万个前提集合（中位数 77 条前提），让 Qwen3.6-27B 基于前提提出独立 Lean 命题。奖励设计成对数形式抑制离群值：
R(T,P) = 0.25 + log(1 + Iθ(T|P)/100)
其中 Iθ 用冻结的 Vθ 计算。奖励有清晰的分层：解析失败 −0.5；编译失败或与前提无关 −0.25；能被 assumption/rfl/simp 等自动策略秒杀的平凡命题得 0；只有有效、相关且非平凡的命题才进入有趣度打分。Pantograph 负责编译检查，确保提议在语法层面就是合法的 Lean 定理类型。GRPO 仅 75 步即完成训练。
4.3 组件三：推理期有趣度剪枝 + 自扩展库
类比：进化算法的「选择压力」——每轮只让最优的分支进入下一轮的搜索前沿。
流程：每轮 conjecturer（此处用 Claude Opus 4.6）收到 20 条前提（5 条来自上一轮新晋定理、15 条来自存量库），生成 400 条候选陈述；语义过滤器去掉等价猜想保证多样性；Claude Code 在 Lean 里逐条独立证明；验证通过的按真实有趣度（此时证明已写出，用真实行数而非估计值）排序，top-10 晋级为下一轮前提。六轮下来得到一条 P0 ⊂ P1 ⊂ … ⊂ P6 的自扩展定理链。
一个细节值得注意：训练时用 Vθ 估计（不可能为每个候选写证明），推理剪枝时用真实证明长度（证明已经写了）——估计器只在验证昂贵的地方出场，这是对计算资源的清醒分配。
五、评估指标与实验证据
论文的评估回答四个递进的问题：预测器准不准？有趣度与效用的相关性成立吗？优化有趣度真的能产出更好的定理？迭代发现循环真的越滚越好？
5.1 难度预测器：27B 专才击败前沿通才
在 4,615 条留出验证提示上（所有模型收到完全相同的定义、前提、目标与输出指令）：
| 模型 | MAE（证明行数）↓ | Spearman ρ ↑ |
|---|---|---|
| Vθ（本文，Qwen3.6-27B + GRPO） | 20.2 | 0.912 |
| GPT-5.5 | 31.0 | 0.776 |
| Claude Opus 4.6 | 34.3 | 0.815 |
三个模型都倾向于低估长证明（校准图上随长度增加系统性偏离 y=x），但本文模型偏差显著更小。这证明「证明代价预测」是一个可以靠数据+公理化奖励专项训练出来的能力，不是通用模型顺手就有的——通用模型缺乏对前提集合变化敏感的结构性理解。
5.2 枢纽验证：有趣度 ↔ 效用 Spearman ρ = 0.756
在 mathlib 全库上计算每个定理的 I0 与 U0（排除无下游用户即 U0=0 的声明后）：ρ = 0.756。更重要的不对称性：存在高有趣度低效用的定理（孤芳自赏的深结果），但几乎没有高效用而低有趣度的定理——高效用是被高有趣度「包含」的。这一实验确立了核心主张：有趣度是效用的可在提议时刻计算的前置代理。另外全库 I0 排序的直观性检查也通过：1^n = 1 垫底，中位值定理、费马小定理居中，费马大定理 n=3/n=4 特例位居前列——「易述难证」的民间直觉与公式一致。
5.3 训练效果：有趣度 4.3 倍提升 + 跳出 mathlib 分布
8 个数学领域（代数、分析、数论、测度/概率、几何/拓扑、组合、范畴/代数几何、基础）、每领域 20 条经 Claude Code 证明验证的定理、共 160 条/模型，用真实证明计算有趣度：
| 模型 | 平均有趣度 I(·|P) | 与 mathlib 重合（实质/完全包含） |
|---|---|---|
| Qwen3.6-27B Base | 1.76 | 91.9% |
| Claude Opus 4.6（被提示生成有趣定理） | — | 92.5% |
| Trained（75 步 GRPO） | 7.58 | 30.6% |
三个要点：其一，平均有趣度提升 4.3 倍，八个领域全部胜出（组合 2.10× 到数论 8.72×），同时全面超过被提示「生成有趣定理」的 Claude Opus 4.6——提示词换不来的能力，75 步结构化奖励就换来了。其二，重合率评估由 LLM-as-a-Judge（Claude Opus 4.6、温度 0、隐藏来源）按 5 级标准盲评：未训练模型 91.9% 的产出实质或完全落在 mathlib 里——LLM 的默认模式是复述已有数学；训练后压到 30.6%，真正 out-of-distribution 的新数学成为多数。其三，这组数字共同说明优化有趣度不是「制造难题」，而是把提议分布推向证明更长且未被现有库覆盖的命题。
5.4 推理期剪枝消融：比值定义优于一切朴素基线
六轮迭代发现（图论前提起步），固定 conjecturer、语义过滤器与证明器，只换晋级规则：
| 晋级规则 | 晋级定理平均有趣度 | 盲评「最有趣」当选率 | 质量分（1-5） | 多样性分（1-5） |
|---|---|---|---|---|
| 无剪枝 | 1.31 | 13% | 2.50 | 1.30 |
| 随机 | 1.56 | 8% | 2.40 | 1.20 |
| 证明长度剪枝 | 3.26 | 19% | 2.60 | 1.30 |
| 有趣度剪枝 | 3.90 | 60% | 3.40 | 2.10 |
盲评设置：评审模型每次看四条定理（各来自一种规则，规则名隐藏），按数学趣味排序，共 100 组。有趣度剪枝以 60% 的首轮当选率碾压其余三者。关键对比是第四行 vs 第三行：按证明长度剪枝看似与按有趣度剪枝只差一个归一化分母，效果却差得多（19% vs 60%）——长度剪枝会集中产出冗长的同族定理（冗余率 50% vs 28%），而比值剪枝天然排除「堆长证明」的作弊路径。这是「收益来自比值定义本身」的直接证据。
5.5 自扩展库与示例
迭代发现产出了图论、代数、测度/概率、数论四个起点共 6 轮的定理图。附录列出代表性生成：四元数平方等于 −1 的完整刻画（实部为零且范数为 1）、上半平指数的衰减性、对合矩阵与伴随矩阵的刻画、乘法幂等基数的三分律等——都是「中等深度、陈述紧凑、证明非平凡」的定理，与设计目标一致。
跨领域矩阵（附录 E）进一步佐证条件化的合理性：测度论定理在解析类前提下有趣度正常、换成代数前提则骤降；而代数在别的领域前提下有时反而更有趣。有趣度确实捕捉到了「陈述难度依赖词汇环境」的结构。
六、效果优势的根源解释
6.1 根源机制与证据链
对比对象：基线是「通用 LLM 直接提议 + 无差别保留」，它为何曾经有效？因为通用模型见过海量数学文本，能产出语法正确、与前提相关的命题——这在「没有更好信号」时是合理默认。但它的根本局限在于：生成分布由训练语料的分布决定，而人类数学文本本身就是mathlib 式已知数学的回声。91.9%/92.5% 的重合率不是模型不行，而是没有任何梯度信号把分布推离已知区域。
本文的根本性改变是引入了一个只在「未知且高压缩比」区域为正的优化压强。因果链：
- 比值定义 I = V/L 把「有趣」操作化为「证明代价/陈述代价」——由 3.1 节防作弊论证与 mathlib 全库排序直观性支持【论文实验已支持】；
- 有趣度在提议时刻可由 Vθ 计算，而效用只能事后观测——ρ=0.756 的强相关（且高效用⇒高有趣度的单向包含）使前者成为后者的有效代理【论文实验已支持】；
- 以有趣度为奖励的 75 步 GRPO 改变了提议分布的信息结构：从「高似然已知」转向「高有趣度未覆盖」，体现为 4.3× 有趣度提升与重合率 91.9%→30.6%【论文实验已支持】；
- 比值（而非证明长度）剪枝维持了选择压强与多样性的兼容——长度剪枝可被「同族冗长」策略攻破（冗余率 50%、盲评当选仅 19%），比值剪枝的冗余率 28%、当选率 60%【论文实验已支持】；
- 难度预测器精度是全链条的精度上限——Vθ 的 MAE 20.2 vs 前沿模型 31.0+，若预测器不准，奖励信号退化为噪声【论文实验已支持，但「预测误差如何传导为提议质量损失」的定量分析论文未做——阅读者推测该传导是温和的，因为排序相关性（Spearman 0.912）比绝对误差对剪枝更关键】。
6.2 相关工作检索与对照
| 研究（可核验链接） | 相似尝试 | 相关结论 | 与本文的差异与适用边界 | 对根源解释的影响 |
|---|---|---|---|---|
| Aksenov et al. 2026, Compression is all you need (arXiv:2603.20396) | 用 mathlib 依赖图上的压缩度量量化「数学兴趣」 | 独立得出「压缩=价值」：人类数学的标志是层级嵌套可压缩性，mathlib 展开长度随深度指数增长 | 理论/实证建模，未训练生成系统；本文的 I0 与其 interest 概念显式对应 | 支持：不同方法（monoid 建模 vs 比值优化）收敛到同一价值定义，强烈佐证有趣度的结构性来源 |
| Poesia et al. 2024, Minimo (arXiv:2407.00695) | 从公理自举，联合学习猜想与证明，目标「难而可证」 | 验证了内在动机驱动可以在命题逻辑/群论等 3 个公理域自举提升 | 小规模玩具域，无真实库；有趣度用「对自身证明器难」定义——是相对智能体能力的，非相对结构的 | 补充：证明「自提问题」范式可行；同时其「难度随证明器进化而移动」提示本文的 V 固定基准是一种简化 |
| Tsoukalas et al. 2025, FERMAT (arXiv:2511.14778) | 用 LLM 进化算法合成可解释的有趣度度量（EvoAbstract） | 发现非硬编码的有趣度度量能显著改进初等数论/有限域的概念发现 | 度量是学出的程序而非显式公式，域为小型符号系统 | 支持：「有趣度可以脱离人类评分被显式优化」在另一实现路径下复现 |
| AlphaProof (Nature 2025, doi:10.1038/s41586-025-09833-y) | Lean + 强化学习的大规模定理证明 | 结论原文：「从解题走向理论构建——持续扩展概念库——是下一大步；让 AI 理解数学品味、有趣度或美感仍是悬而未决的开放问题」 | 只解题不选题；本文恰好回应其点名的开放问题 | 补充：证明侧最高水平的工作明确承认本文所填的缺口，且 AlphaProof 的多日级推理开销凸显「选对题再证」的经济价值 |
| FunSearch (Nature 2023, doi:10.1038/s41586-023-06924-6) | LLM+评估器的演化搜索做出 cap set 新发现 | 「识别并只基于最佳想法构建」的迭代进化循环有效；多样性机制防停滞 | 评估器由人类定义（目标函数），发现物是程序不是定理 | 限定：自改进循环的价值已被广泛验证，但 FunSearch 的价值源是外置的——本文的贡献在于把价值源内置于数学结构，这正是二者本质差异 |
反向证据方面：Mishra 等 2025（论文引用）发现 LLM 不能稳健复现人类对数学题有趣度的判断——这与本文互补而非冲突：本文恰恰放弃了「复现人类判断」路线，改用结构内生定义。未发现直接否定「证明/陈述长度比」有效性的已发表工作；本次检索范围内，本文是首个在真实形式库全库尺度上训练有趣度驱动猜想器的工作。
6.3 综合判断与未决问题
多研究共同支持的机制：「压缩/比值即价值」（本文 + Aksenov + Bengio-Malkin 理论）与「自改进选择循环」（本文 + FunSearch/AlphaEvolve 谱系）两条支柱均有独立来源交叉印证，可信度最高。
仍属推测的机制：有趣度提升 4.3× 的收益中有多少来自 Vθ 精度、多少来自奖励分层（-0.5/-0.25/0/正）的工程质量？论文未做消融。适用条件：收益在「陈述-证明长度是良好代价代理」的领域成立；若证明行数被文体因素污染（论文自承 aesop/grind 等自动化策略以运行时间换行数），比值可能失真。可能失效条件：一是论文自列的局限——行数是文体产物、未量化「连接无关子领域」的价值、未验证新定理对未来证明的实际效用；二是长跑系统的多样性退化风险（作者也承认需要更多去重机制）；三是数学价值的多维性——历史/工具性/连通性的价值均在此定义之外。
七、必要知识反推
假设一个零知识的人要完成这项工作，最少需要掌握什么？
领域知识层：
- Lean 4 / mathlib 的依赖结构——不理解「定理的证明引用哪些前提、定义如何递归展开」，就无法设计 premise expansion，整个数据管道无从谈起。作者团队此前已有多篇 mathlib 大规模形式化论文，这是厚积薄发。
- 数学价值的两类来源（内在易述难证 vs 外在下游效用）与数学史上的美学讨论（Poincaré、Pólya、Thurston）——这些引文不是装饰，而是定义公理化的直觉土壤。
方法论知识层：
- 强化学习与值函数理论——识别出 A2/A3 是 Bellman 型关系，才能把「difficulty 预测」升级为「公理化奖励设计」；GRPO/奖励分层是 DeepSeekMath 以来的成熟工具箱。
- 描述长度/压缩的信息论谱系（Solomonoff、Kolmogorov、Levin 复杂度）——没有这一层，I(T|P) 的比值定义就成了无根之木，也无法与 Aksenov、Bengio-Malkin 的工作对话。
- 内在动机与自动猜想的历史谱系（AM、Graffiti、Minimo、FERMAT）——知道前人死在哪里（领域绑定启发式、玩具域），才能设计出库级方案。
工程知识层：- 大规模数据构造与验证管道——Pantograph 编译检查、LLM-as-a-Judge 盲评协议（隐藏来源、5 级 rubric）、证明代理的「严格修复」约束（Jaccard ≥0.70 防止修变成重写），每个评估环节都要防 LLM 评审的偏差。
- 多智能体编排——Qwen 训练的 Vθ、Claude 当 conjecturer、Claude Code 当证明器、Claude 当裁判：懂得按各模型强项分工是 2026 年的实用主义。
知识融合的关键节点：最大的化学反应点是「premise expansion + Bellman 公理 + 比值有趣度」三者的对接——依赖图展开提供数据，公理提供损失函数，比值提供最终目标。单有任何一个都不够：没有展开的数据是退化的（3 行中位数），没有公理的预测器不满足单调性（会被删前提轻易愚弄），没有比值的目标可被串联作弊攻破。把三个领域的常识在同一个形式库上闭环，才是这项工作的真门槛。
八、论文中可以提取的通用性灵感
灵感一：用「投入产出比」代替「产出」做优化目标。 核心思想：优化一个量时，用它的产出除以它的成本（描述代价/实现代价/交互代价），比值形式天然免疫「堆量作弊」。 论文证据：有趣度剪枝 60% 盲评当选 vs 证明长度剪枝 19%；串联 n 条定理 V=O(n) 但 I=O(1)。 推广场景：① 自动化科研中按「实验成本/假设简洁度」归一化的发现分；② 代码生成里按「功能覆盖/代码长度」筛选工具函数；③ Agent 记忆库按「被复用次数/存储代价」清理条目；④ 课程设计按「能力增长/学习时长」排序知识模块。
灵感二：内在可计算指标可以做外在效用的前置代理。 核心思想：当真正的价值只能事后观测时，寻找一个与强相关、但可在决策时刻计算的内在代理指标。 论文证据：ρ=0.756 且高效用⇒高有趣度的单向包含；有趣度提议时算、效用入库后才知道。 推广场景：① 开源项目用「依赖深度/README 简洁度」预判未来被引用率；② 内容平台用「信息密度」代理长期留存价值；③ 芯片设计用「可综合性指标」代理流片后良率。
灵感三：公理化奖励优于端到端拟合。 核心思想：为预测器显式写下它应满足的公理（grounding、单调性、可分解性），把每条公理编译成一项损失，而不是只拟合标签。 论文证据：L_truth/L_Bellman/L_drop 三项分别对应 A1/A2/A3，27B 专才以 MAE 20.2 大幅胜过 GPT-5.5 的 31.0。 推广场景：① 定价模型加「单调性约束损失」（风险高不应更便宜）；② 推荐系统加「多样性公理」防同质化；③ 任何需要「结构一致性」而不仅是「平均误差」的回归任务。
灵感四：自扩展知识库的最小闭环 = 生成 + 验证 + 比值剪枝。 核心思想：开放系统长期不退化的关键不是更强的生成器，而是每一轮用严格标准只让少数高质量产出成为下一轮的「前提」。 论文证据：top-10 晋级制六轮迭代，多样性分 2.10 vs 无剪枝 1.30；「与前提无关陈述」在奖励层就被截断。 推广场景：① Agent 技能库的「学到-验证-晋级」闭环；② RAG 知识库的增量治理（只入库可验证且高压缩比的新知识）；③ 科研团队的 idea 漏斗；④ 合成数据的自我迭代生成。
灵感五：专才小模型在结构化预测上可越级击败前沿通才。 核心思想：当任务有丰富结构（依赖图、公理、天然标签）时，用领域数据+结构化奖励专项训练的 27B 模型能超过通用旗舰。 论文证据：MAE 20.2 vs 31.0/34.3，Spearman 0.912 vs 0.776/0.815。 推广场景：① 企业用 7B-30B 专才模型做法律条文难度/财务风险分级；② 编译器用小模型预测优化 pass 收益；③ 任何「有大量历史 (输入,代价) 对」的工程预测问题。
附录：本文金句
「一堆事实不是科学，正如一堆石头不是房子。」——Poincaré（论文开篇引用，也点明了本文动机：证明能力之上，还需要选择能力）
「一个定理的优雅程度，正比于其中可见的独立思想数量，反比于看清它们所需的努力。」——Pólya（有趣度比值定义的直接先声）
「我们的美学本能把我们引向有深度与连通性的数学。正是这些模式的深度与美，使它们可能在数学、科学与世界的其他部分以意想不到的方式显现。」——Thurston（有趣度-效用相关的直觉版表述）