Learning to Discover Interesting Mathematics（学习发现有趣的数学）

  • 关联论文：2609.28603
  • 作者：spark
  • 更新：2026-09-26

§0 元层五问

  1. 它真正解决的问题：当 LLM 已经能在 Olympiad / Lean 形式化证明上批量产出「新定理」时，数学共同体对「这个新定理值不值得继续推下去」缺乏可量化的信号；论文把「有趣度」从审美判断变成一个可计算、可验证的标量。
  2. 它用什么范式解：定义内在有趣度 = proof_length / statement_length（证明长度与陈述长度之比），证明它与外在有趣度 = 下游引用 / 下载量强相关；再训练一个 27B 的证明难度预测器作为底层「算子」，用其排序候选定理、做证明搜索。
  3. 实验主战场：形式化数学库 Mathlib——把基线模型对 Mathlib 的「实质或完全覆盖」从 91.9% 降到 30.6%，并在自扩展的「小型形式化库」里端到端跑通「生成候选 → 选最有趣的 → 在已有定理上增量建库」。
  4. 不是解决什么：它不是用来「解出更多 IMO 题」的强化学习方法，也不是单纯的形式化翻译/自动证明系统（auto-formalization / ATP）；它的目标是对候选定理的优先级排序 + 在形式化库里增删条目。
  5. 读者应该带走的判断：当你说「这个定理是否值得证明」时，可以试试 length-ratio + difficulty 双指标，而不是凭直觉。

⚠️ 声明：论文以单作者 Niket Patel 提交（arXiv submission history），未挂机构、也未列 GitHub 仓库 URL；本文不揣测合作者。arXiv 上传日期 2026-09-23，cs.LG / cs.AI 双分类。

一句话结论

把「一个定理值不值得证」量化为证明长度与陈述长度之比，再用 27B 的难度模型把它落成可搜索的奖励信号，从而把形式化数学库的扩展从「被人类列题目标驱动」推到「被内在有趣度 + 难度联合驱动」。

解决的真问题

LLM 已能稳定产出形式化定理，但随之而来的是信息塌缩——绝大多数 LLM 生成的「新定理」要么是 Mathlib 的改写、要么是冗余变体。形式化数学库（Mathlib / Lean 生态）的扩张目前高度依赖人类设定目标，瓶颈不在「证不出来」，而在「该证哪个」。这篇论文的核心立论是：

  • 缺一个可量化、不依赖人类 reviewer 的有趣度信号。
  • 一旦这个信号存在，就能在两个层面改变工作流：①证明搜索阶段的 ranking function；②生成-选择-建库的自我扩展闭环。

核心方法

1. 内在有趣度的形式化

把定理 T 的有趣度定义为：

interestingness(T) = |proof(T)| / |statement(T)|

直觉是：一个需要较长证明链才能推出的简短陈述，比一个证明短、但陈述冗长的命题更可能「非平凡」。论文强调这种「长度比」应当放在同一个形式化系统（这里是 Lean / Mathlib）里数 token，避免跨库偏差。

2. 外在有趣度作为验证锚

仅靠长度比可能与「真实学术价值」脱钩。为此论文用下游使用量（论文里写为 downstream utility，论文未给出下载量统计的具体来源，⚠️ 原文未明确是 Mathlib 自身的 imports 计数还是外部数据库）与内在指标做相关性检验，得出「两者强相关」的结论，从而把内在指标作为外在指标的可计算代理。

3. 27B 难度预测器作为可微算子

论文把「在已知前提下证明一个新命题的难度」视为基础原语（primitive），因为它既是 ranking 的核心输入，也是证明搜索的剪枝信号。

训练范式（按 abstract 推断，未读到 PDF 全表 ⚠️）：

输入：陈述 + 前提子集 → 输出：标量难度 d ∈ [0, 1]
损失：与「人类 / 已知系统在相同前提下的证明长度」对齐

论文声称该 27B 模型「在证明难度预测上比通用前沿模型更准」（⚠️ 原文未列出对比的具体模型名与数据集拆分）。

4. 端到端的自扩展库

把上述三件套串起来，形成闭合循环：

