Interesting features predict which theorems mathematicians value most
What makes a theorem interesting? Operationalizing interestingness for open-ended exploration
Artificial Intelligence
Summary
When mathematicians explore new ideas, they must decide which ones are worth remembering. This paper studies what makes a mathematical theorem interesting by looking at which results experts pick out in formal libraries and papers. The authors find that most interestingness can be predicted from structural features like the length of the statement and proof and the fields involved. They also show that a language model judge and these features complement each other, and that interestingness is mostly shared across mathematicians, with some subjectivity depending on individual authors.
What this means in practice
- •For mathematical knowledge base developers: Improve automated systems that highlight valuable theorems for mathematicians by using structural features of statements and proofs.
- •For ai model designers: Enhance language models judging mathematical results by combining them with features reflecting what mathematicians find interesting.
Authors
Silvère Gangloff
Abstract
An agent that explores, whether it generates conjectures or research ideas, must decide which of them are worth keeping. This judgment of interestingness is usually delegated to a hand-picked proxy or to a language model, neither of which is known to correspond to what humans actually value. I study it for mathematical theorems, by observing which results mathematicians single out in formal libraries and in papers. I model each way of singling out results as an evaluator that weights features of a result's statement, its proof and dependencies, and split its weights into a shared and a subjective part. In formalized mathematics, ex-ante features predict these selections as well as a large language-model judge, and the two complement each other. Interestingness is also largely shared. One set of weights, carried mostly by structural features such as the length of the statement and of the proof and the subfields the proof draws on, accounts for most of the signal and transfers in part across formal libraries. What remains subjective depends on practices and individual authors more than on subfields. The judge's advantage lies in its knowledge of the canon, and neither the judge nor the features rely on memory of the papers. The approach, which infers what a community finds interesting from what it singles out, can be applied to other sciences.