Learning to Discover Interesting Mathematics

AI summary

Overview

• Research area: Machine learning for formal mathematics — automated conjecture generation, proof-difficulty modeling, and reinforcement learning, all grounded in the Lean 4 proof assistant and its mathlib library.
• Technical level: Advanced. The paper assumes familiarity with LLM post-training (GRPO), formal theorem provers, and information-theoretic notions of description length.
• Scope: The paper proposes a computable definition of "interestingness" for mathematical statements, trains a model to predict conditional proof difficulty, and uses the resulting metric to train a conjecturer and to prune an iterative, self-expanding theorem-discovery loop.

What This Paper Is About

LLM-based provers can now verify theorems in Lean 4, but nothing in that pipeline decides which statements are worth proving — the space of all true statements is dominated by trivial or useless results. The paper defines a theorem's intrinsic "interestingness" as the ratio of its proof length to the length of its statement, argues this correlates with the theorem's downstream usefulness, and uses it as an optimizable reward. The goal is a system that proposes, selects, and builds on interesting theorems without human-supplied targets.

Key Contributions

1. A formalized notion of conditional proof difficulty. The authors define V(T|P), the computational cost in lines of code of deriving theorem T from premises P in Lean 4, and state three axioms it should satisfy: grounding, premise monotonicity, and composition (a Bellman-type relation). They post-train a 27B-parameter LLM on roughly 100k mathlib-derived data points and report that it predicts difficulty more accurately and is better calibrated than frontier general-purpose models.

2. A definition of interestingness and a demonstration that it tracks utility. Interestingness is defined as I(T|P) = 100 · V(T|P) / L(T|P), where L(T|P) is the conditional description length — the characters needed to state the theorem plus any definitions it requires that the premises do not already supply. A separate utility measure U₀(T) = |D(T)| · V(T|∅), counting the downstream theorems that cite T times its unconditional proof cost, is shown to correlate with interestingness at a Spearman ρ of 0.756 when declarations with U₀ = 0 are excluded.

3. A trained conjecturer that produces more interesting and less derivative statements. Training with the interestingness reward quadruples mean interestingness (measured against real proofs) relative to the base model, and cuts the share of statements judged substantially or fully contained in mathlib from 91.9% to 30.6%.

4. An inference-time discovery loop. Applying the metric as a pruning rule in a recursive loop that promotes the ten highest-interestingness verified statements per round produces nontrivial statements absent from mathlib, and outperforms pruning by raw proof length, random promotion, and retaining everything.

Main Findings

• Proof-difficulty prediction: On a held-out validation set of 4,615 labeled prompts, the fine-tuned Qwen3.6-27B is substantially more accurate and better calibrated than GPT-5.5 and Claude Opus 4.6. All three models tend to underestimate proof length as length grows. The exact MAE and Spearman ρ values are reported in Figure 1 rather than as numbers in the text, and the paper notes both metrics are computed only over parsed non-negative answers.
• Interestingness is intuitive on existing mathematics: Ranking all mathlib statements by I₀ puts simple algebraic identities such as 1^n = 1 in the bottom decile, analysis in the middle (because its definitional prerequisites are large), and results such as the exponent-3 special case of Fermat's Last Theorem at the top.
• Intrinsic interestingness predicts extrinsic utility: Utility U₀ is by construction extrinsic — it depends on how many later theorems cite a result — yet it correlates with the intrinsic measure at Spearman ρ = 0.756. The authors note that few statements have high graph utility without high interestingness, while some have high interestingness but low utility.
• Training shifts generated theorems: Pooled across eight mathematical areas, mean ground-truth I(·|P) rises from 1.76 for the Qwen 3.6 27B base model to 7.58 for the trained model. The trained model beats the base model in all eight areas, with per-area ratios from 2.10× in combinatorics to 8.72× in number theory, and also beats Claude Opus 4.6 prompted to generate interesting theorems in all areas.
• Novelty versus memorization: An LLM-as-a-Judge (Claude Opus 4.6), blinded to which model produced a statement, rates containment on a five-level rubric. Only 30.6% of the trained model's statements are substantially or fully contained in mathlib (scores 4–5), against 91.9% for the base model and 92.5% for Claude.
• Interestingness pruning wins the discovery loop: In a six-round iterative procedure from premises P₀ in graph theory, promoting the ten highest-interestingness verified statements per round yields the highest running mean of promoted-statement interestingness, the highest LLM-judge quality and diversity ratings (1–5 scale), and the largest share of four-way "most interesting" rankings. Pruning by longest raw proof performs worse, indicating the gain comes from the proof-to-statement ratio rather than from favoring long proofs.

Methodology in Plain English

