---
title: "What makes a theorem interesting? Operationalizing interestingness for open-ended exploration"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2611.02905v1"
permalink: "https://feed.astralor.com/items/itm_f3f8d31307bc7462af775c23"
published: "2026-11-02T10:38:23.000Z"
score: 58
channel: "ai"
tags: ["AI Agent","推理效率","What","Operationalizing","Interestingness","One"]
---

# What makes a theorem interesting? Operationalizing interestingness for open-ended exploration

## 速览

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 mode…

## 关键点

- 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.

## 全文

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.

---

引用前请核对原文;本文由星际流动整理:https://feed.astralor.com/items/itm_f3f8d31307bc7462af775c23