What makes a theorem interesting? Operationalizing interestingness for open-ended exploration
Silvère Gangloff
cs.AI
Nov 2, 2026 · v1
TL;DR
Uses Mathlib's hand-written theorems, with statement, proof and dependency features and curated 'main results' labels, as the main corpus for modeling theorem interestingness.
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.
Problem
Exploring agents must decide which conjectures or results are worth keeping. That judgment of interestingness is usually delegated to hand-picked proxies or language models, and neither is known to match what humans value.
Approach
Interestingness is inferred from which theorems mathematicians single out in formal libraries and papers. Examples are module 'Main results' docs in Mathlib and lists such as Wiedijk's 100 theorems. Each selection mechanism is modeled as an evaluator that weights ex-ante features of a theorem's statement, proof and dependencies, with weights split into shared and subjective parts. Corpora are Mathlib, Metamath, HOL Light and 20k arXiv papers, and the features are compared against an LLM judge.
Results
In formalized mathematics, ex-ante features predict selections about as well as an LLM judge, and the two are complementary. A shared set of weights, dominated by structural features such as statement and proof length and the subfields drawn on, explains most of the signal and partly transfers across libraries. The LLM judge's advantage comes from knowledge of the canon; the extraction, features, labels and protocols are released.
