学习发现有趣的数学

最近，大型语言模型（LLM）越来越能够解决高级数学问题，包括许多已经开放了几十年的问题。这为数学知识以前所未有的规模扩展打开了大门。然而，虽然大语言模型可能能够猜想并证明越来越多的定理，但这种新的数学知识是否有趣或有用仍然悬而未决。我们将定理的内在趣味性定义为其证明长度与其陈述长度之间的比率。我们表明，这与定理下游效用的外在度量密切相关。我们将一组前提条件下的证明难度确定为计算这些指标的有用原语，并训练一个 27B 模型，该模型比前沿通用模型更准确地预测证明难度。针对我们的指标进行优化创建了一个能够产生更有趣的定理的模型，同时还将与 Mathlib 的大量或完全重叠从 91.9% 减少到 30.6%，展示了更多分布外数学的创建。我们证明我们的系统可以生成候选定理，选择其中最有趣的定理，并迭代地构建一个自我扩展的数学库。这些指标为在正式数学库中对猜想进行排名和指导证明搜索提供了实用且可量化的信号。我们的框架提供了一条通往自我扩展、机器验证的数学库的道路，这些数学库可以选择有价值的语句，而不依赖于人类提供的目标。