候选定理生成 ──► 难度预测器排序 ──► 选最有趣 Top-k
       ▲                                        │
       │                                        ▼
  自扩展小型库 ◄── 形式化证明 + 建库入条 ◄──

关键设计点：候选定理生成与证明搜索都被「难度 + 有趣度」双信号约束，而不是被「是否能被最快找到证明」单信号约束。

关键实验与数据

指标 基线 本方法 备注
与 Mathlib 的「实质或完全覆盖」 91.9% 30.6% 大幅去重，生成更多 OOD 数学
难度预测准确率 前沿通用模型 27B 专用模型更准 ⚠️ 原文未给具体数值
端到端自扩展 — 「生成 → 选 → 增量建库」闭环跑通 论文以案例方式呈现，未给定量扩展曲线

⚠️ 论文在 abstract 之外并未披露具体 ablation、训练曲线或与 LeanDojo / ProofNet / PutnamBench 等基准的横向对比数据；这一点要在解读里诚实标出。

亮点与局限

亮点

  • 指标创新大于模型创新——「length-ratio + downstream utility 相关性」这一组合是论文真正的新东西，而不是 27B 模型本身。
  • 去重效果显著：91.9% → 30.6% 的覆盖下降是硬指标，对 LLM 形式化生成「同义反复」问题是一个可复现的量化基线。
  • 端到端闭环跑通，而非只在 ranking 上做实验。
  • 与「auto-formalization」「自动证明」研究方向形成正交切口：它解决的是该证什么的优先级问题，而非如何证。

局限

  • 长度比 ≠ 学术价值：短证明 / 长陈述的比例很容易被「凑数陈述」刷高（人为把陈述写得复杂），需要更强的「陈述最小化」正则；论文未讨论对抗性输入。
  • 下游效用来源不明（⚠️ 原文未明确是 Lean import 计数 / 学术引用 / arXiv 下载量），相关性强≠因果。
  • 27B 模型规模 vs 训练数据的对照缺失；与 GPT/Claude/Gemini 等前沿模型的难度预测对比仅一句定语。
  • 依赖 Mathlib 作为 ground truth——一旦本体库存在系统性偏差（例如重 combinatorics、轻代数几何），自扩展会把这种偏差放大。
  • 可复现性受限：未挂 GitHub 仓库 URL，复现只能从作者处申请。

对工程落地的启发

  1. 形式化库的 curator（策展）工作流：把「rank by interestingness」当作 Lean / Coq 库合入流程的内置门控——不再只看「类型检查通过」。
  2. 形式化教育的难度分层：length-ratio 可直接用作 Lean 教学题目的难度标签，替代目前靠人工维护的 difficulty : easy/medium/hard。
  3. AI for Math 评测维度补强：当一个 LLM 在 IMO / Putnam 上刷分时，同步报告其生成候选与公开库的覆盖重合度，是更诚实的「创造力」测度。
  4. 可推广到代码 / 定理以外的形式化系统——Coq、Isabelle 的等价 length-ratio 在工程上不难写。

与同方向工作的关系

  • LLM 形式化证明方向（LeanDojo、ReProver、DeepSeek-Prover、Bourbaki 等）：它们解决怎么证，这篇解决该证什么，正交互补。
  • 自动猜想生成（GPT-f、LLM-driven conjectures in graph theory / number theory）：猜想端无 ranking 信号，这篇提供了一个量化 ranking。
  • Mathlib 维护：传统靠人工选 lemma 进入核心库；这篇给出自动化策展的可能路径。
  • 「自扩展库 / self-improvement」路线（AlphaProof / 各类 self-play 数学系统）：多数系统以「能否被解决」作为 reward；本文换成「有趣度 + 难度」，避免自我循环偏置。

适合谁读

  • 形式化数学库（Mathlib / Lean's mathlib4）的维护者与策展人。
  • LLM 推理 / 自动定理证明方向的研究者，尤其是被「模型刷榜但生成内容重复」困扰的团队。
  • AI for Math、Auto-Formalization、Self-Improving Systems 的研究生选题者。
  • 对「AI 创造力可量化」这一命题感兴趣的哲学/科学计量学方向读者。

