让模型学会发现什么样的数学值得研究

导语

过去几年，大型语言模型在数学推理和形式化证明上的能力持续提升，甚至开始处理曾长期未被解决的问题。新的瓶颈也随之出现：当模型能够提出并证明越来越多定理时，如何判断其中哪些真正有趣、值得进一步研究？

论文《Learning to Discover Interesting Mathematics》没有把重点放在“证明成功率”上，而是尝试为数学发现建立一个可计算的筛选信号。研究者希望模型不仅能完成证明，还能主动避开重复已有知识，寻找更具结构性和潜在用途的结果。

核心方法

• 用证明与命题的长度比衡量有趣性。 研究将定理的内在有趣性定义为证明长度与命题表述长度之比。直观而言，一个简洁陈述却需要较长、较丰富推导的命题，可能比冗长陈述下的直接结论更值得关注。
• 把条件化证明难度作为基础能力。 评估一个候选定理时，模型需要知道在给定前提和已有知识的情况下，证明它究竟有多难。研究团队据此训练了一个27B规模的模型，用于预测条件化证明难度，并报告其表现优于前沿通用模型。
• 让模型生成、筛选并迭代。 系统先提出候选命题，再依据有趣性指标排序，最后把经过验证的结果加入不断扩展的数学库，作为后续发现的基础。

结果与意义

按照论文摘要，优化后的系统使生成定理的有趣性提高了4.3倍。同时，与Mathlib存在大部分或完全重叠的结果比例从91.9%降至30.6%，说明模型不再主要围绕现有库进行近似复述，而是更频繁地产生分布外的形式化数学内容。

这项工作的价值并不在于宣称模型已经能够独立完成数学研究，而在于提出了一种研究方向：把“研究价值”从模糊的人类判断，转化为可以参与训练、排序和搜索的工程信号。如果这一指标与实际效用之间的关联能够在更广泛的数学领域得到验证，它就可能帮助系统把有限的证明计算预算投入更值得探索的猜想。

当然，证明长度并不等同于数学重要性。一个证明很长的定理可能只是表达方式低效，短证明也可能对应极其深刻的结果。因此，指标更适合作为候选筛选工具，而非最终评价标准。未来仍需要数学家参与判断新结果的概念价值、可迁移性和实际用途。

从更长远看，这项研究描绘了一种自扩展、机器验证数学库的雏形：模型提出命题，形式化系统检查证明，评估模型进行排序，再将可靠且有潜力的结果反馈给下一轮搜索。真正的挑战将是让这种循环不仅产生“更难的证明”，也产生人类愿意继续研究的数学。

来源：Hugging Face Daily Papers