Researchers propose a method to identify interesting mathematical theorems by measuring the ratio of proof length to statement length, which correlates with practical utility. They train a 27B model to predict proof difficulty and develop a system that generates novel theorems, selects the most interesting ones, and iteratively builds self-expanding mathematical libraries with reduced overlap to existing resources.