Learning to Discover Interesting Mathematics

Recently, Large Language Models (LLMs) have been increasingly able to solve advanced mathematical problems, including a few that have been open for decades, while automatically verifying their own proof. 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 identify the difficulty of a proof conditioned on a set of premises as a useful primitive for answering these questions, and train a 27B model that predicts proof difficulty more accurately than frontier general-purpose models. We define intrinsic interestingness as proof difficulty relative to statement description length and show that it correlates strongly with an extrinsic measure of the downstream utility of a theorem. Optimizing for our metric creates a model which is 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.