AI 数学家的新标准：什么定理值得证明
大模型已经能解出一些困扰人类几十年的数学难题，但一个更尴尬的问题浮出水面：它证明出来的东西，到底有没有人关心？这篇论文给了一个反直觉的答案——定理的「有趣程度」可以用一个冷冰冰的比值来衡量：证明长度除以陈述长度。比值越高，说明一句话能引出很长的推理，越值得研究；而且这个比值和定理在后续研究中的实际用处高度相关。研究者训练了一个 270 亿参数的模型来预测证明难度，用它筛选候选定理，结果生成的新定理和现有数学库的重叠率从 91.9% 降到 30.6%，也就是说它开始产出人类没写过、但逻辑上成立的新数学。这不是你明天能用上的工具，但它第一次给了机器一个「什么值得证明」的客观标准，让 AI 数学研究从碰运气变成可筛选的流水线。
📄 原文摘要(英文)
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.