发表机构
CERMICS, ENPC, Institut Polytechnique de Paris; New York University（巴黎高科路桥学校 CERMICS 实验室，巴黎综合理工学院; 纽约大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出以证明与陈述长度比定义定理趣味性，训练27B模型预测证明难度，生成更有趣且分布外的数学定理，并构建自我扩展的数学库。
AI 中文摘要
近年来，大型语言模型（LLMs）越来越能够解决高级数学问题，包括许多已经开放数十年的问题。这为以前所未有的规模扩展数学知识打开了大门。然而，尽管LLMs可能能够推测并证明越来越多的定理，但这些新的数学知识是否有趣或有用仍然是一个未解决的问题。我们将定理的内在趣味性定义为其证明长度与陈述长度之比。我们表明，这与定理下游效用的外在度量密切相关。我们确定了在给定一组前提条件下证明的难度作为计算这些度量的有用原语，并训练了一个27B模型，该模型比前沿通用模型更准确地预测证明难度。针对我们的度量进行优化，创建了一个能够产生更有趣定理的模型，同时将定理与Mathlib的大量或完全重叠从91.9%降低到30.6%，展示了更多分布外数学的生成。我们表明，我们的系统可以生成候选定理，从中选择最有趣的定理，并迭代地构建一个自我扩展的数学库。这些度量提供了一种实用且可量化的信号，用于对猜想进行排序并指导形式数学库中的证明搜索。我们的框架为自我扩展、机器验证的数学库提供了一条路径，这些库可以在不依赖人类提供的目标的情况下选择有价值的陈述。
英文摘要
Recently, Large Language Models (LLMs) have been increasingly able to solve advanced mathematical problems, including many that have been open for decades. This opens the door to expansion of mathematical knowledge at unprecedented scale. Yet, while LLMs may be able to conjecture and prove more and more theorems, it remains open whether this new mathematical knowledge is interesting or useful. We define intrinsic interestingness of a theorem as the ratio between the length of its proof and the length of its statement. We show that this correlates strongly with an extrinsic measure of the downstream utility of a theorem. We identify the difficulty of a proof conditioned on a set of premises as a useful primitive for computing these metrics, and train a 27B model that predicts proof difficulty more accurately than frontier general-purpose models. Optimizing for our metric creates a model capable of producing more interesting theorems, while also reducing substantial or full overlap with Mathlib from 91.9% to 30.6%, showcasing the creation of more out-of-distribution math. We show that our system can generate candidate theorems, select the most interesting among them, and iteratively build on a self-expanding mathematical library. These metrics provide a practical and quantifiable signal for ranking conjectures and guiding proof search within formal mathematical libraries. Our framework provides a path towards self-expanding, machine-verified mathematical libraries that can choose worthwhile statements without relying on human-supplied targets.
