标题Learning to Discover Interesting Mathematics来源arXiv, 2609.28603v1️文章简介研究问题大语言模型虽然能解决数学难题但如何判断它们生成的新定理是否真的“有趣”或有用而不是仅仅在重复已知知识主要贡献论文提出了一种量化数学定理“趣味性”的指标并训练了一个专用模型来预测证明难度成功引导AI自主发现新颖且有价值的数学定理。重点思路定义内在趣味性将定理的趣味性定义为“证明长度”与“陈述长度”的比值。即一个定理如果表述很简单字符少但证明过程很复杂代码行数多则被认为具有高内在趣味性。构建难度预测器识别出“给定前提下的证明难度”是计算趣味性的核心要素。作者利用Lean 4形式化数学库mathlib的数据通过“前提扩展”技术构建数据集微调了一个270亿参数的语言模型使其能比通用前沿模型更准确地预测证明所需的代码行数。验证趣味性与实用性的关联定义了定理的“实用性”为引入该定理后能压缩多少后续证明的代码量。实验发现内在趣味性与这种外在实用性高度正相关说明简单的趣味性指标能有效反映定理的价值。优化生成与迭代发现利用趣味性指标作为奖励信号对模型进行强化学习训练使其倾向于生成高趣味性定理。同时设计了推理时的剪枝算法在多轮迭代中只保留最有趣的已验证定理作为下一轮的前提实现数学库的自我扩张。分析总结预测更精准训练后的27B模型在预测证明难度上其准确率和校准度均显著优于GPT-5.5和Claude Opus 4.6等通用大模型。生成更有趣经过趣味性优化的模型其生成定理的平均趣味性提升了四倍以上且生成的定理在数学各个分支中均表现优异。内容更新颖优化后的模型生成的定理与现有mathlib库的重叠率从91.9%大幅降至30.6%证明该系统能创造出大量分布外Out-of-distribution的新颖数学知识而非简单复述已有内容。迭代效果佳在递归发现实验中基于趣味性评分筛选定理的策略在定理质量、多样性和被人类专家判定为“最有趣”的比例上均优于随机筛选或仅按证明长度筛选的策略。个人观点论文将抽象的“数学美感”转化为可计算的工程指标利用形式化证明中的“代码行数”作为难度的代理变量用“陈述简洁但证明艰难”这一直观逻辑来定义趣味性。