The authors use mathlib as ground truth. They extract 113,547 declarations, keeping each theorem's type, its proof source and line count, and the premises its proof cites. Because mathlib is written in a very atomized style — the median proof is only 3 lines and the median premise is used only once — naïvely training on the dependency graph would produce a useless label. They therefore introduce premise expansion: a cited lemma L is removed from the visible premise set and replaced by L's own premises, while L's proof line count is added to the target's label. Iterating this walks the visible frontier backward through the dependency DAG and yields a richer dataset of (theorem, premises, proof length) triplets, around 100k data points in total.

They then fine-tune Qwen3.6-27B with GRPO for 350 steps, using a reward composed of three terms: a truth term matching the log of the predicted value to the log of the observed cost, a Bellman term enforcing that the cost of a target equals the cost of an intermediate lemma plus the cost of the target given that lemma, and a one-sided "drop" penalty enforcing that removing premises can never make a proof cheaper.

For interestingness, they take the predicted proof cost and divide it by the number of characters needed to state the theorem plus any definitions it needs that the surrounding premises do not already provide (times 100 for scaling). To train a conjecturer, they sample 10,000 premise sets from the mathlib training split — each with at least 16 premises and a median of 77 — freeze the difficulty estimator, and reward proposed statements by 0.25 + log(1 + Iθ(T|P)/100), with parse failures getting −0.5, Lean-invalid or premise-irrelevant statements getting −0.25, and statements provable by simple automation tactics such as assumption, rfl, simp, tauto, and simp_all getting zero. This runs for 75 GRPO steps.

Evaluation samples 20 proven statements per model per area across eight areas, giving 160 statements per model; proofs are obtained from a Claude Code with Opus 4.6 proving agent, which also allows computing ground-truth proof length and therefore ground-truth interestingness. For the iterative discovery experiment, the conjecturer receives 20 premises per round (five drawn from P_{n-1} \ P_{n-2}, the rest from P_{n-1}), generates 400 candidate statements, passes them through a Claude 4.6-based semantic filter for equivalence and diversity, proves the survivors in Lean, and promotes the ten with the highest ground-truth interestingness to form the next premise set. Four promotion rules are compared over six rounds, and the judge is never told which rule produced a given cohort.

Why This Matters

The paper addresses a gap that scaling theorem provers does not close: a prover that can verify anything still needs a reason to pursue one statement over another. By grounding "interestingness" in measurable structure — verified proof length divided by statement description length — the authors turn the selection problem into an optimizable objective, and show that a model trained on it produces statements that are both harder to prove and less contained in the existing library.

Real-world applications:

• Automated research assistants for mathematics that propose candidate lemmas rather than only filling in proofs of human-posed goals.
• Library curation and maintenance — the utility metric U₀ quantifies how much a result compresses downstream proofs, which could inform which lemmas to keep, promote, or refactor in large formalizations.
• Curriculum and data generation for formal mathematics, using interestingness ranking to prioritize which machine-generated statements are worth formalizing and proving.
• Benchmark construction, since the containment rubric distinguishes genuinely out-of-distribution statements from restatements of existing library content.

Industry relevance: the work sits at the intersection of reinforcement learning from verifiable rewards and formal verification. Proof assistants like Lean 4 give a machine-checkable reward signal, making this a clean testbed for reward design principles — reward hacking avoidance (hence the explicit triviality and relevance penalties), value-function estimation under a dependency graph, and inference-time search — that transfer to other domains where outputs can be automatically verified, such as code synthesis and hardware verification.

Future Directions

• Definitions, not just theorems. The authors explicitly state that creating new and useful definitions is outside the scope of this paper but is a natural extension of the discovery loop.
• Online difficulty estimation. A system could update its proof-length predictions as the premise set P₀ expands, using ground-truth outputs from the proving agent rather than relying on a frozen estimator.
• Alternative complexity measures. Proof length in lines of code can be a stylistic artifact, since automation tactics such as aesop and grind trade proof length for runtime. The authors suggest Levin complexity as a potentially richer signal.
• Long-run diversity and de-duplication. The results show a self-expanding library can maintain quality and diversity, but it remains unclear whether the new theorems are useful for proving future results, and the mechanisms needed for diversity and de-duplication in long-running discovery systems are left open.
• Richer notions of connectivity. The utility definition captures only a weak form of a theorem's value in connecting previously unrelated objects or unifying disjoint subfields; quantifying that more precisely is flagged as future work.

Target Audience

Researchers working on LLM-driven mathematical reasoning, reinforcement learning from verifiable rewards, and autoformalization; formal-methods practitioners interested in Lean 4 and mathlib tooling; and anyone studying intrinsic motivation or reward design for open-ended generation, for whom the paper's treatment of triviality, relevance, and originality penalties is directly instructive. Readers without background in LLM post-training or formal proof assistants will find the metric definitions accessible but the experimental setup demanding.

Authors’ abstract

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.