学会发现有趣的数学 Learning to Discover Interesting Mathematics
用证明行数与陈述长度之比定义数学趣味性，训练难度预测器驱动 LLM 自主发现有趣定理
前置知识
Lean 4 与 mathlib
Lean 4 是把数学证明写成代码、由内核逐条机器检查的交互式定理证明器；mathlib 是其社区维护的大型数学库，含十余万条已验证的定义、定理与证明，整体构成一张依赖有向无环图（谁引用了谁）。证明以源码形式存在，其长度可按非空行数统计，因此『证明的代价』第一次有了客观、可数的单位。
本文所有核心量——证明难度、陈述字符数、下游效用——都定义在 Lean 4 代码与 mathlib 依赖图之上。不熟悉这个载体，就无法理解这些度量为什么可计算，也体会不到『行数』作为难度代理的意义与局限。
条件证明难度 V(T|P)
把『证明 T 有多难』建模为相对量：给定可免费引用的前提集合 $P$，推导 $T$ 所需的代价（Lean 证明行数）$V(T|P)$。理想最短证明满足真实性（等于实际行数）、前提单调性（前提越多越容易）与组合性（$V(T|P)\le V(L|P)+V(T|P\cup\{L\})$，取等即 Bellman 方程）三条公理。
它是全文的基石原语：内在趣味性和外在效用都由它组合而成，第 2 节的全部工作就是训练一个满足这些公理的神经网络来预测这个函数。
GRPO（组相对策略优化）
一种面向 LLM 的强化学习算法：对同一个 prompt 采样一组回答（本文每组 8 个），用组内回答的相对优势替代价值网络（critic）来估计优势函数，再配合比例裁剪与 KL 惩罚约束策略更新幅度。实现简单、显存友好，是 DeepSeek-R1 等推理模型的主流后训练方法。
论文两处训练——难度预测器 $V_\theta$（350 步）与定理猜想器（75 步）——都用 GRPO 实现，且奖励以『组内多个角色的预测互相校验』的方式构造，理解 GRPO 才能明白奖励设计如何转化为模型参数更新。
描述长度与柯尔莫哥洛夫复杂度
柯尔莫哥洛夫复杂度 $K(x)$ 指生成 $x$ 的最短程序长度，它不可计算，但确立了『简短描述 + 复杂行为 = 深刻结构』的压缩世界观；MDL（最小描述长度）原则进一步主张好的理论就是对数据的好压缩。在有限语料中，人们用字符数、代码行数等可计算代理来近似这些不可计算的量。
本文的趣味性 $I=$ 证明长度/陈述长度正是这一哲学在形式数学库中的可计算实例；理解这个思想谱系，才能明白定义为何如此设计，以及作者为何在局限中讨论 Levin 复杂度这类变体。
前提扩展与依赖 DAG
mathlib 中每条定理的证明引用若干前提（引理），全体引用构成依赖有向无环图。前提扩展是反事实数据增广：把前提 $L$ 从可见集移除、替换为 $L$ 自己的前提，并把 $L$ 的证明行数累加到目标的难度标签——相当于沿 DAG 回走一步，制造『少给这个引理时证明要多几行』的新样本。
mathlib 高度原子化（证明行数中位数只有 3 行、前提被用次数中位数为 1），直接在原始依赖图上训练得不到有信息量的信号；这一步的数据构造质量决定了难度预测器 $V_\theta$ 的上限。
LLM-as-a-Judge
用强 LLM 按给定评分细则（rubric）对文本打分或排序的评测范式，通常隐藏被评对象的身份（盲评）以减少偏倚。本文用它做两件事：按五级量表评估生成定理被 mathlib 包含的程度（1=不包含，5=完全包含）；以及盲评比较四种提升规则产出的陈述在趣味性、质量与多样性上的高低。
论文多项关键结论（mathlib 重合率从 91.9% 降到 30.6%、盲评 60% 四选一居首）都依赖这一评测方式；了解其协议与潜在偏倚（如评判器与被评模型同源）是正确解读实验结果的前提。
研究动机
LLM 已经能解决大量高难度数学问题——从 IMO 级别赛题到悬置数十年的开放猜想（AlphaProof、FunSearch 等系统的系列成果），Lean 4 形式化验证又保证了这些证明的可靠性。但这恰恰暴露出一个更深层的问题：当机器可以批量提出并证明定理时，它产出的定理是否『有趣』或有用？任意生成真命题只会得到博尔赫斯『巴别图书馆』式的空间——包含所有真理却毫无用处；人类数学历经千年沉淀出的定理集之所以『无理由地有效』（Wigner），正是因为存在某种筛选机制。然而经验研究表明 LLM 对趣味性的判断与人类并不一致，也无法可靠复现人类趣味的多样性。更实际的数据困难在于：mathlib 的依赖图高度原子化——全部 113,547 个声明中证明行数的中位数只有 3 行，任一前提被使用的次数中位数是 1 次，直接在原始依赖图上几乎提取不出难度信号。现有的自动发现系统要么局限于特定领域（TxGraffiti 只处理图不变量），要么依赖人类启发式过滤器，整个领域缺乏一个可计算、可优化、跨领域通用的『什么值得证明』的量化目标。
本文的目标是本文要为自主数学发现系统补上缺失的『选择器』：系统可以生成海量真命题，但必须学会挑选值得证明、值得保留进数学库的那一小部分。目标拆成四个可验证的层次。第一，把证明难度形式化为可计算量：在给定前提集合 $P$ 的条件下推导定理 $T$ 所需的计算代价 $V(T|P)$（以 Lean 证明行数计），并训练一个比 GPT-5.5、Claude Opus 4.6 等前沿模型预测得更准的 27B 模型。第二，给出定理趣味性的可计算定义——陈述长度与证明难度之比——并实证验证它确实捕捉了数学价值：与外在效用（该定理能为整个库节省多少证明代码）强相关。第三，证明这个指标是可优化的：用它作为强化学习奖励后训练语言模型，能系统性地产出更有趣、且与 mathlib 重复度更低的定理。第四，证明该指标在推理时即可发挥作用：作为迭代发现循环中的剪枝/提升规则，驱动一个只靠初始前提就能自我扩张、机器可验证的数学库。
与已有工作不同的是，切入角度的独特之处在于『内在主义』立场。此前的自动发现工作或学习启发式的『内在动机』信号（Poesia、Tsoukalas 等在小公理域内学趣味性目标），或完全依赖人类指定目标（人提猜想、机器证明）。本文主张数学结构本身含有可量化的价值：『容易陈述但难以证明』的命题天然对应人类对深刻的直觉——作者引用 Pólya『定理的优雅正比于能从中看到独立思想的数量、反比于看到它们所需的努力』。技术上，作者把 Bengio 与 Malkin 的信息论观点（有价值的框架描述长度小、又接近大量可证命题）落地为形式库上两个可计算的有限语料代理：趣味性 $I(T|P)=100\,V(T|P)/L(T|P)$ 与效用 $U_0(T)=|\mathcal{D}(T)|\cdot V(T|\emptyset)$。最关键的实证桥梁是：纯内在的 $I_0$ 与纯外在的 $U_0$ 在 mathlib 上 Spearman 相关达 0.756，说明『美学即压缩』不只是哲学口号而是可测规律。这使系统能在提案时用可算的趣味性代替只能事后观测的效用，把『生成有效命题』与『选择有价值的发现』区分开——后者正是此前 LLM 数学系统普遍缺失的能力。
核心方法
直觉先行：一个定理有趣，当且仅当它『用很少的话说了一件很难的事』。技术路线分四步。第一步，数据：从 mathlib 提取 113,547 个声明，用『前提扩展』沿依赖 DAG 反向游走——把前提 $L$ 从前提集中移除、换上它自己的前提、并把 $L$ 的证明行数加到标签——把原子化的库变成 18,318 个训练组的 (定理, 前提集, 证明行数) 三元组。第二步，难度模型：用 GRPO 对 Qwen3.6-27B 后训练 350 步，奖励编码 grounding（贴合真实行数）、Bellman 分解（$V(T|P)=V(L|P)+V(T|P\cup\{L\})$）与前提单调性三条公理。第三步，定义条件描述长度 $L(T|P)$ 与趣味性 $I(T|P)=100\,V(T|P)/L(T|P)$，先在 mathlib 全库验证排序符合直觉（费马大定理特例居顶、$1^n=1$ 垫底），再发现 $I_0$ 与效用 $U_0$ 强相关（$\rho=0.756$）。第四步，两个应用：以 $I$ 为奖励 GRPO 训练『猜想器』生成更有趣的定理；在推理时的迭代发现循环中按真实趣味性对候选排序，每轮只把前 10 名提升进下一轮前提集，形成自我扩张的定理图。
核心创新有三层。第一，把证明难度当作『前提条件化的价值函数』来学，而非无条件评估『这道题多难』。同一定理在不同数学词汇背景下难度完全不同——有测度论词汇时陈述概率定理很容易，只给代数几何前提则极难——$V(T|P)$ 显式建模这种相对性，使趣味性成为相对于当前库的量，天然适配自我扩张场景。第二，趣味性定义为证明行数与条件描述长度之比 $I(T|P)=100\,V(T|P)/L(T|P)$，分母只计入前提词汇未覆盖的新定义字符，这个比值巧妙抵御合取攻击：把 $n$ 个无关定理拼成 $T_1\wedge\cdots\wedge T_n$，难度 $O(n)$ 但趣味性仍 $O(1)$。第三，也是最关键的实证发现：纯内在的趣味性与纯外在的效用 $U_0(T)=|\mathcal{D}(T)|\cdot V(T|\emptyset)$（把该定理免费提供给全库所节省的证明行数）在 mathlib 上 Spearman 相关 0.756——『易陈述而难证明』的定理恰恰是能压缩后续数学的可复用抽象。与已有方法的本质区别：以前的定理证明系统优化『给定目标怎么证』，本文优化『什么目标值得证』，用可学习、机器可验证的代理指标替代不可靠的人类美学判断。
方法步骤详情
完整流水线：①数据构造——对每个根定理 $T$，从 $P=\mathrm{deps}(T)$、$c=\mathrm{lines}(T)$ 出发做 3 次固定种子（31）的随机扩展游走：均匀抽前提 $L$，令 $P^-=P\setminus\{L\}\cup\mathrm{deps}(L)$，标签从 $c$ 变为 $c+\ell$；每条边发 6 种互相校验的角色 prompt（base/keep/remove/lemma_context/lemma_native/base_drop），同根不跨划分。得 18,318 训练组、109,908 条 prompt，标签中位 49 行。②训练 $V_\theta$——GRPO 350 步，奖励为 truth 项 $-|\log V_\theta-\log C|$ 加 Bellman 项与单调 drop 项，组内六角色均值联合计分。③在 4,615 条验证 prompt 上与前沿模型同 prompt 对比 MAE 与 Spearman $\rho$。④训练猜想器——抽 10,000 个前提集（各至少 16 条、中位 77 条），模型只看前提与定义、输出独立 Lean 命题；奖励 $R=0.25+\log(1+V_\theta/L)$，解析失败 $-0.5$、编译失败或与前提无关 $-0.25$、被 assumption/rfl/simp/tauto/simp_all 关闭的平凡命题 0，共 75 步。⑤评估——8 个领域 × 每模型 20 条候选，由 Claude Code + Opus 4.6 证明（含受约束的边际修复），用编译后真实证明行数算真值趣味性，并按五级量表盲评 mathlib 包含度。⑥推理时迭代发现——维护 $P_0\subset P_1\subset\cdots$，每轮收 20 条前提（5 新 15 旧）生成 400 候选，语义过滤去重后送 Lean 证明，按真值趣味性提升前 10 名进入下一轮；$P_0$ 为 80 条图论前提，跑 6 轮。
技术新颖性
技术新颖性有四。其一，结构化 RL 奖励：把三条公理（grounding、前提单调性、Bellman 等式）直接编码进组相对奖励，六个 prompt 角色在组内互相校验——例如 base 角色的预测必须等于 keep 角色与 lemma 角色预测之和——用『一致性约束』代替更多标注，这在难度估计文献中相当新颖。其二，有限语料的复杂度代理：$I$ 与 $U$ 分别对应柯尔莫哥洛夫复杂度与压缩视角的有限语料近似；归一化（除以描述长度、乘 100 使均值约 1）与条件化（相对前提词汇）使它既不可被合取攻击、又随库增长自适应。其三，实证打通内在与外在：0.756 的秩相关为『数学美即压缩』的哲学直觉（Pólya、Thurston）提供首次大规模、机器可验证的定量证据，并说明趣味性可在提案时计算、是效用的事前代理。其四，同一指标双用途：既进奖励函数改变参数（猜想器趣味性均值提升 4.3 倍），又在推理时当剪枝规则（盲评 60% 四选一居首）；消融还证明增益来自比值本身而非偏爱长证明——按纯证明长度剪枝盲评仅 19% 居首。整体上，这是把『趣味性』从主观不可计算的美学判断改造成形式库中可计算、可优化目标的第一份系统性工作。
实验结果
四条实验线。第一，难度预测（Figure 1）：4,615 条验证 prompt 上，$V_\theta$ 的 MAE 为 20.2 行，优于 GPT-5.5 的 31.0 与 Claude 4.6 的 34.3（误差降约 35%）；Spearman $\rho$ 0.912 对 0.776 与 0.815；三模型都低估长证明，但 $V_\theta$ 偏移与离散度最小。第二，度量验证（Figure 2、3）：$I_0$ 全库排序符合直觉——底部是 $1^n=1$ 等代数恒等式，中部是定义前置庞大的分析学，顶部是费马大定理 $n=3,4$；$I_0$ 与效用 $U_0$ 排除零后相关 0.756，几乎不存在高效用低趣味的定理。第三，猜想器训练（Figure 4、5）：真值趣味性均值从 1.76 升至 7.58（约 4.3 倍），8 领域全部提升（组合 2.10× 到数论 8.72×），且全部超过被提示生成有趣定理的 Claude 4.6；与 mathlib 大量/完全重合（4-5 分）的比例从基线 91.9%（Claude 92.5%）降到 30.6%，证明提升不是复述库内内容——样例含四元数平方根刻画、对合矩阵与伴随矩阵等价、乘法幂等基数等非平凡命题。第四，推理时消融（Figure 7、Table 1-4）：趣味性提升规则的提升语句平均 $\hat{I}_{ver}$ 3.899（证明长度剪枝 3.259、随机 1.556、不剪枝 1.313）；提升前候选池均值也最高（2.332 对 1.31–1.69），说明更好的前提库正反馈到后续生成；盲评四选一 60% 排第一（平均名次 1.80），整队质量 3.40±0.52、多样性 2.10±0.32、冗余 28.0%，全面优于其他规则。Figure 6 的图论发现（Tutte 违背者与生成匹配）不在 mathlib 中。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 证明难度预测（4,615 条 mathlib 验证 prompt） | MAE（证明行数，越低越好） | 20.2（$V_\theta$，27B 专用模型） | GPT-5.5：31.0；Claude Opus 4.6：34.3 | 较最强基线降低约 35% 的绝对误差 |
| 证明难度预测（同上验证集） | Spearman 秩相关 ρ | 0.912 | GPT-5.5：0.776；Claude Opus 4.6：0.815 | 较 GPT-5.5 +0.136，较 Claude 4.6 +0.097 |
| 生成定理的真值趣味性（8 领域 × 20 条经 Lean 验证的定理） | 平均条件趣味性 $I(\cdot|P)$ | 7.58（训练后的 27B 猜想器） | Qwen3.6-27B 基线：1.76 | 约 4.3 倍（各领域 2.10×–8.72×），且全部 8 个领域超过 Claude Opus 4.6 |
| 生成定理与 mathlib 的重合度（每模型 160 条，5 级包含度量表） | 评分 4–5（大量/完全包含）占比 | 30.6% | 基线模型 91.9%；Claude Opus 4.6：92.5% | 降低约 61 个百分点 |
| 迭代发现：提升语句质量（80 条图论前提起步，6 轮） | 提升语句平均 $\hat{I}_{ver}$ | 3.899（趣味性剪枝） | 证明长度剪枝 3.259；随机 1.556；不剪枝 1.313 | 较最强基线 +19.6%，较不剪枝约 3 倍 |
| 迭代发现：盲评趣味性（100 组四选一，评判器不知生成策略） | 排名第一比例 / 平均名次 | 60% / 1.80 | 证明长度剪枝 19% / 2.36；不剪枝 13% / 2.89；随机 8% / 2.95 | 排名第一比例较最强基线 +41 个百分点 |
| 迭代发现：整队评估（十条一组，隐藏策略身份） | 质量 / 多样性（1–5 分）/ 冗余率 | 3.40 / 2.10 / 28.0% | 其他三种规则质量 2.40–2.60、多样性 1.20–1.30、冗余 50–53% | 质量与多样性各 +0.8 分，冗余率约减半 |
局限与改进
作者承认的局限：①Lean 证明行数有风格伪影——aesop、grind 等自动化 tactic 常用运行时间换代码长度，作者建议未来考虑 Levin 复杂度；②趣味性未捕捉连接不相关对象、统一分散子领域的价值，效用只是这种连通性的弱形式；③只处理定理陈述，不涉及新数学定义的创造，而定义创新恰是数学史上最有价值的进步之一；④新定理质量与多样性更高，但是否真有助于证明未来的结果尚不清楚；⑤长期运行需要更强的多样性与去重机制。我的观察：$V_\theta$ 的训练与评估全在 mathlib 分布内，对库外领域校准未知；证明器、评判器与基线猜想器之一都是 Claude Opus 4.6 同源模型，存在自偏好与循环验证风险，且边际修复允许弱化结论，部分『发现』实为修补后的命题；$\rho=0.756$ 排除了 $U_0=0$ 的声明，属幸存者样本——新定理效用天然为零，代理关系能否外推无直接证据；趣味性优化可能催生『低级词汇+冗长证明』的策略性命题，75 步 GRPO 的短训练是否出现 reward hacking 值得监控；盲评依赖单一 LLM 判断『有趣』，与该范式想取代的人类美学判断之间仍有鸿沟。
独立分析的弱点
①行数度量可博弈：一行暴力 simp 可能展开数千 kernel 步，模型也可能用绕路证明刷行数。改进：改用 kernel 检查步数、类型检查耗时或 Levin 复杂度 $K^t=\min\{|p|+\log t(p)\}$，或对同一命题的多个验证证明取最短。②$V_\theta$ 分布脆弱：只在 mathlib 上训练，而迭代发现恰恰推向分布外，预测误差随轮次累积。改进：按作者建议在线更新（用证明真值回填），并做不确定性感知剪枝，高方差候选交由真实证明校准。③评判循环同源：质量、多样性、包含度评分全部来自 Claude Opus 4.6，它既是证明器又是基线猜想器宿主。改进：多评判器集成（GPT、Gemini、开源模型）加少量人类数学家盲评锚定，报告评判器间一致性。④效用代理幸存者偏差使『趣味性≈效用』外推缺乏保障。改进：构造合成下游任务——把候选定理加入库后度量后续自动证明任务的行数节省或成功率提升。⑤多样性机制粗糙：冗余率仍 28%，长程运行会陷入同族变体爆炸。改进：定理族嵌入聚类、行列式点过程做多样化采样、探索-利用调度。⑥完全没有定义创造。改进：把描述长度框架扩展到定义层——新定义的趣味性可定义为『用它表述的一族定理获得的压缩增益』与『定义本身长度』之比。
未来方向
作者明确提出的方向：一是把发现对象从定理陈述扩展到有用新定义的自动创造；二是在线学习证明难度——随着前提集扩张，用证明代理的真值输出持续更新 $V_\theta$ 的预测，让度量与库共同进化；三是闭环验证自扩张库中新生成定理的实际用处，即它们是否真能加速未来结果的证明；四是为长期运行系统设计必需的多样性与去重机制。基于本文成果可自然延伸的方向还包括：把趣味性剪枝嵌入树搜索式证明系统（AlphaProof 风格），用 $V(T|P)$ 作为搜索启发式估值，实现『面向发现的搜索』而非『面向目标的搜索』；利用跨领域趣味性矩阵的发现（测度论离开分析学前提后趣味性暴跌、代数在跨领域前提下反而升高）设计领域课程，主动选择『在哪个背景下探索哪个领域』收益最大；把该框架与自动形式化管道（教材到 Lean）结合，对人类研究级猜想按估计趣味性排序，形成人机协作的选题助手；在 Isabelle/HOL、Coq、Metamath 等其他证明助手库上复测 $I$-$U$ 相关性，检验度量的跨系统普适性；以及探索趣味性与已知数学结构不变量（泛性质、对偶性等）的联系，向可解释的数学价值理论推进。
复现评估
复现基础较好但门槛不低。有利条件：基础模型 Qwen3.6-27B 开放权重；训练数据程序化派生自开源 mathlib（113,547 个声明），构造细节充分——种子 31、每根 3 条扩展游走、每边 6 种 prompt 角色、reservoir 采样与停机条件齐备；两张超参表覆盖难度模型（GRPO 350 步、lr $10^{-6}$、batch 384、KL 0.01）与猜想器（75 步、12,288 token 上下文）；Lean 环境用开源 Pantograph，mathlib 版本固定；验证 prompt、包含度 rubric 与全部 judge prompt 全文在附录。障碍：迭代发现与评估依赖专有 API——Claude Code + Opus 4.6 作证明代理（含边际修复）与两类评判器、GPT-5.5 作对比基线，无法完全复现且有持续成本；27B 的 GRPO 训练（131k 上下文）需多卡 H100 级集群；端到端评估每模型要产出 160 条经 Lean 验证的定理，证明成本可观。论文未提及开源代码或数据发布。综合：难度模型的数据管道与奖励设计可独立复现（可行性高），完整复现含前沿对比的全部结论难度中高，预算数千美元 API 费用加相当规模 GPU 时。
论文图表
散点图，每个点是一个 mathlib 定理：横轴是效用 $U_0$（把该定理免费加入库后全库节省的证明行数），纵轴是内在趣味性 $I_0$；排除 $U_0=0$ 的声明后 Spearman ρ=0.756。图中标注了费马大定理（n=3）、组合零点定理、马尔可夫不等式、控制收敛定理、中国剩余定理、Jensen 不等式、Cauchy-Schwarz 不等式、中值定理等的位置。
全文最关键的实证桥梁：证明纯内在的趣味性与纯外在的下游效用强相关，从而为『在提案时用可计算的趣味性作效用的事前代理』这一整个方法论提供依据。
从图论初始前提集 $P_0$ 出发迭代发现到 $P_6$ 的定理依赖图：节点为已验证定理，灰线是 Lean 证明中的显式依赖，绿色深浅编码相对 $P_0$ 的 log10 趣味性，红线追溯 $P_6$ 中最有趣定理的祖先链。图中展示的代表性发现是一条关于『连通分量族是与泛顶点不相交的团且图无 Tutte 违背者时存在满足分量界的生成匹配』的定理，mathlib 中并不存在。
把抽象的迭代发现算法具体化：展示一轮轮自我扩张如何实际运作、发现的定理长什么样、以及后代定理如何复用祖先，是理解第 3.4 节机制的直观入口。