NYU paper scores theorem 'interestingness' as proof length over statement length and cuts Mathlib overlap from 91.9% to 30.6%

arXiv / HuggingFace Daily Papers·medium signalXBlueskyLinkedInCopy link

arXiv 2609.28603 (23 Sep; Patel, Rammal, Hayat, Munos, Kempe) defines a theorem's intrinsic interestingness as the ratio of its proof length to its statement length, and shows the ratio correlates with how useful the theorem is downstream. The team trains a 27B model that predicts proof difficulty better than frontier general models. Optimizing for the metric drops substantial or full overlap with Mathlib from 91.9% to 30.6%, and the system grows its own theorem library over successive rounds. It targets the question this month's AI-solved problems raised: which new results deserve a human's attention.