Learning to Discover Interesting Mathematics

The paper defines the intrinsic interestingness of a theorem as the ratio between its proof length and statement length, correlating strongly with downstream utility. The authors train a 27B model to accurately predict proof difficulty. Optimizing for this metric yields a model capable of producing more interesting theorems while reducing overlap with Mathlib from 91.9% to 30.6%, showcasing out-of-distribution math creation. The system can generate candidates, select the most interesting ones, and build a self-expanding mathematical library.

A 27B model is trained that predicts proof difficulty more accurately than frontier general-purpose models.

Optimizing for our metric reduces substantial or full overlap with Mathlib from 91.9% to 30.6%.