学习发现有趣的数学

# Learning to Discover Interesting Mathematics
Source: [https://arxiv.org/html/2609.28603](https://arxiv.org/html/2609.28603)
Ahmad RammalAffiliation:FAIR @ MetaAffiliation:CERMICS, ENPC, Institut Polytechnique de ParisAmaury HayatAffiliation:CERMICS, ENPC, Institut Polytechnique de ParisRemi MunosAffiliation:FAIR @ MetaJulia KempeAffiliation:FAIR @ MetaAffiliation:New York University

###### 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 withmathlibfrom91\.9%91\.9\\%to30\.6%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\.

††date:September 23, 2026††correspondence:Correspondence to Niket Patel,nnp5656@nyu\.edu\.## 1Introduction

Since the earliest work on the subject, mathematical reasoning has been a cornerstone of research in Artificial Intelligence \(AI\)\([Turing, 1939](https://arxiv.org/html/2609.28603#bib.bib3);[Newell and Simon, 1956](https://arxiv.org/html/2609.28603#bib.bib4)\)\. Recent work on applications of Large Language Models \(LLMs\) to solving mathematical conjectures has shown striking success, and we now have seen many instances of LLMs solving problems that have eluded human mathematicians\([Novikov et al\., 2025](https://arxiv.org/html/2609.28603#bib.bib8);[Sothanaphan, 2026](https://arxiv.org/html/2609.28603#bib.bib9);[Alexeev et al\., 2026a](https://arxiv.org/html/2609.28603#bib.bib10);[Alexeev et al\., 2026b](https://arxiv.org/html/2609.28603#bib.bib11);[Alon et al\., 2026](https://arxiv.org/html/2609.28603#bib.bib12);[Chen and Jiang, 2026](https://arxiv.org/html/2609.28603#bib.bib13);[Oum, 2026](https://arxiv.org/html/2609.28603#bib.bib14);[Huang, 2026](https://arxiv.org/html/2609.28603#bib.bib15);[OpenAI, 2026a](https://arxiv.org/html/2609.28603#bib.bib55)\)\. Though LLM\-based theorem provers can often make errors, they are particularly strong and reliable when their outputs are verified by a proof assistant such as Lean 4\([de Moura and Ullrich, 2021](https://arxiv.org/html/2609.28603#bib.bib17);[The mathlib Community, 2020](https://arxiv.org/html/2609.28603#bib.bib18);[Yang et al\., 2023](https://arxiv.org/html/2609.28603#bib.bib19);[Xin et al\., 2024](https://arxiv.org/html/2609.28603#bib.bib24);[AlphaProof and AlphaGeometry teams, 2024](https://arxiv.org/html/2609.28603#bib.bib23);[Ren et al\., 2025](https://arxiv.org/html/2609.28603#bib.bib25)\)\. However, a common critique of applications of LLMs to solving mathematical conjectures is that they often only appear to solve problems that lie within the “convex hull” of existing mathematics\.

Our long\-term goal is to build systems capable of*autonomous mathematical discovery*\. Such a system should be able to engage in*open\-ended*reasoning\. Starting from a set of initial premises, the system should be able to formulate new questions, decide which are worth pursuing, construct and verify their proofs, and build on this knowledge\([Barkeshli et al\., 2026](https://arxiv.org/html/2609.28603#bib.bib45)\)\. A fundamental challenge to achieving such a system is the question of interestingness of the mathematical statement\. The version of mathematics that was created by human intuition over thousands of years has proven to be an “unreasonably effective” tool to approaching real world problems\([Wigner, 1960](https://arxiv.org/html/2609.28603#bib.bib5)\)\. In contrast, arbitrarily adding trivial statements, or even nontrivial but*uninteresting*statements, is unlikely to lead to the same success that mathematics has achieved in the past\.

> *“Science is built up with facts, as a house is with stones\. But a collection of facts is no more a science than a heap of stones is a house\.”*–*Science and Hypothesis,*[Poincaré \(1905\)](https://arxiv.org/html/2609.28603#bib.bib7)

We can reason by analogy with Borges’s “Library of Babel”\([Borges, 1962](https://arxiv.org/html/2609.28603#bib.bib6);[Litt, 2026](https://arxiv.org/html/2609.28603#bib.bib52)\)\. Borges’s library holds every book that can be written, and therefore holds every truth in it; it is nonetheless useless, since no reader could find meaning within its nearly infinite shelves\. The space of all true mathematical statements has the same character, whereas mathematics, as it has been created by humans, does not\. Extrapolating outside the “convex hull” of mathematics, therefore, requires both the ability to navigate the space of possible deductions and a notion of value that distinguishes a discovery from a merely valid statement\.

We seek a system that can begin with the mathematics that is already known, and recursively produce new mathematical results\. Any such autonomous system needs a quantitative object to optimize\. Prior work has often focused on “Intrinsic Motivation”\([Poesia et al\., 2024](https://arxiv.org/html/2609.28603#bib.bib41);[Tsoukalas et al\., 2025](https://arxiv.org/html/2609.28603#bib.bib42)\)\. We take a different view, one in which there are inherent aspects of mathematics that can quantify the quality of a mathematical statement, itsinterestingness\. Prior work has found that LLMs do not robustly capture the same notions of interestingness, and the same diversity in those notions, as humans do\([Mishra et al\., 2025](https://arxiv.org/html/2609.28603#bib.bib16)\)\. In the present work, we consider two complementary sources of value\. On one hand, a theorem may be*intrinsically interesting*, if it is easy to state but very difficult to prove\. Alternatively, a theorem could be*useful*because of its relation to the surrounding body of mathematics\. A useful theorem is a reusable abstraction that \- once added to a body of mathematics \- compresses later proofs by making them easier to derive\.

A fundamental primitive required to understand or estimate either of the above quantities is the difficulty to prove a theoremTT, conditioned on a set of premisesPPwhich are already available, which we will termV⁡\(T\|P\)V\(T\|P\)\. Proof assistants\([de Moura and Ullrich, 2021](https://arxiv.org/html/2609.28603#bib.bib17)\)allow a way to quantify the difficulty of a proof, in terms of the number of lines of code required to formally prove it\. Lean 4’s librarymathlibprovides a large dependency graph of machine\-checked definitions, theorems, and proofs\([The mathlib Community, 2020](https://arxiv.org/html/2609.28603#bib.bib18)\), which we can utilize to learn to model the conditional proof difficultyV⁡\(T∣P\)V\(T\\mid P\), mathematical interestingness and utility, and autonomous mathematical discovery\. We make the following primary contributions\.

##### Contributions\.

1. 1\.We formalize proof difficulty as the computational cost of deriving a target theorem from a given mathematical context in Lean 4\. We post\-train a 27B parameter LLM to predict the difficulty of a proof given a set of premises, and show that this predictor outperforms frontier LLMs\.
2. 2\.We motivate and define a notion of a theorem’s*interestingness*as the ratio between the length of the proof and the length of the statement of the theorem\. We also define a notion of*utility*based on the amount a theorem is able to compress a set of theorems and their proofs, and show that utility strongly correlates with interestingness\.
3. 3\.With our notion of*interestingness*, we are able to show that we can post\-train a language model to produce more interesting theorems, and we find that this quadruples the mean interestingness, as measured by the length of the real proof divided by the length of the statement\. This training procedure also reduces the fraction of generated statements judged substantially or fully contained inmathlibfrom91\.9%91\.9\\%to30\.6%30\.6\\%, showcasing the creation of more out\-of\-distribution math\.
4. 4\.We showcase our method in a specific setting where we apply our interestingness metric as an inference\-time pruning algorithm to perform recursive mathematical discovery, and find nontrivial statements that are not present inmathlib\.

## 2Modeling the Conditional Proof Difficulty

We ultimately want to train a model that can predict the difficulty of a proof without needing to write the proof beforehand\. We model this difficulty as a function of both the target theorem and the premises available in the local context\. We define the estimator of the difficulty of proving a theoremTTgiven premisesPPas the valueV⁡\(T∣P\)V\(T\\mid P\)\. Such a premise\-conditioned value function should satisfy certain properties\. For any codebase𝒟\\mathcal\{D\}of theorems and proofs stated in a formal language like Lean 4, we will denote byC𝒟​\(T\|P\)C\_\{\\mathcal\{D\}\}\(T\|P\)the ground truth number of lines of code in the codebase to prove theoremTTgiven premisesPP\. For any such codebase, this quantity is not necessarily defined for all choices ofT,PT,P, as some theorems may have multiple proofs, so we will defineVVas satisfying the following conditions:

###### Definition 1\(Conditional\-value axioms\)\.

A conditional proof computational\-costVVis*faithful*on𝒟\\mathcal\{D\}if for all targetsT∈𝒟T\\in\\mathcal\{D\}, lemmasL∈𝒟L\\in\\mathcal\{D\}, and premise setsP,Q⊂𝒟P,Q\\subset\\mathcal\{D\}, such thatP⊆QP\\subseteq Q, the property \(A1\) below holds wheneverC𝒟C\_\{\\mathcal\{D\}\}is well defined and \(A2\)–\(A3\) always hold:

\(A1\) grounding:V⁡\(T∣P\)=C𝒟​\(T∣P\),\\displaystyle V\(T\\mid P\)=C\_\{\\mathcal\{D\}\}\(T\\mid P\),\(1\)\(A2\) premise monotonicity:V⁡\(T∣Q\)≤V⁡\(T∣P\),\\displaystyle V\(T\\mid Q\)\\;\\leq\\;V\(T\\mid P\),\(2\)\(A3\) composition:V⁡\(T∣P\)≤V⁡\(L∣P\)\+V⁡\(T∣P∪\{L\}\)\.\\displaystyle V\(T\\mid P\)\\;\\leq\\;V\(L\\mid P\)\+V\(T\\mid P\\cup\\\{L\\\}\)\.\(3\)

Axioms \(A2\)–\(A3\) hold for the ideal shortest proof\. We would expect to see equality in \(A3\) if a lemmaLLis required as an intermediate step towards proving the theorem from the premises, giving us the following Bellman\-type relation:

V⁡\(T∣P\)=V⁡\(L∣P\)\+V⁡\(T∣P∪\{L\}\)\.V\(T\\mid P\)=V\(L\\mid P\)\+V\(T\\mid P\\cup\\\{L\\\}\)\.\(4\)We will use these properties to inform the training objective in the following sections\.

### 2\.1Generating a Dataset

We usemathlib\([de Moura and Ullrich, 2021](https://arxiv.org/html/2609.28603#bib.bib17);[The mathlib Community, 2020](https://arxiv.org/html/2609.28603#bib.bib18)\)as a ground truth library from which we generate our training data\. For each theorem we extract its rendered type, the local definitions required to state it, the proof source, and the premises required for the proof\. If we were to naïvely train on the dependency graph ofmathlibwe would not get a useful predictor, as the library is built in a very atomized way\. But we still need to assign a label to each theoremTT\. For instance, the median proof length inmathlibis33lines of code, and the median number of times any particular premise is used is11\. To remedy this, we employ a technique we callpremise expansion\. We call a statementLLa premise ofTTif it is*directly*used in the proof ofTT, and we will writePPorP⁡\(T\)P\(T\)to denote the set of premises ofTT\. In this case, one*expansion step*will removeLLfrom the set of premises ofTT, and add ,P⁡\(L\)P\(L\), the premises ofLLto the premises ofTT\. So the new set of premises ofTTisP⁡\(T\)∪P⁡\(L\)\\LP\(T\)\\cup P\(L\)\\backslash L\. We then add the number of lines of code in the proof ofLLto the label ofTT\. Iterating moves the visible frontier backward through the dependency Directed Acyclic Graph \(DAG\)\(Appendix[B\.1](https://arxiv.org/html/2609.28603#A2.SS1)\), creating a richer dataset of theorem, premises, proof triplets\. We end up with around 100k data points which we use in the next section\. We evaluate on a withheld evaluation set coming from the same construction\.

Figure 1:The trained value is substantially better calibrated on held\-out samples frommathlib\.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ρ\\rhoon all 4,615 validation prompts\.
### 2\.2Modeling the Conditional Proof Length

We want to train a modelVθV\_\{\\theta\}that can predict the difficulty of proving a theoremTTconditioned on a set of premisesPP\. We fine\-tune Qwen3\.6\-27B\([Qwen Team, 2026](https://arxiv.org/html/2609.28603#bib.bib49)\)with group relative policy optimization \(GRPO\)\([Shao et al\., 2024](https://arxiv.org/html/2609.28603#bib.bib28);[Miles Team, 2026](https://arxiv.org/html/2609.28603#bib.bib54)\)on the dataset from Section[2\.1](https://arxiv.org/html/2609.28603#S2.SS1)for 350 steps\. Full definitions and specific details on the training setup are relegated to Appendix[B\.2](https://arxiv.org/html/2609.28603#A2.SS2)\. We create a reward that is designed to satisfy the desiderata in Definition[1](https://arxiv.org/html/2609.28603#Thmlemma1)\. We designℒtruth\\mathcal\{L\}\_\{\\rm truth\}to satisfy \([1](https://arxiv.org/html/2609.28603#S2.E1)\)\. IfLLis a lemma used to go fromPPtoTT, in order to satisfy \([4](https://arxiv.org/html/2609.28603#S2.E4)\), we introduceℒBellman\\mathcal\{L\}\_\{\\rm Bellman\}\. To satisfy \([2](https://arxiv.org/html/2609.28603#S2.E2)\), we addℒdrop\\mathcal\{L\}\_\{\\rm drop\}, whereQ⊊PQ\\subsetneq P\. Our final reward is,

ℛ=\\displaystyle\\mathcal\{R\}=−\|log⁡Vθ​\(T\|P\)−log⁡C𝒟​\(T\|P\)\|\\displaystyle\-\|\\log V\_\{\\theta\}\(T\|P\)\-\\log C\_\{\\mathcal\{D\}\}\(T\|P\)\|\(ℒtruth\)\\displaystyle\(\\mathcal\{L\}\_\{\\rm truth\}\)−\|log⁡Vθ​\(T\|P\)−log⁡\(Vθ​\(L\|P\)\+Vθ​\(T\|P∪\{L\}\)\)\|\\displaystyle\-\|\\log V\_\{\\theta\}\(T\|P\)\-\\log\(V\_\{\\theta\}\(L\|P\)\+V\_\{\\theta\}\(T\|P\\cup\\\{L\\\}\)\)\|\(ℒBellman\)\\displaystyle\(\\mathcal\{L\}\_\{\\rm Bellman\}\)−max⁡\{0,log⁡V⁡\(T\|P\)−log⁡V⁡\(T\|P\\Q\)\}\\displaystyle\-\\max\\\{0,\\log V\(T\|P\)\-\\log V\(T\|P\\backslash Q\)\\\}\(ℒdrop\)\\displaystyle\(\\mathcal\{L\}\_\{\\rm drop\}\)
We evaluate models on a held\-out validation set of 4,615 labeled validation prompts\. All models receive identical definitions, premises, target, and output instruction\. We report mean absolute error \(MAE\) and Spearman rank correlation, computing both only over parsed non\-negative answers \(Appendix[B\.3](https://arxiv.org/html/2609.28603#A2.SS3)\)\. Figure[1](https://arxiv.org/html/2609.28603#S2.F1)showcases performance of our trained model over GPT\-5\.5\([OpenAI, 2026b](https://arxiv.org/html/2609.28603#bib.bib50)\)and Claude Opus 4\.6\([Anthropic, 2026](https://arxiv.org/html/2609.28603#bib.bib51)\)\. We find that while all three models tend to underestimate the difficulty of proofs, ours is substantially more accurate and better calibrated than the others\.

## 3Interestingness\-Driven Mathematical Discovery

A human mathematician may find a mathematical conjecture valuable for many reasons\. They could be interested in a statement because of historical or social factors, like for instance that several famous mathematicians before them tried and failed to find a proof of a statement\. They could also study statements that are related to the physical world\. These are factors which are extrinsic to the field of math, and rely on its relation to the world outside it\. As such, these factors are not something that we could model in search of a quantitative definition of the interestingness of a statement; they lie outside the scope of our present objective\.

We instead focus on structural properties that can be measured directly in a formal mathematical library\. In particular, statements that are simple to express but difficult to prove often align with human intuitions about mathematical interestingness\. Motivated by this observation, we define an intrinsic notion of interestingness that combines statement length with conditional proof difficulty\. This quantity is not intended to capture every source of mathematical value, but to provide a concrete objective for guiding mathematical discovery\. We separately consider a theorem’s utility, which measures its value to subsequent mathematical developments\.

In Section[3\.1](https://arxiv.org/html/2609.28603#S3.SS1)we define and study the*interestingness*of a mathematical statement\. In Section[3\.2](https://arxiv.org/html/2609.28603#S3.SS2)we examine the*utility*of a mathematical statement and show its relation to the interestingness\. We then show in Section[3\.3](https://arxiv.org/html/2609.28603#S3.SS3)that interestingness is a concrete metric that can be optimized, via training and at inference\-time\.

### 3\.1The Intrinsic Interestingness of a Mathematical Statement

In this section, we attempt to define a notion of the interestingness of a mathematical statement or conjecture that aims to capture an*intrinsic*property of the mathematical result, ignoring any relation to the outside world, or to other parts of the mathematical literature\. We claim that a statementTTis*interesting*given a set of premisesPPif it is easy to state, and has a long and incompressible proof\. To compute this, we can take a ratio between the length of a proof given some premises in terms of lines of code, and the number of characters of Lean 4 needed to state a theorem given some set of definitions one already has access to\. For instance, one would expect that a theorem in probability theory is easy to state for a reader who already has a measure\-theoretic vocabulary and enormously difficult for a reader given access to only statements in algebraic geometry\. We recall the following quote by Pólya on the nature of aesthetics in math,

> *“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\.”*–*Mathematical Discovery,*[Pólya \(1981\)](https://arxiv.org/html/2609.28603#bib.bib2)

Formally, for any Lean declarationXX, letS⁡\(X\)S\(X\)denote the number of characters in its statement, and letC⁡\(X\)C\(X\)be the set of all definitions required to stateXX, including whatever definitions are needed to state those definitions, recursively\. SoC⁡\(X\)C\(X\)will contain all the definitions required to formally stateXXfrom the axioms\. We will then define the conditional description length as

L⁡\(T∣P\)=S⁡\(T\)\+∑d∈C⁡\(T\)∖C⁡\(P\)S⁡\(d\)\.L\(T\\mid P\)\\;=\\;S\(T\)\+\\\!\\\!\\sum\_\{d\\in C\(T\)\\setminus C\(P\)\}\\\!\\\!S\(d\)\.\(5\)
In this way, the termL⁡\(T\|P\)L\(T\|P\)counts the description length of all the definitions needed to state the theoremTT, given access to all the definitions used in the premisesPP\. We then formally define the conditional interestingness111We use a factor of 100 in the definition here so that the Interestingness has a mean 1̃, as in Figure[2](https://arxiv.org/html/2609.28603#S3.F2)and Figure[4](https://arxiv.org/html/2609.28603#S3.F4)\.of a statement as

I⁡\(T∣P\)=100​V⁡\(T∣P\)L⁡\(T∣P\)\.I\(T\\mid P\)\\;=\\;100\\;\\frac\{V\(T\\mid P\)\}\{L\(T\\mid P\)\}\.\(6\)
We choose this definition to quantify the intrinsic difficulty of a mathematical statement as it is trivially possible to construct arbitrarily difficult statements, if we do not normalize by the description length of the statement\. For instance, suppose we had a fixed set of premisesPPand a set of theorems\{T1,T2,…\}\\\{T\_\{1\},T\_\{2\},\\ldots\\\}that are all entirely unrelated and have a fixed proof length\. Then the “theorem”T^n=T1∧T2∧⋯∧Tn\\hat\{T\}\_\{n\}=T\_\{1\}\\wedge T\_\{2\}\\wedge\\cdots\\wedge T\_\{n\}would have difficultyV⁡\(T^n\|P\)=O⁡\(n\)V\(\\hat\{T\}\_\{n\}\|P\)=O\(n\), whereas the interestingness isI⁡\(T^n\|P\)=O⁡\(1\)I\(\\hat\{T\}\_\{n\}\|P\)=O\(1\)\.

In the special case where we consider the empty set of premises, we can create an absolute scale of the interestingness of a mathematical statementI0​\(T\)=I⁡\(T\|∅\)I\_\{0\}\(T\)=I\(T\|\\varnothing\)222This corresponds to the notion of “interest” from[Aksenov et al\. \(2026\)](https://arxiv.org/html/2609.28603#bib.bib46)\.\. With no premises, the denominator is the target’s own vocabulary length,L⁡\(T∣∅\)=S⁡\(T\)\+∑d∈C⁡\(T\)S⁡\(d\)L\(T\\mid\\varnothing\)=S\(T\)\+\\sum\_\{d\\in C\(T\)\}S\(d\)\. As we no longer require conditioning on a set of premises, the numerator can now be deterministically computed from a library such asmathlib, as we can just unroll the proof as written via premise expansion\. The result \(Figure[2](https://arxiv.org/html/2609.28603#S3.F2)\) serves as a useful verification for the construction of our metric on existing statements ofmathlib\. We can see in the bottom decile simple algebraic relations, like for instance the identity that1n=11^\{n\}=1, and in the upper quartiles we see results such as special cases of Fermat’s Last Theorem, which happen to require very little machinery to state but are tough to prove\.

Figure 2:Quantifying the interestingness of a statement\.Here we show the distribution of interestingnessI0I\_\{0\}, as defined in Section[3\.1](https://arxiv.org/html/2609.28603#S3.SS1), of all statements frommathlib\. 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\.
### 3\.2Intrinsic Interestingness Correlates with Extrinsic Utility

![Refer to caption](https://arxiv.org/html/2609.28603v1/u0_utility_vs_i0_interestingness.png)Figure 3:Utility and interestingness are correlated\.Each point is amathlibtheorem\. UtilityU0U\_\{0\}, defined in Section[3\.2](https://arxiv.org/html/2609.28603#S3.SS2), is the number of lines of code saved across the library when the theorem is admitted as a premise, while interestingnessI0I\_\{0\}, defined in Section[3\.1](https://arxiv.org/html/2609.28603#S3.SS1), is the ratio between a theorem’s proof length and description length\. Excluding the declarations withU0=0U\_\{0\}=0gives a Spearmanρ=0\.756\\rho=0\.756\.We will define the*utility*of a theorem to answer the following question: If we had access to this statement for free, how much would it compress the rest of the mathematical library? Concretely, we compare two libraries: one in whichTTis available as a premise, and one in which it is not, so that every statement relying onTTmust re\-derive it from scratch\. The utility ofTTis the number of lines of code saved by the first library relative to the second\. If we letD⁡\(T\)D\(T\)be the set of theorems and lemmas that cite / useTTdirectly, then\|D⁡\(T\)\|\\lvert D\(T\)\\rvertwould be the number of direct users of a theorem\. So we can define

U0​\(T\)=\|D⁡\(T\)\|⋅V⁡\(T\|∅\)\.U\_\{0\}\(T\)=\\lvert D\(T\)\\rvert\\,\\cdot V\(T\|\\varnothing\)\.\(7\)
DespiteU0U\_\{0\}being an*extrinsic*measure, depending on a theorem’s relation to the broader mathematical theory surrounding it, andI0I\_\{0\}being an*intrinsic*measure depending only on a theorem and its proof, we find that they are strongly correlated\. In Figure[3](https://arxiv.org/html/2609.28603#S3.F3), we see a strong positive correlation betweenU0U\_\{0\}andI0I\_\{0\}onmathlib, giving a Spearman correlation of0\.7560\.756if we disregard statements with no downstream users\. While some statements have high interestingness but low utility, few statements, if any, have high graph utility without high interestingness\. Interestingness is therefore a practical surrogate for the quality of a mathematical statement as it can be computed or estimated at proposal time, whereas utility is observable only after placing a theorem in a body of work and seeing its descendants\. We recall the following quote of Thurston\.

> *“Our aesthetic instincts draw us to mathematics of a certain depth and connectivity\. The very depth and beauty of the patterns makes them likely to be manifested, in unexpected ways, in other parts of mathematics, science, and the world\.”*–*Mathematical Education,*[Thurston \(2005\)](https://arxiv.org/html/2609.28603#bib.bib1)

### 3\.3Optimizing for Interestingness

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 inlog10\\log\_\{10\}\-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 existingmathlibcontent\.For each model we take the 160 statements from Figure[4](https://arxiv.org/html/2609.28603#S3.F4), and judge to what degree each statement is contained withinmathlib\. Appendix[C\.2\.2](https://arxiv.org/html/2609.28603#A3.SS2.SSS2)gives the rubric, prompt, and protocol\.The preceding construction turns the task of creating new, interesting, mathematics into an optimizable objective\. Given a mathematical context of prior lemmas and premisesPP, a conjecturing model, or*conjecturer*, should be able to propose a statementTTwhich is cheap to express in the vocabulary ofPPbut requires a difficult proof\. With the use of our estimatorVθV\_\{\\theta\}we trained in Section[2](https://arxiv.org/html/2609.28603#S2), we can obtain an estimate of the conditional interestingness, which we can use as a reward signal to train a model to produce more interesting conjectures\. From themathlibtraining split we randomly select10,00010\{,\}000sets of premises\. Each setPPcontains at least 16 premises, with the median containing7777\. Appendix[C\.1](https://arxiv.org/html/2609.28603#A3.SS1)details the sampling procedure\. The model is conditioned on the available premises and definitions and emits a standalone Lean proposition\. For a valid and nontrivial proposal, the training reward is,

R⁡\(T,P\)=0\.25\+log⁡\(1\+Vθ​\(T∣P\)L⁡\(T∣P\)\)=0\.25\+log⁡\(1\+Iθ​\(T∣P\)100\)\.R\(T,P\)=0\.25\+\\log\\\!\\left\(1\+\\frac\{V\_\{\\theta\}\(T\\mid P\)\}\{L\(T\\mid P\)\}\\right\)=0\.25\+\\log\\\!\\left\(1\+\\frac\{I\_\{\\theta\}\(T\\mid P\)\}\{100\}\\right\)\.\(8\)HereVθV\_\{\\theta\}is a frozen proof line count predictor andLLis the conditional description length from Equation[5](https://arxiv.org/html/2609.28603#S3.E5)\. The logarithm controls the influence of outliers while preserving the ordering induced by interestingness\. Parse failures receive reward−0\.5\-0\.5, Lean\-invalid or statements that don’t relate to the premises at all receive−0\.25\-0\.25, and statements which are able to be proven with simple proof automation tactics333For instance,assumption,rfl,simp,tauto, andsimp\_all\.receive zero\. The constant term0\.250\.25appears in the reward to provide a baseline reward for valid, relevant, and non\-trivial statements\. Appendix[C\.1](https://arxiv.org/html/2609.28603#A3.SS1)describes elaboration, relevance, and triviality checks in full\.

We evaluate Qwen3\.6\-27B\([Qwen Team, 2026](https://arxiv.org/html/2609.28603#bib.bib49)\), trained with7575GRPO steps with the reward from \([8](https://arxiv.org/html/2609.28603#S3.E8)\), against the corresponding base model and Claude 4\.6 on a held\-out validation set from eight coarse mathematical areas inmathlib\. For each conjecturer and area, we repeatedly sample premises and generate candidate theorem statements, then ask a Claude Code with Opus 4\.6 proving agent for an exact proof or a tightly constrained marginal repair\. Having a proof of each of these statements allows us to verify that they are correct, and to compute the ground\-truth proof length, allowing us to get a ground\-truth estimate of the interestingness\. We retain2020proven statements per model and area, across 8 areas of mathematics, resulting in160160total statements per model\. We showcase the ground\-truth interestingness scores in Figure[4](https://arxiv.org/html/2609.28603#S3.F4); full details are available in Appendix[C\.2](https://arxiv.org/html/2609.28603#A3.SS2)\.

We find that training produces a large shift in ground\-truth verified interestingness \(Figure[4](https://arxiv.org/html/2609.28603#S3.F4)\)\. Pooled across areas, meanI\(⋅∣P\)I\(\\cdot\\mid P\)rises from1\.761\.76for the Qwen 3\.6 27B base model, to7\.587\.58for our trained model\. The trained model’s mean is higher than the base model’s in all eight areas, with area\-level ratios ranging from2\.10×2\.10\\timesin combinatorics to8\.72×8\.72\\timesin number theory\. The trained model similarly beats Claude Opus 4\.6 \(prompted to generate interesting theorems\) in all areas\.

The shift is also not explained merely by reproducing existingmathlibdeclarations \(Figure[5](https://arxiv.org/html/2609.28603#S3.F5)\)\. With the conjecturer and subject area hidden, an LLM\-as\-a\-Judge \(in this case Claude Opus 4\.6\) rates each verified statement on the five\-level containment rubric described in the caption\. Only30\.6%30\.6\\%of statements from the trained model are substantially or fully contained \(scores 4–5\), compared with91\.9%91\.9\\%for Base and92\.5%92\.5\\%for Claude\. Together, Figures[4](https://arxiv.org/html/2609.28603#S3.F4)and[5](https://arxiv.org/html/2609.28603#S3.F5)show that optimizing conditional interestingness moves the conjecturer toward statements with longer verified proofs relative to their descriptions and substantially less overlap with the existing library\.

### 3\.4Inference\-Time Optimization for Theory Creation

![Refer to caption](https://arxiv.org/html/2609.28603v1/forward_dependency_graph.png)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](https://arxiv.org/html/2609.28603#S3.SS4)\. Green shade encodeslog10\\log\_\{10\}total interestingness relative toP0P\_\{0\}on a per\-figure scale\. The red lines trace the ancestry of the most interesting theorem introduced inP6P\_\{6\}\. More such graphs can be found in Figure[12](https://arxiv.org/html/2609.28603#A5.F12)in Appendix[C\.2](https://arxiv.org/html/2609.28603#A3.SS2)\.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](https://arxiv.org/html/2609.28603#A4.T4)\) and the share of four\-way comparisons in which each rule’s statement is ranked most interesting \(Table[3](https://arxiv.org/html/2609.28603#A4.T3)\)\. Right: running mean of the verified interestingness of each setPnP\_\{n\}throughP6P\_\{6\}\. More experiments are available in Appendix[D](https://arxiv.org/html/2609.28603#A4)\.In the previous section, we showed that we can successfully train a conjecturer to generate more interesting individual conjectures\. But our ultimate goal is not just to generate individual interesting theorems, but to iteratively build a body of interesting theorems, where one round’s discoveries become the premises for the next round\. We showcase here how we can use our metric of interestingness to achieve this at inference\-time, without updating the weights of the model\. We evaluate an iterative theorem\-discovery procedure, and we showcase that optimizing for interestingness gives us the strongest results across several metrics\. We want to have a system that starts from a set of premisesP0P\_\{0\}, and then adds verified theorems to create an iterated increasing set of premisesP0⊂P1⊂⋯⊂PNP\_\{0\}\\subset P\_\{1\}\\subset\\cdots\\subset P\_\{N\}\. At each iterationnn, the conjecturer, here Claude 4\.6, receives 20 premises, five of which are sampled fromPn−1\\Pn−2P\_\{n\-1\}\\backslash P\_\{n\-2\}, and the rest fromPn−1P\_\{n\-1\}\. It generates 400 candidate statements\. A Claude 4\.6 based semantic filter removes equivalent conjectures and enforces diversity across theorem families\. The surviving statements are then proved independently with Claude Code in Lean\. Successfully verified statements are ranked by the interestingness as computed from the ground\-truth proof, and the ten highest scoring results are “promoted” and added to the next set of premisesPiP\_\{i\}\. Appendix[D](https://arxiv.org/html/2609.28603#A4)compares this rule against retaining every verified statement, promoting ten statements uniformly at random, and promoting the ten statements with the longest verified proofs; interestingness pruning yields the highest running mean of promoted\-statement interestingness and the highest quality, diversity, and “most interesting” judgments \(Figure[7](https://arxiv.org/html/2609.28603#S3.F7)\)\. We use the verified proof length here rather thanVθV\_\{\\theta\}because every candidate has already been proved at this stage, so the exact value ofVVis available; the learned estimator is needed only where proving every candidate is too time\-consuming, as in the reinforcement\-learning setting of Section[3\.3](https://arxiv.org/html/2609.28603#S3.SS3)\. We showcase an experiment whereP0P\_\{0\}is a set of premises from graph theory here in Figure[6](https://arxiv.org/html/2609.28603#S3.F6); Appendix Figure[12](https://arxiv.org/html/2609.28603#A5.F12)showcases the result of picking premises from Algebra, Measure / Probability Theory, and Number Theory\.

The promotion rule at the end of each round is the only place where interestingness enters the loop, so we isolate its effect by holding the conjecturer, the semantic filter, and the proving agent fixed and varying only how the verified statements are pruned\. We compare four rules: retaining every verified statement, promoting ten uniformly at random, promoting the ten statements with the longest verified proofs, and promoting the ten with the highest ground\-truth interestingness\. Each rule is run for 6 rounds from the sameP0P\_\{0\}, drawing on premises from graph theory, and we evaluate the resulting trajectories in two ways\. We aim to quantify the quality and diversity of the samples from each of the runs, which we are able to do by using an LLM\-as\-a\-judge\. The judge \(Claude 4\.6\) is never told which promotion rule produced the statements it evaluates\. First, for each rule and round, it rates the cohort of ten promoted statements for quality and diversity on a 1–5 scale \(Table[4](https://arxiv.org/html/2609.28603#A4.T4)\)\. Second, it is shown four statements at a time, one from each rule, and ranks them by how mathematically interesting they are \(Table[3](https://arxiv.org/html/2609.28603#A4.T3)\)\. We also track the running mean of the verified interestingness of the setsPnP\_\{n\}, and we find that interestingness pruning is the strongest promotion rule on each of these metrics, as displayed in Figure[7](https://arxiv.org/html/2609.28603#S3.F7)\. Notably, pruning by raw proof length alone performs worse, indicating that the gain comes from the ratio defined in \([6](https://arxiv.org/html/2609.28603#S3.E6)\) rather than from simply favoring long proofs\.

## 4Discussion

Current LLM\-based mathematics systems prove or solve human\-posed problems; they do not decide which problems are worth posing\. Our work takes a step toward changing this by defining a simple notion of interestingness\. Crucially, our metric emerges from the structure of the proofs, and requires no human judgment of what constitutes interesting mathematics\. Our results show that this metric is already sufficient to steer a language model toward non\-trivial, out\-of\-distribution conjectures\. Beyond individual conjectures, our iterative discovery procedure demonstrates that a system can build on its own outputs across rounds, with each round’s most interesting theorems becoming premises for the next\. Together, these results offer a proof of concept that interesting self\-expanding mathematical libraries, grown without human intervention beyond the initial premises, are feasible\.

We identify the following limitations with our specific methodology in this paper\. Proof length in terms of lines of code can be a stylistic artifact, as automation tactics, such asaesopandgrind, often trade proof length for runtime\. Alternative notions such as the “Levin complexity” might provide a richer signal in light of this\([Li and Vitányi, 2008](https://arxiv.org/html/2609.28603#bib.bib29)\)\. Our definition also isolates some aspects of mathematical value, and one may object that much of what makes a theorem interesting is that it connects previously unrelated objects or unifies disjoint subfields\. Our definition of utility captures a weak form of this, but future work could try to quantify this notion more precisely\.

Future work should aim towards extending our notions of discovery beyond just theorem statements to also allow for the creation of new and useful definitions, something we do not consider in this paper\. Additionally, one could investigate training a model to estimate the proof difficulty in an online fashion, where as you expand your set of premisesP0P\_\{0\}, you are also updating your predictions of the proof length based on the ground truth outputs of your proving agent\. Our results showed that LLMs are capable of creating a self\-expanding mathematical library, which can have a high quality and diversity of theorems, but it is not yet clear if the new theorems are also useful for proving future results\. Future work should look into the mechanisms for diversity and de\-duplication that are required for long\-running discovery systems\.

## Acknowledgments

JK and NP thank the Simons Foundation for support through the Collaborative Grant “The Physics of Learning and Neural Computation” as well as support by the NSF through NRT Award 1922658\. AH is supported by Hi\! PARIS and ANR/France 2030 program \(ANR\-23\-IACL\-0005\)\. NP thanks Vivien Cabannes, Charles Arnal, Taco Cohen, Anirudh Goyal, Skander Moalla and Anikait Singh for helpful discussions and feedback\.

## References

- Aksenovet al\.\(2026\)V\. Aksenov, E\. Bodnia, M\. H\. Freedman, and M\. MulliganCompression is all you need: modeling mathematics\.arXiv preprint arXiv:2603\.20396\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px4.p1.1),[footnote 2](https://arxiv.org/html/2609.28603#footnote2)\.
- Alexeevet al\.\(2026a\)B\. Alexeev, M\. Putterman, M\. Sawhney, M\. Sellke, and G\. ValiantShort proofs in combinatorics and number theory\.arXiv preprint arXiv:2603\.29961\.Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Alexeevet al\.\(2026b\)B\. Alexeev, M\. Putterman, M\. Sawhney, M\. Sellke, and G\. ValiantShort proofs in combinatorics, probability and number theory II\.arXiv preprint arXiv:2604\.06609\.Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Alonet al\.\(2026\)N\. Alon, T\. F\. Bloom, W\. T\. Gowers, D\. Litt, W\. Sawin, A\. Shankar, J\. Tsimerman, V\. Wang, and M\. M\. WoodRemarks on the disproof of the unit distance conjecture\.arXiv preprint arXiv:2605\.20695\.Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- AlphaProof and AlphaGeometry teams \(2024\)AlphaProof and AlphaGeometry teamsAI achieves silver\-medal standard solving International Mathematical Olympiad problems\.Note:Google DeepMind BlogExternal Links:[Link](https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/)Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px1.p1.1),[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Anivaet al\.\(2025\)L\. Aniva, C\. Sun, B\. Miranda, C\. Barrett, and S\. KoyejoPantograph: a machine\-to\-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4\.InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems,pp\. 104–123\.Cited by:[§C\.1\.2](https://arxiv.org/html/2609.28603#A3.SS1.SSS2.p1.1)\.
- Anthropic \(2026\)AnthropicSystem Card: Claude Opus 4\.6\.System CardAnthropic\.External Links:[Link](https://www-cdn.anthropic.com/0dd865075ad3132672ee0ab40b05a53f14cf5288.pdf)Cited by:[§2\.2](https://arxiv.org/html/2609.28603#S2.SS2.p2.1)\.
- Armstrong and Kempe \(2026\)S\. Armstrong and J\. KempeFormalization of De Giorgi–Nash–Moser theory in Lean\.arXiv preprint arXiv:2604\.05984\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px2.p1.1)\.
- Azerbayevet al\.\(2023\)Z\. Azerbayev, B\. Piotrowski, H\. Schoelkopf, E\. W\. Ayers, D\. Radev, and J\. AvigadProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.arXiv preprint arXiv:2302\.12433\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px2.p1.1)\.
- Barkeshliet al\.\(2026\)M\. Barkeshli, M\. R\. Douglas, and M\. H\. FreedmanArtificial intelligence and the structure of mathematics\.arXiv preprint arXiv:2604\.06107\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px3.p1.1),[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px4.p1.1),[§1](https://arxiv.org/html/2609.28603#S1.p2.1)\.
- Bengio and Malkin \(2024\)Y\. Bengio and N\. MalkinMachine learning and information theory concepts towards an AI mathematician\.Bulletin of the American Mathematical Society61\(3\),pp\. 457–469\.External Links:[Document](https://dx.doi.org/10.1090/bull/1839)Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px3.p1.1)\.
- Blier and Ollivier \(2018\)L\. Blier and Y\. OllivierThe description length of deep learning models\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px4.p1.1)\.
- Borges \(1962\)J\. L\. BorgesThe library of babel\.InLabyrinths: Selected Stories and Other Writings,D\. A\. Yates and J\. E\. Irby \(Eds\.\),Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p4.1)\.
- Chen and Jiang \(2026\)X\. Chen and X\. JiangMoonshine: an autonomous mathematical research agent centered on conjecture generation\.arXiv preprint arXiv:2606\.10806\.Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Coltonet al\.\(2000\)S\. Colton, A\. Bundy, and T\. WalshOn the notion of interestingness in automated mathematical discovery\.International Journal of Human\-Computer Studies53\(3\),pp\. 351–375\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px3.p1.1)\.
- Davilaet al\.\(2025\)R\. Davila, B\. Brimkov, and R\. PepperIn reverie together: ten years of mathematical discovery with a machine collaborator\.arXiv preprint arXiv:2507\.17780\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px3.p1.1)\.
- Davila \(2024\)R\. DavilaAutomated conjecturing with TxGraffiti\.arXiv preprint arXiv:2409\.19379\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px3.p1.1)\.
- de Moura and Ullrich \(2021\)L\. de Moura and S\. UllrichThe Lean 4 theorem prover and programming language\.InInternational Conference on Automated Deduction \(CADE\),Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1),[§1](https://arxiv.org/html/2609.28603#S1.p6.1),[§2\.1](https://arxiv.org/html/2609.28603#S2.SS1.p1.1)\.
- Fajtlowicz \(1988\)S\. FajtlowiczOn conjectures of Graffiti\.InAnnals of Discrete Mathematics,Vol\.38,pp\. 113–118\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px3.p1.1)\.
- Gloeckleet al\.\(2024\)F\. Gloeckle, J\. Limperg, G\. Synnaeve, and A\. HayatABEL: sample efficient online reinforcement learning for neural theorem proving\.InThe 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24,Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px1.p1.1)\.
- Gloeckleet al\.\(2026\)F\. Gloeckle, A\. Rammal, C\. Arnal, R\. Munos, V\. Cabannes, G\. Synnaeve, and A\. HayatAutomatic textbook formalization\.arXiv preprint arXiv:2604\.03071\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px2.p1.1)\.
- Huang \(2026\)Y\. HuangAutonomous disproofs of the sum\-product conjecture overℝ\\mathbb\{R\}with GPT\-5\.5 Pro\.arXiv preprint arXiv:2607\.20525\.Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Kolmogorov \(1965\)A\. N\. KolmogorovThree approaches to the quantitative definition of information\.Problems of Information Transmission1\(1\)\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px4.p1.1)\.
- Lampleet al\.\(2022\)G\. Lample, M\. Lachaux, T\. Lavril, X\. Martinet, A\. Hayat, G\. Ebner, A\. Rodriguez, and T\. LacroixHyperTree proof search for neural theorem proving\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px1.p1.1)\.
- Lenat \(1977\)D\. B\. LenatAutomated theory formation in mathematics\.InProceedings of the 5th International Joint Conference on Artificial Intelligence \(IJCAI\),pp\. 833–842\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px3.p1.1)\.
- Li and Vitányi \(2008\)M\. Li and P\. VitányiAn introduction to Kolmogorov complexity and its applications\.3rd edition,Springer\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px4.p1.1),[§4](https://arxiv.org/html/2609.28603#S4.p2.1)\.
- Linet al\.\(2025\)Y\. Linet al\.Goedel\-Prover: a frontier model for open\-source automated theorem proving\.arXiv preprint arXiv:2502\.07640\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px1.p1.1)\.
- Litt \(2026\)D\. LittMathematics in the library of babel\.Note:Blog postExternal Links:[Link](https://www.daniellitt.com/blog/2026/2/20/mathematics-in-the-library-of-babel)Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p4.1)\.
- Miles Team \(2026\)Miles TeamMiles: enterprise\-grade reinforcement learning for large\-scale model post\-training\.Note:[https://github\.com/radixark/miles](https://github.com/radixark/miles)Cited by:[§2\.2](https://arxiv.org/html/2609.28603#S2.SS2.p1.1)\.
- Mishraet al\.\(2025\)S\. Mishra, Y\. Machino, G\. Poesia, A\. Jiang, J\. Hsu, A\. Weller, C\. Mishra, D\. Broman, J\. B\. Tenenbaum, M\. Jamnik, C\. E\. Zhang, and K\. M\. CollinsA matter of interest: understanding interestingness of math problems in humans and language models\.arXiv preprint arXiv:2511\.08548\.Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p5.1)\.
- Newell and Simon \(1956\)A\. Newell and H\. A\. SimonThe logic theory machine—a complex information processing system\.IRE Transactions on Information Theory2\(3\),pp\. 61–79\.External Links:[Document](https://dx.doi.org/10.1109/TIT.1956.1056797)Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Novikovet al\.\(2025\)A\. Novikov, N\. Vũ, M\. Eisenberger, E\. Dupont, P\. Huang, A\. Z\. Wagner, S\. Shirobokov, B\. Kozlovskii, F\. J\. R\. Ruiz, A\. Mehrabian, M\. P\. Kumar, A\. See, S\. Chaudhuri, G\. Holland, A\. Davies, S\. Nowozin, P\. Kohli, and M\. BalogAlphaEvolve: a coding agent for scientific and algorithmic discovery\.arXiv preprint arXiv:2506\.13131\.Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- OpenAI \(2026a\)OpenAIFinite time blowup for Navier–Stokes\.Technical reportOpenAI\.External Links:[Link](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf)Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- OpenAI \(2026b\)OpenAIGPT\-5\.5 System Card\.Technical reportOpenAI\.External Links:[Link](https://openai.com/index/gpt-5-5-system-card/)Cited by:[§2\.2](https://arxiv.org/html/2609.28603#S2.SS2.p2.1)\.
- Oum \(2026\)S\. OumA proof of the cycle double cover conjecture by OpenAI: an exposition\.arXiv preprint arXiv:2607\.16356\.Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Poesiaet al\.\(2024\)G\. Poesia, D\. Broman, N\. Haber, and N\. D\. GoodmanLearning formal mathematics from intrinsic motivation\.arXiv preprint arXiv:2407\.00695\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px3.p1.1),[§1](https://arxiv.org/html/2609.28603#S1.p5.1)\.
- Poincaré \(1905\)H\. PoincaréScience and hypothesis\.Walter Scott Publishing Company,London\.Note:Translated by W\. J\. GreenstreetCited by:[§1](https://arxiv.org/html/2609.28603#S1.p3.1.1)\.
- Polu and Sutskever \(2020\)S\. Polu and I\. SutskeverGenerative language modeling for automated theorem proving\.arXiv preprint arXiv:2009\.03393\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px1.p1.1)\.
- Pólya \(1981\)G\. PólyaMathematical discovery: on understanding, learning, and teaching problem solving\.Combined ed\. edition,John Wiley & Sons,New York\.External Links:ISBN 0\-471\-08975\-3Cited by:[§3\.1](https://arxiv.org/html/2609.28603#S3.SS1.p2.1.1)\.
- Qwen Team \(2026\)Qwen TeamQwen3\.6\-27B: flagship\-level coding in a 27B dense model\.External Links:[Link](https://qwen.ai/blog?id=qwen3.6-27b)Cited by:[§2\.2](https://arxiv.org/html/2609.28603#S2.SS2.p1.1),[§3\.3](https://arxiv.org/html/2609.28603#S3.SS3.p2.1)\.
- Rammalet al\.\(2026\)A\. Rammal, N\. Patel, F\. Gloeckle, A\. Hayat, J\. Kempe, R\. Munos, C\. Arnal, and V\. CabannesFormalizing mathematics at scale\.arXiv preprint arXiv:2605\.29955\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px2.p1.1)\.
- Renet al\.\(2025\)Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\. F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. RuanDeepSeek\-Prover\-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.arXiv preprint arXiv:2504\.21801\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px1.p1.1),[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Shaoet al\.\(2024\)Z\. Shao, P\. Wang, Q\. Zhu, R\. Xu, J\. Song, X\. Bi,et al\.DeepSeekMath: pushing the limits of mathematical reasoning in open language models\.arXiv preprint arXiv:2402\.03300\.Cited by:[§2\.2](https://arxiv.org/html/2609.28603#S2.SS2.p1.1)\.
- Solomonoff \(1964\)R\. J\. SolomonoffA formal theory of inductive inference, part I\.Information and Control7\(1\)\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px4.p1.1)\.
- Sothanaphan \(2026\)N\. SothanaphanResolution of Erdős problem \#728: a writeup of Aristotle’s Lean proof\.arXiv preprint arXiv:2601\.07421\.Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- The mathlib Community \(2020\)The mathlib CommunityThe Lean mathematical library\.InCertified Programs and Proofs \(CPP\),Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1),[§1](https://arxiv.org/html/2609.28603#S1.p6.1),[§2\.1](https://arxiv.org/html/2609.28603#S2.SS1.p1.1)\.
- Thurston \(2005\)W\. P\. ThurstonMathematical education\.External Links:math/0503081,[Link](https://arxiv.org/abs/math/0503081)Cited by:[§3\.2](https://arxiv.org/html/2609.28603#S3.SS2.p2.2.1)\.
- Tsoukalaset al\.\(2025\)G\. Tsoukalas, R\. Saha, A\. Thakur, S\. Reguyal, and S\. ChaudhuriLearning interestingness in automated mathematical theory formation\.arXiv preprint arXiv:2511\.14778\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px3.p1.1),[§1](https://arxiv.org/html/2609.28603#S1.p5.1)\.
- Turing \(1939\)A\. M\. TuringSystems of logic based on ordinals\.Proceedings of the London Mathematical Society45\(1\),pp\. 161–228\.External Links:[Document](https://dx.doi.org/10.1112/plms/s2-45.1.161)Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Urban \(2026\)J\. Urban130k lines of formal topology in two weeks: simple and cheap autoformalization for everyone?\.External Links:2601\.03298Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px2.p1.1)\.
- Wanget al\.\(2025\)H\. Wanget al\.Kimina\-Prover Preview: towards large formal reasoning models with reinforcement learning\.arXiv preprint arXiv:2504\.11354\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px1.p1.1)\.
- Wanget al\.\(2026\)Z\. Wang, W\. Ma, Z\. Ming, G\. Zhang, K\. Yuan, and Z\. WenM2F: automated formalization of mathematical literature at scale\.External Links:2602\.17016Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px2.p1.1)\.
- Wigner \(1960\)E\. P\. WignerThe unreasonable effectiveness of mathematics in the natural sciences\.Communications on Pure and Applied Mathematics13\(1\),pp\. 1–14\.External Links:[Document](https://dx.doi.org/10.1002/cpa.3160130102)Cited by:[§1](https://arxiv.org/html/2609.28603#S1.p2.1)\.
- Wuet al\.\(2022\)Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. SzegedyAutoformalization with large language models\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px2.p1.1)\.
- Xinet al\.\(2024\)H\. Xin, D\. Guo, Z\. Shao, Z\. Ren, Q\. Zhu, B\. Liu, C\. Ruan, W\. Li, and X\. LiangDeepSeek\-Prover: advancing theorem proving in LLMs through large\-scale synthetic data\.arXiv preprint arXiv:2405\.14333\.Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px1.p1.1),[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Xuet al\.\(2020\)Y\. Xu, S\. Zhao, J\. Song, R\. Stewart, and S\. ErmonA theory of usable information under computational constraints\.InInternational Conference on Learning Representations \(ICLR\),Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px4.p1.1)\.
- Yanget al\.\(2023\)K\. Yang, A\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. AnandkumarLeanDojo: theorem proving with retrieval\-augmented language models\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px1.p1.1),[§1](https://arxiv.org/html/2609.28603#S1.p1.1)\.
- Yinget al\.\(2024\)H\. Ying, Z\. Shi, Z\. He, B\. Gao, C\. Chen, Z\. Yu, S\. Song, Q\. Fan, Y\. Li, L\. Li,et al\.Lean workbook: a large\-scale Lean problem set formalized from natural language math problems\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[Appendix A](https://arxiv.org/html/2609.28603#A1.SS0.SSS0.Px2.p1.1)\.

## Contents

## Appendix ARelated Work

##### Language models for formal theorem proving\.

Language models can generate formal proof steps\([Polu and Sutskever, 2020](https://arxiv.org/html/2609.28603#bib.bib20)\), with subsequent systems adding tree search and reinforcement learning\([Lample et al\., 2022](https://arxiv.org/html/2609.28603#bib.bib21);[Gloeckle et al\., 2024](https://arxiv.org/html/2609.28603#bib.bib22)\), library retrieval\([Yang et al\., 2023](https://arxiv.org/html/2609.28603#bib.bib19)\), synthetic data\([Xin et al\., 2024](https://arxiv.org/html/2609.28603#bib.bib24)\), subgoal decomposition, and test\-time search\([AlphaProof and AlphaGeometry teams, 2024](https://arxiv.org/html/2609.28603#bib.bib23);[Ren et al\., 2025](https://arxiv.org/html/2609.28603#bib.bib25);[Lin and others, 2025](https://arxiv.org/html/2609.28603#bib.bib26);[Wang and others, 2025](https://arxiv.org/html/2609.28603#bib.bib27)\)\. These methods primarily optimize completion of a fixed target under a particular prover and budget, whereas we aim to explore open\-ended reasoning\.

##### Autoformalization and formal libraries at scale\.

LLM autoformalization has progressed from statement\-level translation\([Wu et al\., 2022](https://arxiv.org/html/2609.28603#bib.bib32)\)and paired datasets\([Azerbayev et al\., 2023](https://arxiv.org/html/2609.28603#bib.bib33);[Ying et al\., 2024](https://arxiv.org/html/2609.28603#bib.bib34)\)to large Lean developments from mathematical textbooks\([Urban, 2026](https://arxiv.org/html/2609.28603#bib.bib35);[Wang et al\., 2026](https://arxiv.org/html/2609.28603#bib.bib36);[Gloeckle et al\., 2026](https://arxiv.org/html/2609.28603#bib.bib37)\)\.AutoformBotandAtlasfurther demonstrate coordination and verification across 26 books\([Rammal et al\., 2026](https://arxiv.org/html/2609.28603#bib.bib48)\)\. Recent work has also begun formalizing research\-level results, such as the De Giorgi–Nash–Moser theory for elliptic PDEs\([Armstrong and Kempe, 2026](https://arxiv.org/html/2609.28603#bib.bib58)\)\. These results establish the scalability of formal\-library construction while exposing planning problems from missing infrastructure and long\-range dependencies\.

##### Automated mathematical discovery and conjecturing\.

AM and Graffiti pioneered automatic concept and conjecture generation\([Lenat, 1977](https://arxiv.org/html/2609.28603#bib.bib38);[Fajtlowicz, 1988](https://arxiv.org/html/2609.28603#bib.bib39)\), and interestingness itself became an explicit research problem\([Colton et al\., 2000](https://arxiv.org/html/2609.28603#bib.bib40)\)\. Graffiti’s successors, notably TxGraffiti\([Davila, 2024](https://arxiv.org/html/2609.28603#bib.bib56)\), have produced conjectures that led to multiple published papers over a decade of human–machine collaboration\([Davila et al\., 2025](https://arxiv.org/html/2609.28603#bib.bib57)\); however, these systems operate on graph invariants and their heuristic filters are intrinsically tied to that domain\.[Bengio and Malkin \(2024\)](https://arxiv.org/html/2609.28603#bib.bib47)propose an information\-theoretic view of mathematical interestingness, suggesting that valuable frameworks have small description length while being close to many provable statements; our definition can be seen as a computable, formal\-library\-grounded instantiation of this principle\. More recent systems jointly learn conjecturing and proof in small axiomatic domains\([Poesia et al\., 2024](https://arxiv.org/html/2609.28603#bib.bib41)\)or learn interestingness objectives for theory formation\([Tsoukalas et al\., 2025](https://arxiv.org/html/2609.28603#bib.bib42)\)\. Proposals for autonomous discovery add novelty assessment, result selection, and closed\-loop knowledge growth\([Barkeshli et al\., 2026](https://arxiv.org/html/2609.28603#bib.bib45)\)\. Our objective supplies such a signal at formal\- library scale, grounding intrinsic interestingness in verified proof length and relating it to a theorem’s extrinsic utility\. This separates the ability to generate valid statements from the harder problem of selecting discoveries\.

##### Description length and mathematical compression\.

Kolmogorov complexity measures shortest description length\([Solomonoff, 1964](https://arxiv.org/html/2609.28603#bib.bib30);[Kolmogorov, 1965](https://arxiv.org/html/2609.28603#bib.bib31);[Li and Vitányi, 2008](https://arxiv.org/html/2609.28603#bib.bib29)\), while proof length and statement description length are distinct finite\-corpus proxies\. Resource\-bounded information\([Xu et al\., 2020](https://arxiv.org/html/2609.28603#bib.bib44);[Blier and Ollivier, 2018](https://arxiv.org/html/2609.28603#bib.bib43)\)and recent views of mathematics as a proof hypergraph compressed by useful abstractions\([Barkeshli et al\., 2026](https://arxiv.org/html/2609.28603#bib.bib45);[Aksenov et al\., 2026](https://arxiv.org/html/2609.28603#bib.bib46)\)motivate our library\-grounded quantities\. Interestingness compares proof and description length, while utility measures downstream proof compression; both are relative to the available mathematical context\. They are computable, finite\-corpus proxies rather than claims about uncomputable description complexity\.

## Appendix BTraining the Difficulty ModelVθV\_\{\\theta\}

### B\.1Data

#### B\.1\.1Source corpus

From our extraction ofmathlib, we get 113,547 declarations\. For each declaration we record the fully qualified name, rendered type, and file path; the file\-local definitions required to interpret the target and premises; the project\-local theorem declarations referenced by the accepted proof; the source proof span and its non\-blank physical line count; and the dependency metadata used to change which premises are visible\.

From each theorem we build a group and are able to compute our reward within such a group\. Fix a root theoremTT, letPPbe the premises currently visible to the model, and letccbe the materialized computational\-cost of that pair: the number of proof lines needed to deriveTTfromPP\. WriteDDfor the file\-local definitions shipped with the prompt anddeps⁡\(⋅\)\\operatorname\{deps\}\(\\cdot\), for the extracted dependencies of a declaration\. Sample a cited lemma uniformly from the theorem declarations among the visible premises,

L∼Unif⁡\(P\)L\\sim\\mathrm\{Unif\}\\bigl\(P\)Letℓ\\ellbe the proof cost ofLL\. Now expand it: replacingLLby its own dependencies gives the expanded premise setP−P^\{\-\}, and dropping each of its premises independently gives the thinned premise setP\.8P^\{\.8\},

P−=\(P∖\{L\}\)∪deps⁡\(L\),P\.8=\{p∈P−:up<0\.8\},up∼Unif⁡\[0,1\]\.P^\{\-\}=\\bigl\(P\\setminus\\\{L\\\}\\bigr\)\\cup\\operatorname\{deps\}\(L\),\\qquad P^\{\.8\}=\\\{\\,p\\in P^\{\-\}:u\_\{p\}<0\.8\\,\\\},\\quad u\_\{p\}\\sim\\mathrm\{Unif\}\[0,1\]\.A proof fromP−P^\{\-\}can no longer citeLLand must derive it, so it costsc\+ℓc\+\\ell\. WritingDpreD\_\{\\rm pre\}for the definitions visible before the expansion andD⁡\(L\)D\(L\)for those ofLLalone, the edge emits six prompts\(target∣definitions,premises\)\(\\text\{target\}\\mid\\text\{definitions\},\\,\\text\{premises\}\)together with their observed computational\-cost labels\.

All six rows remain adjacent during reward construction, so that the reward can be evaluated within a group without any cross\-batch bookkeeping\. Roots, not individual prompt rows, determine the data split, so variants of one theorem never straddle the train/validation boundary\.

For each root, generation starts fromP=deps⁡\(T\)P=\\operatorname\{deps\}\(T\)andc=lines⁡\(T\)c=\\operatorname\{lines\}\(T\)and runs three deterministically seeded random expansion walks\. After an edge is emitted, the walk continues from\(P−,c\+ℓ\)\(P^\{\-\},c\+\\ell\)\. Each walk reservoir\-samples at most three eligible edges, stops after 300 expansion attempts or once the visible premise set reaches 150 premises, and excludes prompts above 60,000 characters\. The walks and reservoirs use seed 31; validation roots are randomly selected with probabilityp=0\.01p=0\.01\.

The final dataset contains 18,318 training groups \(109,908 prompts\) and 923 validation groups \(5,538 prompts\)\. Grounded labels have mean 92\.3, median 49, 90th percentile 245, and maximum 500 proof lines\.

#### B\.1\.2Prompt

Every model receives the same instruction template\. The frontier\-model evaluations permit free\-form reasoning but require the final integer after\#\#\#\#; training uses identical semantic content\.

YouaregivenLeandefinitions,premises,andatargettheoremstatement\.

Estimatetheproofdifficulty:thetotalnumberofprooflinesrequiredto

derivethetargettheoremfromthesepremises\.

Thedefinitionsarefile\-localdefinitionsthatthestatementandpremises

dependon\.Usethemonlytounderstandwhatthestatementmeans\-\-doNOT

judgedifficultybasedonthem,anddonotcountthemasprooflines\.

Payattentiontoexactlywhichpremisesareavailable\.Donotinfer

difficultyfromthenumberofpremisesalone\.

Donotdrafttheproof\.Justestimatethedifficultyfromthedependency

structure\.Giveaconciseestimate,thenputthefinalansweronitsownline:

\#\#\#\#<integer\>

Definitions:

\[numberedLeandeclarations\]

Premises:

\[numberedLeanhypotheses\]

Targettheorem:

theoremtarget:\[renderedtype\]:=by

Whatisthetotalproofdifficulty\(numberofprooflines\)?

Hypothesis names are normalized positionally toh1,h2, and so on; the target is renamedtarget; and any proof body after:= byis stripped\. The model sees file\-local definitions first, then premises, then the target\.

### B\.2Model and Optimization

#### B\.2\.1Training objective

Writem⁡\(x\)=log⁡\(1\+x\)m\(x\)=\\log\(1\+x\), letvr​jv\_\{rj\}be sampled completionjjfor rolerr, and letv¯r\\bar\{v\}\_\{r\}be the mean of the parsed completions for that role within the batch; we abbreviate the six role means ofbase,remaining\_keep,remaining\_remove,lemma\_context,lemma\_native, andbase\_dropasv¯base\\bar\{v\}\_\{\\rm base\},v¯keep\\bar\{v\}\_\{\\rm keep\},v¯rem\\bar\{v\}\_\{\\rm rem\},v¯ctx\\bar\{v\}\_\{\\rm ctx\},v¯nat\\bar\{v\}\_\{\\rm nat\}, andv¯drop\\bar\{v\}\_\{\\rm drop\}\. Algorithm[1](https://arxiv.org/html/2609.28603#alg1)gives the per\-completion reward used before GRPO normalization\. Define the Bellman residuala⁡\(x,y,z\)=\|m⁡\(x\)−m⁡\(y\+z\)\|a\(x;y,z\)=\|m\(x\)\-m\(y\+z\)\|and the agreement residualq⁡\(x,y\)=\|m⁡\(x\)−m⁡\(y\)\|q\(x,y\)=\|m\(x\)\-m\(y\)\|\.

Algorithm 1TrainingReward— exact per\-completion reward\.1:completion

v=vr​jv=v\_\{rj\}of role

rr; role means

v¯base\\bar\{v\}\_\{\\rm base\},

v¯keep\\bar\{v\}\_\{\\rm keep\},

v¯rem\\bar\{v\}\_\{\\rm rem\},

v¯ctx\\bar\{v\}\_\{\\rm ctx\},

v¯nat\\bar\{v\}\_\{\\rm nat\},

v¯drop\\bar\{v\}\_\{\\rm drop\}; label

crc\_\{r\}
2:reward

ℛr​j\\mathcal\{R\}\_\{rj\}
3:if

vvdoes not contain exactly one</think\>followed by exactly one terminal\#\#\#\# non\-negative\-integerthen

4:return

−2000\-2000
5:endif

6:

etruth←0e\_\{\\rm truth\}\\leftarrow 0if

r=base\_dropr=\\text\{\{base\\\_drop\}\}, else

q⁡\(v,cr\)q\(v,c\_\{r\}\)
7:if

r=baser=\\text\{\{base\}\}then

8:

eadd←14\[a\(v;v¯keep,v¯ctx\)\+a\(v;v¯keep,v¯nat\)e\_\{\\rm add\}\\leftarrow\\tfrac\{1\}\{4\}\\bigl\[a\(v;\\bar\{v\}\_\{\\rm keep\},\\bar\{v\}\_\{\\rm ctx\}\)\+a\(v;\\bar\{v\}\_\{\\rm keep\},\\bar\{v\}\_\{\\rm nat\}\)
9:

\+a\(v;v¯rem,v¯ctx\)\+a\(v;v¯rem,v¯nat\)\]\+\\,a\(v;\\bar\{v\}\_\{\\rm rem\},\\bar\{v\}\_\{\\rm ctx\}\)\+a\(v;\\bar\{v\}\_\{\\rm rem\},\\bar\{v\}\_\{\\rm nat\}\)\\bigr\]
10:

edrop←\[m⁡\(v\)−m⁡\(v¯drop\)\]\+e\_\{\\rm drop\}\\leftarrow\[\\,m\(v\)\-m\(\\bar\{v\}\_\{\\rm drop\}\)\\,\]\_\{\+\}
11:elseif

r=remaining\_keepr=\\text\{\{remaining\\\_keep\}\}or

r=remaining\_remover=\\text\{\{remaining\\\_remove\}\}then

12:

eadd←12​\[a⁡\(v¯base,v,v¯ctx\)\+a⁡\(v¯base,v,v¯nat\)\];edrop←0e\_\{\\rm add\}\\leftarrow\\tfrac\{1\}\{2\}\\bigl\[a\(\\bar\{v\}\_\{\\rm base\};v,\\bar\{v\}\_\{\\rm ctx\}\)\+a\(\\bar\{v\}\_\{\\rm base\};v,\\bar\{v\}\_\{\\rm nat\}\)\\bigr\];\\quad e\_\{\\rm drop\}\\leftarrow 0
13:elseif

r=lemma\_contextr=\\text\{\{lemma\\\_context\}\}then

14:

eadd←13​\[a⁡\(v¯base,v¯keep,v\)\+a⁡\(v¯base,v¯rem,v\)\+q⁡\(v,v¯nat\)\];edrop←0e\_\{\\rm add\}\\leftarrow\\tfrac\{1\}\{3\}\\bigl\[a\(\\bar\{v\}\_\{\\rm base\};\\bar\{v\}\_\{\\rm keep\},v\)\+a\(\\bar\{v\}\_\{\\rm base\};\\bar\{v\}\_\{\\rm rem\},v\)\+q\(v,\\bar\{v\}\_\{\\rm nat\}\)\\bigr\];\\quad e\_\{\\rm drop\}\\leftarrow 0
15:elseif

r=lemma\_nativer=\\text\{\{lemma\\\_native\}\}then

16:

eadd←13​\[a⁡\(v¯base,v¯keep,v\)\+a⁡\(v¯base,v¯rem,v\)\+q⁡\(v,v¯ctx\)\];edrop←0e\_\{\\rm add\}\\leftarrow\\tfrac\{1\}\{3\}\\bigl\[a\(\\bar\{v\}\_\{\\rm base\};\\bar\{v\}\_\{\\rm keep\},v\)\+a\(\\bar\{v\}\_\{\\rm base\};\\bar\{v\}\_\{\\rm rem\},v\)\+q\(v,\\bar\{v\}\_\{\\rm ctx\}\)\\bigr\];\\quad e\_\{\\rm drop\}\\leftarrow 0
17:else⊳\\trianglerightr=base\_dropr=\\text\{\{base\\\_drop\}\}

18:

eadd←0;edrop←\[m⁡\(v¯base\)−m⁡\(v\)\]\+e\_\{\\rm add\}\\leftarrow 0;\\quad e\_\{\\rm drop\}\\leftarrow\[\\,m\(\\bar\{v\}\_\{\\rm base\}\)\-m\(v\)\\,\]\_\{\+\}
19:endif

20:return

−0\.50​etruth−0\.35​eadd−0\.15​edrop\-0\.50e\_\{\\rm truth\}\-0\.35e\_\{\\rm add\}\-0\.15e\_\{\\rm drop\}

#### B\.2\.2Hyperparameters

### B\.3Evaluation Protocols

Evaluation is performed with greedy decoding and an 8,192\-token response cap, to match training\. MAE, median absolute error, log\-spaceR2R^\{2\}, and Spearmanρ\\rhoare computed over all valid outputs\. Every row from Claude and the trained modelVθV\_\{\\theta\}is successfully parsed, whereas GPT\-5\.5 produced 6 invalid outputs across all 4,615 prompts\.

Calibration points in Figure[1](https://arxiv.org/html/2609.28603#S2.F1)divide\[0,450\]\[0,450\]proof lines into five equal\-width 90\-line bins\. Within each observed\-difficulty bin the marker gives the mean observed label against the mean prediction, and the shaded band spans the 25th–75th percentiles of predictions\. Binning is used only for the plot on the left of Figure[1](https://arxiv.org/html/2609.28603#S2.F1); every aggregate metric on the right is computed on unbinned rows\.

## Appendix CTraining a Conjecturing Model

### C\.1Conjecturing Model Training

#### C\.1\.1Data construction

The theorem\-proposal data are reconstructed from thebase\_droprows of the corpus from[B\.1](https://arxiv.org/html/2609.28603#A2.SS1), and only the premises are used here\. Premises are renamed positionally, and contexts with fewer than 16 premises or more than 12,288 tokens are removed\. From this we randomly select 10,000 sets of premises for training and an additional 512 for validation, each set containing a median of 77 premises\. The model sees definitions and premise statements but never the source theorem or its proof\. Section[C\.1\.4](https://arxiv.org/html/2609.28603#A3.SS1.SSS4)gives the verbatim system and user templates\.

#### C\.1\.2Compilation, relevance, and triviality

A response must contain exactly one nonempty expression between<<<STATEMENT\>\>\>and<<<END\>\>\>\. Pantograph\([Aniva et al\., 2025](https://arxiv.org/html/2609.28603#bib.bib53)\)compiles the expression as the type of a standalone theorem against themathlibenvironment, to ensure it is syntactically valid\. We only allow for the model to produce theorems and reject declarations, definitions, proof commands,:=, andsorry; parse failures receive−0\.5\-0\.5and expressions that fail compilations receive−0\.25\-0\.25\.

For a compiled type, the global definition graph computesL⁡\(T∣P\)L\(T\\mid P\)by subtracting the vocabulary exposed by the supplied premises\. The proposal must share at least one non\-generic identifier with a premise/definition context; failure receives−0\.25\-0\.25\. Direct premise restatements \(as measured by token\-level similarity\) are marked trivial\. Other candidates are tested for triviality usingassumption,rfl,simp,tauto, andsimp\_all; a candidate closed by any one receives reward of00\. Only valid, relevant, nontrivial statements are sent to theVθV\_\{\\theta\}LLM to judge the difficulty, and they then receive reward according to Equation[8](https://arxiv.org/html/2609.28603#S3.E8)\.

#### C\.1\.3Optimization configuration

#### C\.1\.4Theorem\-proposal prompt

Bracketed fields such as\[NUMBERED PREMISES\]are populated mechanically with the corresponding Lean declarations; they are not additional instructions\.

The system message is:

YouareanexpertLean4andMathlibtheoremproposer\.Answerimmediatelywiththetaggedtheoremstatement\.Donotthinkaloud,explain,explore,orwriteaproof\.Yourfirstoutputmustbe<<<STATEMENT\>\>\>andthewholeresponseshouldstayunder256tokens\.

The user message is:

GiventheLeanpremisesbelow,proposeonenew,interestingtheoremstatementthatisaplausiblelogicalconsequenceofthem\.Thestatementwillbescoredbyestimatedproofdifficultydividedbyitspremise\-relativedefinitionlength\.

Astrongtheoremisnontrivial,concise,andusesmultiplepremisesinameaningfulway\.Itmustbeawell\-typedLeanpropositionthatcouldactuallybeprovedfromtheavailablepremises\.DonotoutputFalse,anunsupportedconjecture,arestatementofonepremise,avacuousimplication,orareflexiveidentitysuchas‘x=x‘or‘P<\-\>P‘\.Usemathematicalobjectsoroperationssuppliedbyatleasttwodifferentpremises\.Theoutputmustbeastandaloneproposition:donotmentionlocalaliasessuchas‘h1‘inthegeneratedstatement\.

Preferashortconsequenceobtainedbyinstantiatingandchainingtheexactpremisesoverabroadtheoremwithmanyfreshlyinventedbinders\.Copynamespaces,bindertypes,typeclassassumptions,andfunctionargumentorderexactlyfromthedeclarationsbelow\.Donotguessshorthandnamesornotationthatisnotshown\.Ifyouuseapremisenamesuchas‘h2‘,applyitonlyatitsdisplayedsignature\.

Silentlytype\-checkthefinalexpressionbeforeemittingit:fullyapplymapsthatneedarguments,giveeverynewvariableanexplicittype,anduseeachoperationonlyonvaluesofitsdeclaredtype\(forexample,donotaddorsubtractpropositions\)\.Theoutputisatype,sodonotuse‘let‘,‘by‘,‘:=‘,holes,tactics,proofterms,or‘\#‘cardinalitynotation\.Donotprintthischeck\.

\#Definitionsforunderstandingthepremisevocabulary

\[NUMBEREDDEFINITIONS,WHENPRESENT\]

\#Availablepremisedeclarations\(\[POSITIONALPREMISENAMES\]\)

\[NUMBEREDPREMISES\]

\#Outputcontract

OutputonlyasinglestandaloneLeantypeexpressionbetweenthetags\.Donotreferencethepremisealiasesabove\.Ifnewvariablesarenecessary,bindthemwithaleading‘forall‘/‘forall‘\.Donotincludeatheoremname,‘:=by‘,proof,codefence,orcommentary\.

<<<STATEMENT\>\>\>

<oneconciseLeantheoremstatement\>

<<<END\>\>\>

### C\.2Conjecturing Model Evaluation

#### C\.2\.1Balanced verified cohort

The eight strata we select premises from are Algebra, Analysis, Number Theory, Measure/Probability, Geometry/Topology, Combinatorics, Category/Algebraic Geometry, and Foundations\. For each group, we sample theorems from each of the three models we evaluate \(Claude, the trained conjecturing model, and the base model\), and pass it to a Claude Code with Claude Opus 4\.6 as a proof agent\. We repeat until we have 20 distinct theorems from each area\.

The proving agent first attempts the statement byte\-for\-byte\. If that fails, a separate marginal\-repair pass may add a necessary hypothesis, correct an index or bound, or narrowly weaken a conclusion\. A repair is accepted only if it compiles, preserves the counts of∀,∃,↔,∧,∨,¬\\forall,\\exists,\\leftrightarrow,\\land,\\lor,\\neg, passes anti\-vacuity checks, and has a token\-set Jaccard similarity at least0\.700\.70, to disallow the statement becoming irrelevant or too easy\. We recompute proof lines and conditional length from the final compiled declaration and compiled proof, so the reported score is ground\-truth interestingness under the proving pipeline rather than the difficulty model’s training reward\.

#### C\.2\.2Mathlib containment

Claude Opus 4\.6 at temperature 0 independently judges all 480 verified statements with proposer, area, and model hidden\. Each prompt includes the final statement, verified proof body, and referencedmathlibdeclarations as non\-exhaustive evidence\. The proof scaffold is pinned tomathlibrevision905b95\.\.\.\. Scores range from 1 \(not contained\) to 5 \(an exact or trivially equivalent named declaration exists\); score 4 denotes a few\-line wrapper or immediate specialization\. The judge must name a concrete declaration for score 5 and returns structured JSON\. Figure[5](https://arxiv.org/html/2609.28603#S3.F5)reports all of the recorded statements per model\. The complete rubric and judge prompt are provided in Section[C\.2\.3](https://arxiv.org/html/2609.28603#A3.SS2.SSS3)\.

#### C\.2\.3Mathlib\-containment rubric and judge prompt

The five\-level rubric is:

5\-\-Fullycontained\.Theexactstatement\(oradirect,triviallyequivalentreformulation\)existsinMathlibasanameddeclaration\.Ausercouldciteitdirectly,orwithathinwrapper\.

4\-\-Substantiallycontained\.ThestatementisprovableinafewlinesfromexistingMathliblemmas,orastrictlymoregeneralversionisinMathlibandthetargetisanimmediatespecialization\.

3\-\-Partiallycontained\.Coreingredients\(definitionsandkeysupportinglemmas\)existinMathlib,buttheheadlinestatementitselfisnotthereandwouldrequirenontrivialassembly\.

2\-\-Minimallycontained\.Onlybackgrounddefinitionsorunrelatedprerequisitesareavailable;thesubstantivecontentismissing\.

1\-\-Notcontained\.Mathlibdoesnotcontainthestatementorthenecessaryspecializeddefinitions\.

Operationalguidance:

\-Judgelibrarycontainment,notmathematicalvalidity,beauty,novelty,importance,orapparentdifficulty\.

\-"Afewlines"meansashortLeanproofassembleddirectlyfromexistingdeclarations,notmerelyashortinformalmathematicalargument\.

\-Usescore5onlywhenthereisaconcretematchingnameddeclaration\(possiblywithsymmetry,simplification,notationchanges,oranimmediatespecialization\)\.Identifythatdeclarationwheneverpossible\.

\-AverifiedproofanditsreferencedMathlibdeclarationsaresuppliedasevidence\.Theyarenotexhaustive:ageneratedproofmayoverlookamoredirectexistingtheorem,andprooflengthisnotbyitselfdispositive\.

\-Donotinferahighscoremerelybecausethetheoremiselementary\.Conversely,donotinferalowscoremerelybecauseitsgeneratedproofislong\.

\-Iftheexactdeclarationnameisuncertain,reportthatuncertaintyandavoidscore5unlesstheAPImatchisotherwiseunmistakable\.

Each item is judged with:

YouareanimpartialexpertjudgeofLean4Mathliblibrarycontainment\.

Applythesuppliedrubricexactly\.EstimatehowmuchofthetargettheoremisalreadycontainedinMathlib\.Thetheoremhasbeenverified,sodonotjudgewhetheritistrue\.Donotjudgeitsmathematicalnovelty,importance,elegance,ordifficulty\.

Theproofbodyandreferenceddeclarationsaresupportingevidence,notanexhaustiveMathlibsearch\.Ageneratedproofcanmissadirectexistingtheorem\.Treatscore5asrequiringaconcretematchingnameddeclarationoranunmistakablydirectAPImatch\.Distinguishagenuinelyfew\-lineMathlibwrapper\(score4\)fromnontrivialassemblyofingredients\(score3\)\.

<rubric\>

\[RUBRICABOVE\]

</rubric\>

<target\_theorem\>

\[STATEMENT\]

</target\_theorem\>

<verified\_proof\_bodylines="\[LINECOUNT\]"\>

\[PROOFBODY\]

</verified\_proof\_body\>

<referenced\_mathlib\_declarations\>

\[NAMESANDTYPES,ORNORECOVEREDLIST\]

</referenced\_mathlib\_declarations\>

ReturnexactlyoneJSONobjectandnoMarkdownorsurroundingcommentary:

\{

"score":<integer1\-5\>,

"matching\_declaration":"<concreteMathlibdeclarationforscore5,bestcandidateotherwise,ornone\>",

"supporting\_declarations":\["<zeroormoreimportantdeclarationnames\>"\],

"rationale":"<conciseexplanationtiedtotherubric\>",

"confidence":"<high\|medium\|low\>"

\}

### C\.3Selected Generations

Each item gives the final compiled Lean statement followed by a mathematical informalization\.

- ∀\\forallq:ℍ\\mathbb\{H\}, q\*q=\-1↔\\leftrightarrowq\.re=0∧\\land∥\\\|q∥\\\|=1 Quaternionic square roots of minus one\.A real quaternion squares to−1\-1if and only if its real component is zero and its norm is one\. Equivalently, the square roots of−1\-1are precisely the unit purely imaginary quaternions\.
- ∀\\forallz:UpperHalfPlane, ∃\\existsn:ℕ\\mathbb\{N\},0<n∧\\land ∥\\\|Complex\.exp \(2\*↑\\uparrowReal\.pi\*Complex\.I\*↑\\uparrowz\)^n∥\\\|<1/2 Decay of the upper\-half\-plane exponential\.For everyzzin the complex upper half\-plane, some positive power ofe2​π​i​ze^\{2\\pi iz\}has absolute value less than1/21/2\.
- ∀\\forall\(n:Type\_\)\[Fintypen\]\[DecidableEqn\] \(R:Type\_\)\[CommRingR\] \(A:MatrixnnR\), A\*A=1↔\\leftrightarrow A\.det\*A\.det=1∧\\land A\.adjugate=A\.det∙\\mathbin\{\\bullet\}A Involutory matrices and their adjugates\.For a finite square matrixAAover a commutative ring,A2=IA^\{2\}=Iif and only if\(detA\)2=1\(\\det A\)^\{2\}=1andadj⁡\(A\)=\(detA\)​A\\operatorname\{adj\}\(A\)=\(\\det A\)A\.
- ∀\\forallκ\\kappa:Cardinal, κ\\kappa\*κ\\kappa=κ\\kappa↔\\leftrightarrow κ\\kappa=0∨\\lorκ\\kappa=1∨\\lorCardinal\.aleph0≤\\leqκ\\kappa Multiplicatively idempotent cardinals\.A cardinal is unchanged by squaring exactly when it is00,11, or infinite \(equivalently, at leastℵ0\\aleph\_\{0\}\)\.
- ∀\\forallz:UpperHalfPlane, ∃\\existsw:UpperHalfPlane, w=\-\(1:ℂ\\mathbb\{C\}\)/\(z:ℂ\\mathbb\{C\}\)∧\\land ∀\\foralln:ℕ\\mathbb\{N\},n\>0↔\\leftrightarrow \(↑\\uparrown:ℂ\\mathbb\{C\}\)\*\(z:ℂ\\mathbb\{C\}\)≠\\neq0 Modular inversion in the upper half\-plane\.For every upper\-half\-plane pointzz, the modular inversew=−1/zw=\-1/zis again in the upper half\-plane\. Moreover, for every natural numbernn, positivity ofnnis equivalent to the nonvanishing of the complex productn​znz\.
- ∀\\forall\(R:Type\_\)\[CommRingR\], ∀\\forall\(W’:WeierstrassCurve\.JacobianR\) \(P:Fin3→\\toR\), W’\.Equation\(W’\.negP\)↔\\leftrightarrowW’\.EquationP Negation preserves the Jacobian equation\.For a Jacobian Weierstrass model over any commutative ring, negating a projective point preserves the curve equation:−P\-Plies on the curve exactly whenPPdoes\.
- ∀\\forall\(K:Type\_\)\[FieldK\]\(f:PolynomialK\), Function\.Injective \(fung:PolynomialK=\>g\*f\)↔\\leftrightarrow f≠\\neq0 Injectivity of polynomial multiplication\.Over a field, right multiplication by a polynomialffis injective on the polynomial ring if and only ifffis nonzero\.
- ∀\\forall\(K:Type\_\)\[FieldK\]\[NumberFieldK\] \(x:K\), x≠\\neq0↔\\leftrightarrow ∀\\forallw:NumberField\.InfinitePlaceK, \(NumberField\.InfinitePlace\.mk \(NumberField\.InfinitePlace\.embeddingw\)\)x\>0 Positivity at every infinite place\.An element of a number field is nonzero exactly when its value at every infinite place is strictly positive, where an infinite place evaluates through the absolute value associated with its embedding\.
- ∀\\forall\(α\\alpha:Type\_\)\[GeneralizedBooleanAlgebraα\\alpha\] \(ab:α\\alpha\), a=b↔\\leftrightarrow ∀\\forallc:α\\alpha,a\\c=b\\c∧\\landc\\a=c\\b Equality via relative complements\.Two elementsa,ba,bof a generalized Boolean algebra are equal exactly when, for everycc, removingccfrom them gives the same result and removing them fromccalso gives the same result\.
- ∀\\forall\(V:Type\_\)\[FiniteV\]\(G:SimpleGraphV\), G\.edgeSet=∅\\varnothing↔\\leftrightarrow ∀\\foralls:SetV,G\.IsCliques↔\\leftrightarrows\.ncard<2 Empty graphs characterized by their cliques\.A finite simple graph has no edges if and only if its cliques are precisely the vertex sets containing fewer than two vertices\.
- ∀\\forall\(V:Type\_\)\(G:SimpleGraphV\)\[FiniteV\], G\.IsClique\(Set\.univ:SetV\)↔\\leftrightarrow ∀\\forall\(M:Gc\.Subgraph\), M\.IsMatching↔\\leftrightarrowM\.verts=∅\\varnothing Completeness through matchings in the complement\.A finite simple graph is complete if and only if a subgraph of its complement is a matching exactly when that subgraph has no vertices\.
- ∀\\foralln:ℕ\\mathbb\{N\},n\>0↔\\leftrightarrow ∀\\forallf:Polynomialℝ\\mathbb\{R\},f\.natDegree≤\\leqn\-1→\\to \(\(∀\\forallk<n, Polynomial\.eval \(Polynomial\.Chebyshev\.nodenk\)f=0\)↔\\leftrightarrow f=0\) Vanishing at Chebyshev nodes\.A natural numbernnis positive exactly when every real polynomial of degree at mostn−1n\-1that vanishes at allnnChebyshev nodes is the zero polynomial \(and the zero polynomial vanishes at those nodes\)\.
- ∀\\forall\(C:Type\_\)\[CategoryTheory\.CategoryC\] \[CategoryTheory\.AbelianC\] \(XY:C\)\(f:X⟶\\longrightarrowY\), CategoryTheory\.Monof→\\to \(CategoryTheory\.IsIsof↔\\leftrightarrow ∀\\forall\(Z:C\)\(g:Y⟶\\longrightarrowZ\), \(g=0↔\\leftrightarrowf≫\\ggg=0\)\) Detecting isomorphisms in an abelian category\.Letf:X→Yf:X\\to Ybe a monomorphism in an abelian category\. Thenffis an isomorphism exactly when precomposition withffdetects zero morphisms out ofYY: for everyg:Y→Zg:Y\\to Z, one hasg=0g=0if and only ifg∘f=0g\\circ f=0\.

## Appendix DInference\-Time Pruning Ablation

In this experiment, we aim to isolate the effect of the promotion rule in the recursive discovery loop of Section[3\.4](https://arxiv.org/html/2609.28603#S3.SS4)\. All four trajectories we study start from the set of 80 premisesP0P\_\{0\}from graph theory, and share the same Claude Opus 4\.6 conjecturer model, and Claude Code based proving procedure\. Each initial generation pass proposes 400 statements\. Every prompt contains 20 premises: five sampled from the immediately preceding setPn\\Pn−1P\_\{n\}\\backslash P\_\{n\-1\}and 15 from the initial pool and older promoted roundsPn−1P\_\{n\-1\}\.

These statements are proved independently in Lean\. We compare four post\-verification promotion rules:*no pruning*retains every verified novel statement;*random*retains ten uniformly at random;*proof length*retains the ten statements with the longest verified proofs; and*interestingness*retains the ten statements with the largest ratio

I^ver​\(T∣P\)=100​lines in the accepted proof of​Tcharacters in the normalized statement of​T\.\\widehat\{I\}\_\{\\rm ver\}\(T\\mid P\)=100\\,\\frac\{\\text\{lines in the accepted proof of \}T\}\{\\text\{characters in the normalized statement of \}T\}\.\(9\)
### D\.1Comparison across promotion policies

All policies share the same initial premises and differ only in which verified statements are promoted\. Table[1](https://arxiv.org/html/2609.28603#A4.T1)compares the statements promoted over the ten rounds\. Mean interestingness is computed within each round and then averaged across rounds, giving every round equal weight\.

Table 1:Quality of the promoted statementsUnsurprisingly, interestingness pruning produces the highest mean and median interestingness, while proof\-length pruning produces the longest proofs\. A direct advantage on promoted interestingness is partly expected because one policy selects on that quantity\. We therefore separately evaluate every unique candidate successfully proved in Lean*before*the current round’s promotion rule is applied\. Table[2](https://arxiv.org/html/2609.28603#A4.T2)reports their number, mean and median interestingness, and mean proof length across all ten rounds, using the same aggregation as Table[1](https://arxiv.org/html/2609.28603#A4.T1)\.

Table 2:Verified candidates before selection\.The judge sees four statements at a time, one from each policy, and ranks them by mathematical interestingness\. Policy names, proofs, and scores are hidden\. We evaluate 100 such groups, and show the results below\.

Table 3:Direct policy\-blinded judgment of mathematical interestingness\.The judge also evaluates ten groups of ten statements promoted by each policy in each round as a group\. Policy names and scores are hidden\. The judge rates the group’s overall quality and diversity and identifies repeated theorem families\. For no pruning, which retains more than ten statements, we select ten at random\.

Table 4:Policy\-blinded cohort judgment\.Entries are mean±\\pmsample standard deviation across the ten round\-level cohorts for each promotion rule\.
### D\.2Judge prompts

The complete judge instruction is deliberately short and uses a broad notion of what a mathematician might appreciate:

Youareamathematiciancomparingfourformallyverifiedtheoremstatements\.

Rankthemfrommosttoleastmathematicallyinteresting\.Useabroadnotionofinterestingness:amathematicianmightappreciateastatementbecauseitisnontrivial,surprising,elegant,conceptuallyilluminating,potentiallyusefulorreusable,connectsideas,oropensfurtherquestions\.Judgethemathematicalcontent,notnotation,verbosity,statementlength,orguessedprooflength\.

\[A\]

<THEOREM\>

\[B\]

<THEOREM\>

\[C\]

<THEOREM\>

\[D\]

<THEOREM\>

ReturnexactlyoneJSONobjectandnoMarkdown:

\{"ranking":\["A","B","C","D"\],"rationale":"oneortwosentences","confidence":"high\|medium\|low"\}

The complete cohort\-judge prompt is:

YouareanimpartialexpertjudgeofacollectionoftenverifiedLean4theoremstatements\.

Thestatementsareallcorrect\.Judgethecollectionitself,withoutguessingitssourceorgenerationmethod\.

Ratetwodimensionsfrom1to5\.

MATHEMATICALQUALITY

5:Mostlynontrivial,coherent,potentiallyreusableresultsthatexpresssubstantivemathematicalcontent\.

4:Generallymeaningfulresultswithsomeroutineoroverlyspecializeditems\.

3:Mixedquality;severalusefulstatementsbutsubstantialroutineconjunctions,wrappers,ornarrowvariants\.

2:Mostlyshallow,over\-specialized,ormechanicallyassembledstatements\.

1:Almostentirelytrivial,incoherent,vacuous,orunhelpfulstatements\.

SEMANTICDIVERSITY

5:Manygenuinelydistincttheoremfamiliesormathematicalideas,withlittleredundancy\.

4:Severaldistinctfamiliesandonlylimitedrepetition\.

3:Ameaningfulmixture,butmultiplestatementsrepeatthesamecorepattern\.

2:Dominatedbyoneortwonarrowfamilieswithsuperficialvariations\.

1:Nearlyallstatementsareequivalent,nestedvariants,orroutinerepackagings\.

Groupstatementsbytheirsubstantiveconclusionandproofidea,notmerelysurfacesyntax\.Astronger/weakervariantorconjunctionofthesamecorefactsshouldnormallystayinthesamefamily\.

<statements\>

\[1\]

<THEOREM\>

\.\.\.

\[10\]

<THEOREM\>

</statements\>

ReturnexactlyoneJSONobjectandnoMarkdown:

\{

"quality\_score":<integer1\-5\>,

"diversity\_score":<integer1\-5\>,

"distinct\_families":<integer1\-10\>,

"redundant\_statement\_indices":\[<zeroormoreintegers1\-10\>\],

"family\_assignments":\[\{"indices":\[<integers\>\],"family":"<shortlabel\>"\}\],

"rationale":"<conciseexplanation\>",

"confidence":"<high\|medium\|low\>"

\}

## Appendix EAdditional Figures

### E\.1Cross\-area interestingness matrix

The displayed matrix uses ten targets from each of 12 areas\. Starting from one area\-conditioned premise frontier per column, we apply three synchronous expansion rounds: every current extracted theorem premise is replaced by all original theorem premises used in its proof, unavailable declarations remain terminals, and each resulting frontier is deduplicated\. FreshVθV\_\{\\theta\}predictions are obtained for all 1,440 target–condition pairs\. Each target’s score is divided by its same\-area score before cell medians are formed\. Only 28 off\-diagonal 95% confidence intervals exclude one\. Across the 132 off\-diagonal cell medians, the median is0\.5200\.520and 73\.5% are below one\. We see here that, as we might expect, a definition\-heavy field such as measure theory becomes much less interesting when it is not given premises from analytic areas\. We find also that some areas, such as algebra, become more interesting when supplied with premises from other fields\.

![Refer to caption](https://arxiv.org/html/2609.28603v1/area_matrix.png)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\.
### E\.2Iterative discovery graphs

Figure[12](https://arxiv.org/html/2609.28603#A5.F12)provides more iterative discovery graphs\.

\{subfigure\}

\[b\]![Refer to caption](https://arxiv.org/html/2609.28603v1/forward_dependency_graph_algebra.png)

Figure 9:Algebra\. For monicqqandrr, reducingp​rprmoduloq​rqrequals reducingppmoduloqqand then multiplying byrr\.\{subfigure\}

\[b\]![Refer to caption](https://arxiv.org/html/2609.28603v1/forward_dependency_graph_measure_probability.png)

Figure 10:Measure/probability\. Ifμ\\muis absolutely continuous with respect toν\\nu, then under the stated measurability conditions, the sum of the pushforwards ofc​μc\\muandμ\\muis absolutely continuous with respect to\(c\+1\)\(c\+1\)times the pushforward ofν\\nu\.\{subfigure\}

\[b\]![Refer to caption](https://arxiv.org/html/2609.28603v1/forward_dependency_graph_number_theory.png)

Figure 11:Number theory\. Applying a real invertible2×22\\times 2matrix to a nonreal complex number and then applying its inverse restores the imaginary part\.Figure 12:Iterative forward\-discovery graphs throughP6P\_\{6\}\.Each panel shows 30 of the 240 initial premises inP0P\_\{0\}, always retaining every initial premise used by a displayed proof\. Gray lines record explicit dependencies in accepted Lean proofs; coral marks the ancestry of the theorem with the highest totalP0P\_\{0\}\-relative interestingness among the statements introduced inP6P\_\{6\}\. Green encodeslog10⁡IP0\\log\_\{10\}I\_\{P\_\{0\}\}with a separate scale in each panel\. Each subcaption reports the selected statement\.