# Learning to Discover Interesting Mathematics：用有趣度指标引导模型自动发现数学定理

- 来源：HuggingFace Daily Papers（社区热门论文）
- 发布时间：2026-09-23 08:00
- AIHOT 分数：52
- AIHOT 链接：https://aihot.news/items/cmuhiyya20az6rojnzzdgfazt
- 原文链接：https://arxiv.org/abs/2609.28603

## AI 摘要

论文提出用证明长度与陈述长度之比衡量定理的内在有趣度，并证明其与下游实用性相关。作者训练了一个 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.