是什么让一个定理有趣？将趣味性操作化以支持开放式探索

一个进行探索的智能体，无论是生成猜想还是研究构想，都必须决定哪些值得保留。这种对趣味性的判断通常交由人工挑选的代理指标或语言模型完成，但两者是否符合人类真正重视的东西，目前都不得而知。我以数学定理为研究对象，通过观察数学家在形式化库和论文中特别挑选出哪些结果来研究这一问题。我将每一种挑选结果的方式建模为一个评估器，对结果的陈述、证明及依赖关系的特征赋予权重，并将这些权重分为共享部分和主观部分。在形式化数学中，事前特征对这些选择的预测能力与大型语言模型评判器相当，且两者能够互补。趣味性也在很大程度上具有共性。一组权重能够解释大部分信号，并能在不同形式化库之间实现部分迁移；这些权重主要落在结构性特征上，例如陈述和证明的长度，以及证明所借助的数学分支。剩余的主观部分更多取决于实践惯例和作者个人，而非数学分支。评判器的优势在于其对经典成果的了解，而且无论是评判器还是这些特征，都不依赖对论文的记忆。这种根据一个共同体特别挑选的内容来推断其认为什么有趣的方法，也可应用于其他科学领域。