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:

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.