Recently, Large Language Models (LLMs) have been increasingly able to solve advanced mathematical problems, including many that have been open for decades. This opens the door to expansion of mathematical knowledge at unprecedented scale. Yet, while LLMs may be able to conjecture and prove more and more theorems, it remains open whether this new mathematical knowledge is interesting or useful. We define intrinsic interestingness of a theorem as the ratio between the length of its proof and the length of its statement. We show that this correlates strongly with an extrinsic measure of the downstream utility of a theorem. We identify the difficulty of a proof conditioned on a set of premises as a useful primitive for computing these metrics, and train a 27B model that predicts proof difficulty more accurately than frontier general-purpose models. Optimizing for our metric creates a model capable of producing more interesting theorems, while also reducing substantial or full overlap with Mathlib from 91.9% to 30.6%, showcasing the creation of more out-of-distribution math. We show that our system can generate candidate theorems, select the most interesting among them, and iteratively build on a self-expanding mathematical library. These metrics provide a practical and quantifiable signal for ranking conjectures and guiding proof search within formal mathematical libraries. Our framework provides a path towards self-expanding, machine-verified mathematical libraries that can choose worthwhile statements without relying on human-supplied targets.
Figures & tables
Figure 1: The trained value is substantially better calibrated on held-out samples from mathlib . The left panel groups examples by observed proof length, points give the mean observed and mean predicted proof lines, and shaded bands the interquartile range of predictions within each bin. The dashed line represents what we would expect from an optimal predictor. Note that all models underestimate proof length with increased length. The right plots report matched MAE and Spearman ρ on all 4,615 validation prompts.
Figure 2: Quantifying the interestingness of a statement. Here we show the distribution of interestingness I0 , as defined in Section 3.1 , of all statements from mathlib . The resulting ordering is intuitive, with basic algebraic identities at the bottom, analysis in the middle because its definitional prerequisites are enormous, and theorems that are famously easy to state but hard to prove, like Fermat’s Last Theorem for exponent 3, at the top.
Figure 3: Utility and interestingness are correlated. Each point is a mathlib theorem. Utility U0 , defined in Section 3.2 , is the number of lines of code saved across the library when the theorem is admitted as a premise, while interestingness I0 , defined in Section 3.1 , is the ratio between a theorem’s proof length and description length. Excluding the declarations with U0=0 gives a Spearman ρ=0.756 .
Figure 4: Training shifts generated theorems toward higher ground-truth interestingness. Our trained 27B model is consistently able to produce more interesting statements, with 20 statements per coarse area. Left: kernel densities estimator (KDE; a method that smooths the observed histogram with a kernel to give a continuous density estimate) fitted in log10 -interestingness space over all 160 outcomes per model. Right: mean ground-truth interestingness by mathematical area over the same complete cohort, shown on a logarithmic radial scale from 0.5 to 20. Colors identify the same models in both panels.
Figure 5: Interestingness training reduces overlap with existing mathlib content. For each model we take the 160 statements from Figure 4 , and judge to what degree each statement is contained within mathlib . Appendix C.2.2 gives the rubric, prompt, and protocol.
Figure 6: Iterative forward discovery builds a reusable theorem graph. Here we showcase a result from our iterative forward discovery algorithm introduced in Section 3.4 . Green shade encodes log10 total interestingness relative to P0 on a per-figure scale. The red lines trace the ancestry of the most interesting theorem introduced in P6 . More such graphs can be found in Figure 12 in Appendix C.2 .
Figure 7: Interestingness pruning is the most effective inference-time pruning criterion. Left three panels: LLM judge scores over all 6 rounds for cohort quality and diversity (Table 4 ) and the share of four-way comparisons in which each rule’s statement is ranked most interesting (Table 3 ). Right: running mean of the verified interestingness of each set Pn through P6 . More experiments are available in Appendix D .
Appendix figures & tables6 assets
Supplementary material from the paper’s appendix.
Appendix
Promotion rule
Mean Iver
Median Iver
Mean proof lines
No pruning
1.313
1.114
3.80
Random
1.556
1.175
4.39
Proof length
3.259
2.480
11.48
Interestingness
3.899
3.380
7.41
Appendix
Table 1: Quality of the promoted statements
Promotion rule
Mean Iver
Median Iver
Mean proof lines
No pruning
1.313
1.114
3.80
Random
1.461
1.271
3.74
Proof length
1.694
1.167
5.46
Interestingness
2.332
1.754
4.56
Appendix
Table 2: Verified candidates before selection.
Promotion rule
Ranked first
Ranked in top two
Mean rank ↓
No pruning
13%
34%
2.89
Random
8%
29%
2.95
Proof length
19%
64%
2.36
Interestingness
60%
73%
1.80
Appendix
Table 3: Direct policy-blinded judgment of mathematical interestingness.
Promotion rule
Quality (1–5)
Diversity (1–5)
Families per ten
Redundant
No pruning
2.50±0.53
1.30±0.48
2.60±0.97
50.0%±26.7%
Random
2.40±0.52
1.20±0.42
2.90±0.99
53.0%±18.9%
Proof length
2.60±0.52
1.30±0.48
2.90±0.74
50.0%±18.3%
Interestingness
3.40±0.52
2.10±0.32
3.50±0.71
28.0%±7.9%
Appendix
Table 4: Policy-blinded cohort judgment. Entries are mean ± sample standard deviation across the ten round-level cohorts for each promotion rule.
Figure 8: Full cross-area interestingness matrix. Each cell is the median target-wise ratio for the row area under premises from the column area versus the same-area premise condition. All premise frontiers are synchronously expanded through three rounds before new predictions are obtained. We select ten targets per area (120 total); four row areas contribute nine ratios after each excludes one non-positive same-area score. Asterisks mark 95% confidence intervals that exclude one.
Figure 9: Algebra. For monic q and r , reducing pr modulo qr equals reducing p modulo q and then multiplying by r .
School of Computer Science Beijing University of Posts and Telecommunications Beijing, China · Graduate College for Engineers Beijing University of Posts and Telecommunications Beijing, China · School of Mathematical Sciences Fudan University Shanghai, China +6