Learning to Discover Interesting Mathematics

Large language models have recently become increasingly able to solve advanced mathematical problems, including many that had been open for decades, opening the door to expanding mathematical knowledge at unprecedented scale. However, while LLMs may conjecture and prove more theorems, it remains an open question whether the resulting knowledge is interesting or useful.

To address this, the paper defines the intrinsic interestingness of a theorem as the ratio between the length of its proof and the length of its statement. It shows this metric correlates strongly with an extrinsic measure of a theorem's downstream utility. The authors 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 this metric produces a model capable of generating more interesting theorems. It also reduces substantial or full overlap with Mathlib from 91.9% to 30.6%, demonstrating the creation of more out-of-distribution mathematics. The system can generate candidate theorems, select the most interesting among them, and iteratively build on a self-expanding mathematical library.

Overall, the proposed metrics provide a practical and quantifiable signal for ranking conjectures and guiding proof search within formal mathematical libraries. The framework offers a path toward self-expanding, machine-verified mathematical libraries that can choose worthwhile statements without relying on human-supplied targets.