# Learning to Discover Interesting Mathematics

> A quantitative metric of mathematical interestingness, defined as proof difficulty divided by statement length, enables LLMs to autonomously discover novel, useful theorems beyond existing mathematical libraries.

- **Source:** [arXiv](https://arxiv.org/abs/2609.28603)
- **Published:** 2026-09-26
- **Permalink:** https://picx.dev/p/FpylKg
- **Whiteboard:** https://picx.dev/p/FpylKg/image

## Summary

## Summary (Overview)

- This paper introduces a **quantitative definition of mathematical interestingness** as the ratio between proof difficulty and statement description length, enabling automated mathematical discovery without human-provided targets.
- The authors train a **27B parameter LLM to predict conditional proof difficulty** (measured in Lean 4 lines of code) more accurately than frontier general-purpose models like GPT-5.5 and Claude Opus 4.6.
- **Intrinsic interestingness strongly correlates with extrinsic utility** (Spearman $\rho = 0.756$), validating that the metric captures downstream mathematical value.
- Training a conjecturing model with interestingness as a reward **quadruples mean ground-truth interestingness** (from 1.76 to 7.58) and **reduces overlap with mathlib** from 91.9% to 30.6%, demonstrating generation of genuinely novel mathematics.
- An **iterative discovery procedure** using interestingness-based pruning at inference time outperforms baselines (random, longest-proof, keep-all) across quality, diversity, and running mean interestingness.

---

## Introduction and Theoretical Foundation

### Background and Motivation

The paper addresses a critical gap in AI-driven mathematical discovery: while LLMs can increasingly solve advanced mathematical problems—including open problems—they lack a principled notion of *which* statements are worth proving. As the authors note:

> "The space of all true mathematical statements has the same character [as Borges's Library of Babel], whereas mathematics, as it has been created by humans, does not."

The key challenge is defining an **optimizable objective** for autonomous mathematical discovery that:
1. Distinguishes genuinely interesting theorems from trivial-but-valid statements
2. Can be computed without human judgment
3. Correlates with the extrinsic utility of a theorem to downstream mathematics

### Theoretical Foundations

The paper builds on the following conceptual foundations:

- **Proof assistants (Lean 4)** provide a formal, machine-verifiable framework where proof difficulty can be quantified as lines of code.
- **mathlib** provides a large dependency graph of verified theorems, enabling empirical study of proof structures.
- The authors draw on Pólya's aesthetic principle: *"The elegance of a mathematical theorem is directly proportional to the number of independent ideas one can see in the theorem and inversely proportional to the effort it takes to see them."*

### Core Definitions

The central primitive is the **conditional proof difficulty** $V(T \mid P)$—the computational cost of deriving theorem $T$ from premises $P$. This satisfies three axioms:

$$
\text{(A1) grounding:} \quad V(T \mid P) = C_{\mathcal{D}}(T \mid P)\tag{1}
$$

$$
\text{(A2) premise monotonicity:} \quad V(T \mid Q) \leq V(T \mid P)\tag{2}
$$

$$
\text{(A3) composition:} \quad V(T \mid P) \leq V(L \mid P) + V(T \mid P \cup \{L\})\tag{3}
$$

With equality in (A3) giving the **Bellman relation**:

$$
V(T \mid P) = V(L \mid P) + V(T \mid P \cup \{L\})\tag{4}
$$

---

## Methodology

### 3.1 Dataset Generation via Premise Expansion

Since raw mathlib proofs have median length of only 3 lines, the authors employ **premise expansion**: iteratively unrolling lemmas backward through the dependency DAG. For a theorem $T$ with premise $L$, one expansion step transforms premises $P(T) \to P(T) \cup P(L) \setminus \{L\}$, adding the proof length of $L$ to the label. This produces a richer dataset of ~100K (theorem, premises, proof-length) triplets.

### 3.2 Training the Difficulty Predictor

The authors fine-tune **Qwen3.6-27B** using **GRPO** (Group Relative Policy Optimization) with a composite reward designed to satisfy the axioms:

$$
\mathcal{R} = -\left|\log V_\theta(T|P) - \log C_{\mathcal{D}}(T|P)\right| \quad \text{(truth)}
$$

$$
- \left|\log V_\theta(T|P) - \log\left(V_\theta(L|P) + V_\theta(T|P \cup \{L\})\right)\right| \quad \text{(Bellman)}
$$

$$
- \max\left\{0, \log V(T|P) - \log V(T|P \setminus Q)\right\} \quad \text{(drop)}
$$

The model is evaluated on 4,615 held-out validation prompts using MAE and Spearman rank correlation.

### 3.3 Defining Interestingness and Utility

**Conditional description length** (accounting for definitions needed to state $T$ given premises $P$):

$$
L(T \mid P) = S(T) + \sum_{d \in C(T) \setminus C(P)} S(d)\tag{5}
$$

**Conditional interestingness**:

$$
I(T \mid P) = 100\frac{V(T \mid P)}{L(T \mid P)}\tag{6}
$$

**Utility** (lines of code saved across the library if $T$ is available):

$$
U_0(T) = |D(T)| \cdot V(T \mid \emptyset)\tag{7}
$$

**Training reward** for the conjecturer:

$$
R(T, P) = 0.25 + \log\left(1 + \frac{I_\theta(T \mid P)}{100}\right)\tag{8}
$$

### 3.4 Training the Conjecturer

- Conditioned on sets of ≥16 premises (median 77) from mathlib's training split
- Emits standalone Lean propositions
- Reward: +0.25 baseline for valid/nontrivial statements, −0.25 for irrelevant/invalid, −0.5 for parse failures, 0 for trivially provable statements
- Evaluated against base Qwen and Claude 4.6 on 8 mathematical areas (20 proven statements per model per area)

### 3.5 Iterative Discovery at Inference Time

Starting from premises $P_0$, each round:
1. Conjecturer (Claude 4.6) proposes 400 candidate statements from 20 premises
2. Semantic filter removes duplicates and enforces diversity
3. Statements proved independently via Claude Code in Lean
4. **Top-10 by ground-truth interestingness** promoted to $P_n$

Compared against: keep-all, random-10, and longest-proof-10 rules over 6 rounds.

---

## Empirical Validation / Results

### Difficulty Prediction Quality

**Figure 1** demonstrates that the trained model substantially outperforms GPT-5.5 and Claude Opus 4.6 on held-out mathlib samples:
- Better calibration across all proof-length bins
- All models underestimate long proofs, but the trained model is far closer to optimal
- Lower MAE and higher Spearman $\rho$ on 4,615 validation prompts

### Interestingness Distribution Analysis

**Figure 2** validates the metric's intuitive ordering:
- **Bottom decile**: Simple algebraic identities (e.g., $1^n = 1$)
- **Middle**: Analysis theorems (large definitional prerequisites)
- **Top**: Famous hard-to-prove statements (e.g., Fermat's Last Theorem for exponent 3)

### Utility-Interestingness Correlation

**Figure 3** shows a **Spearman correlation of 0.756** between utility $U_0$ and interestingness $I_0$ (excluding zero-utility statements). Key finding: high interestingness without high utility exists, but high utility without interestingness is rare.

### Conjecture Quality After Training

**Figure 4** shows dramatic improvement:
- **Mean interestingness**: 1.76 (base Qwen) → 7.58 (trained model)
- **Area-level ratios**: 2.10× (combinatorics) to 8.72× (number theory)
- Trained model beats Claude Opus 4.6 in all eight areas

**Figure 5** shows novelty gains:
- Statements substantially/fully contained in mathlib: **91.9% (base) → 30.6% (trained)**
- Claude baseline: 92.5% overlap

### Iterative Discovery Results

**Figure 7** comparison of promotion rules over 6 rounds:

| Metric | Interestingness Pruning | Longest Proof | Random | Keep All |
|--------|------------------------|---------------|--------|----------|
| Running mean interestingness | **Highest** | Lower | Lower | Lowest |
| LLM-judge quality score | **Highest** | Lower | Lower | Lower |
| LLM-judge diversity score | **Highest** | Lower | Lower | Lower |
| "Most interesting" ranking share | **Highest** | Lower | Lower | Lower |

Key insight: pruning by raw proof length alone performs worse than interestingness, confirming that the *ratio* (not just length) matters.

**Figure 6** showcases a discovered theorem graph where the most interesting theorem in $P_6$ traces ancestry through multiple generations of premises.

---

## Theoretical and Practical Implications

### Contributions to Mathematical Discovery

1. **A concrete, optimizable objective**: Interestingness $I(T \mid P) = V(T \mid P)/L(T \mid P)$ provides a computable target for autonomous systems that requires no human judgment.

2. **Validated proxy for utility**: The strong correlation with downstream utility suggests that optimizing for interestingness yields theorems that compress future proofs—addressing the "unreasonable effectiveness" of mathematics.

3. **Out-of-distribution generation**: A 3× reduction in mathlib overlap demonstrates that training against intrinsic metrics moves models beyond the "convex hull" of existing mathematics.

4. **Self-expanding libraries**: The iterative procedure shows a system can build on its own discoveries, with interestingness-provided pruning maintaining quality across generations.

### Methodological Considerations

- **Proof length as proxy**: Line counts can be stylistic artifacts; automation tactics (aesop, grind) trade length for runtime. Alternative notions like **Levin complexity** may provide richer signals.
- **Limited scope of interestingness**: The metric captures intrinsic difficulty but not cross-field connectivity or unification of disparate areas—a potentially important aspect of mathematical value.

---

## Conclusion

This paper demonstrates that **quantitative, structural metrics of mathematical interestingness** can effectively guide autonomous mathematical discovery. The key takeaways:

1. **Conditional proof difficulty** can be learned more accurately than frontier LLMs provide
2. **Interestingness** (proof length / statement length) correlates with extrinsic utility and is optimizable via RL
3. **Interestingness-optimized conjecturers** produce more novel, out-of-distribution theorems
4. **Iterative discovery** with interestingness pruning builds high-quality, self-expanding mathematical libraries

### Future Directions

- **Definition creation**: Extending discovery beyond theorem statements to new, useful definitions
- **Online difficulty estimation**: Updating proof-length predictions as the premise set expands
- **Cross-field connectivity**: Quantifying the "unification" value of theorems that connect disjoint mathematical areas
- **Diversity mechanisms**: Developing better deduplication and diversity preservation for long-running discovery systems
- **Levin complexity**: Exploring richer alternatives to line-count-based difficulty

> "Our results offer a proof of concept that interesting self-expanding mathematical libraries, grown without human intervention beyond the initial premises, are feasible."

The work provides a foundational framework for moving from LLMs that *solve* problems to systems that *choose* which problems are worth solving—a critical step toward genuine autonomous mathematical research.

---

_Markdown view of https://picx.dev/p/FpylKg, served by PicX — AI-generated visual whiteboard summaries of research papers._