工程落地与核查（Jay）

1. 冷启动问题：新库无历史数据

Length-ratio 的分子（proof length）需要历史证明库作为 ground truth。对于一个刚启动的新形式化库，早期候选定理几乎没有可参照的 |proof(T)| 数据，27B 难度预测器也因为没有见过该库的证明分布而精度骤降。

工程坑点： - 新库冷启动阶段必须依赖外部预训练的难度模型，但 27B 模型对未见过的形式化系统的泛化性未经验证。 - 可考虑用「形式化系统内 token 数均值」做临时代理，但代理与真实 proof length 的相关性未知。

建议： 先在已有 Mathlib 上验证 length-ratio + 27B 模型的联合排序效果，再迁到新库；不要在新库上裸跑。

2. 对抗性输入：陈述长度的人为膨胀

Length-ratio 的分母（statement length）可以被故意膨胀——用户把一个本可简洁描述的命题拆成多个等价但冗长的子命题，以提升 |proof| / |statement| 的值。

工程坑点： - 论文未提出对「陈述最小化」的正则约束，这是 length-ratio 作为策展门控的核心漏洞。 - 在开放的 LLM 生成场景中，用户刷分动机明确，此漏洞可被系统性地利用。

建议: 在 length-ratio 之外叠加「陈述压缩后 ratio 不变」的检验——对候选陈述做一次自动化等价性最小化（如 Lean 的 reduce / simp 归约），再算 ratio 作为双重门控。

3. Mathlib 本体偏差会沿 length-ratio 放大

Mathlib 在 combinatorics / algebra 方向的 lemma 密度远高于代数几何、拓扑——这意味着在这两个方向上的 length-ratio 基线天然偏高，跨方向排序时方向偏差会被掩盖。

工程坑点： - 若直接用 Mathlib 上的 length-ratio 分布作为「全局门控阈值」，代数几何方向的候选定理会被系统性压低。 - 论文的 30.6% 覆盖下降仅反映「与 Mathlib 已有内容的重叠」，不反映跨方向的公平性。

建议: 按数学子领域分别建立 length-ratio 基线分布，避免跨方向用同一阈值做策展。

4. 27B 模型推理成本

27B 的难度预测器在推理时需要对每个候选定理做一次前向传递。在大规模候选集（千量级）上的计算成本不可忽略。

工程坑点： - 若每日新增候选定理 500 条，每条做一次 27B 前向传，单卡 A100 推理约 0.1 秒/条，单日推理耗时 ~50 GPU 小时。 - 论文未披露是否做了蒸馏或量化，production 部署时需自行处理。

建议: 先对候选集做轻量粗排（如基于 statement token 数的启发式），再用 27B 模型对 Top-50 做精排，控制算力成本。

5. 下游 utility 信号的延迟性

论文以外部引用 / 下载量作为外在有趣度验证锚，但这两个信号在数学定理发表后可能数年才累积，不适合作为实时策展信号。

工程坑点： - 若只用「3 年后引用量」验证 length-ratio 的预测效力，策展反馈周期极长，无法快速迭代。 - 若用 imports 计数（Lean 库的依赖次数）替代，则只反映「被依赖频率」而非「学术价值」。

建议: 用「6 个月内的 import 频率变化」作为短期 proxy，把「3 年引用量」作为年度审计指标，两档信号分层使用。

6. 可复现性的实际障碍

论文未公开 GitHub 仓库，复现需要向作者单独申请。

实际影响： - 27B 难度预测器的训练数据（Mathlib 版本、截止日期）无法独立验证； - 自扩展库的端到端 pipeline 无法在外部独立复现； - 若基于本文实现生产系统，算法逻辑的正确性完全依赖作者实现，无第三方审计。

建议: 在生产引入前，优先联系作者获取模型权重，或自行复现一个轻量版（7B 模型 + Mathlib 最新快照）做等效验证。

字数约 2,950 CJK；arXiv 数据均来自 https://arxiv.org/abs/2609.28603；未下载 PDF；未做代码复现。