Recently, Large Language Models (LLMs) have been increasingly able to solve advanced mathematical problems, including many that have been open for decades. This opens the door to expansion of mathematical knowledge at unprecedented scale. Yet, while LLMs may be able to conjecture and prove more and more theorems, it remains open whether this new mathematical knowledge is interesting or useful. We define intrinsic interestingness of a theorem as the ratio between the length of its proof and the length of its statement. We show that this correlates strongly with an extrinsic measure of the downstream utility of a theorem. We identify the difficulty of a proof conditioned on a set of premises as a useful primitive for computing these metrics, and train a 27B model that predicts proof difficulty more accurately than frontier general-purpose models. Optimizing for our metric creates a model capable of producing more interesting theorems, while also reducing substantial or full overlap with Mathlib from 91.9% to 30.6%, showcasing the creation of more out-of-distribution math. We show that our system can generate candidate theorems, select the most interesting among them, and iteratively build on a self-expanding mathematical library. These metrics provide a practical and quantifiable signal for ranking conjectures and guiding proof search within formal mathematical libraries. Our framework provides a path towards self-expanding, machine-verified mathematical libraries that can choose worthwhile statements without relying on human-supplied targets.
Figures & tables
Figure 1: The trained value is substantially better calibrated on held-out samples from mathlib . The left panel groups examples by observed proof length, points give the mean observed and mean predicted proof lines, and shaded bands the interquartile range of predictions within each bin. The dashed line represents what we would expect from an optimal predictor. Note that all models underestimate proof length with increased length. The right plots report matched MAE and Spearman ρ on all 4,615 validation prompts.
Figure 2: Quantifying the interestingness of a statement. Here we show the distribution of interestingness I0 , as defined in Section 3.1 , of all statements from mathlib . The resulting ordering is intuitive, with basic algebraic identities at the bottom, analysis in the middle because its definitional prerequisites are enormous, and theorems that are famously easy to state but hard to prove, like Fermat’s Last Theorem for exponent 3, at the top.
Figure 3: Utility and interestingness are correlated. Each point is a mathlib theorem. Utility U0 , defined in Section 3.2 , is the number of lines of code saved across the library when the theorem is admitted as a premise, while interestingness I0 , defined in Section 3.1 , is the ratio between a theorem’s proof length and description length. Excluding the declarations with U0=0 gives a Spearman ρ=0.756 .
Figure 4: Training shifts generated theorems toward higher ground-truth interestingness. Our trained 27B model is consistently able to produce more interesting statements, with 20 statements per coarse area. Left: kernel densities estimator (KDE; a method that smooths the observed histogram with a kernel to give a continuous density estimate) fitted in log10 -interestingness space over all 160 outcomes per model. Right: mean ground-truth interestingness by mathematical area over the same complete cohort, shown on a logarithmic radial scale from 0.5 to 20. Colors identify the same models in both panels.
Figure 5: Interestingness training reduces overlap with existing mathlib content. For each model we take the 160 statements from Figure 4 , and judge to what degree each statement is contained within mathlib . Appendix C.2.2 gives the rubric, prompt, and protocol.
Figure 6: Iterative forward discovery builds a reusable theorem graph. Here we showcase a result from our iterative forward discovery algorithm introduced in Section 3.4 . Green shade encodes log10 total interestingness relative to P0 on a per-figure scale. The red lines trace the ancestry of the most interesting theorem introduced in P6 . More such graphs can be found in Figure 12 in Appendix C.2 .
Figure 7: Interestingness pruning is the most effective inference-time pruning criterion. Left three panels: LLM judge scores over all 6 rounds for cohort quality and diversity (Table 4 ) and the share of four-way comparisons in which each rule’s statement is ranked most interesting (Table 3 ). Right: running mean of the verified interestingness of each set Pn through P6 . More experiments are available in Appendix D .
Appendix figures & tables6 assets
Supplementary material from the paper’s appendix.
Appendix
Promotion rule
Mean Iver
Median Iver
Mean proof lines
No pruning
1.313
1.114
3.80
Random
1.556
1.175
4.39
Proof length
3.259
2.480
11.48
Interestingness
3.899
3.380
7.41
Appendix
Table 1: Quality of the promoted statements
Promotion rule
Mean Iver
Median Iver
Mean proof lines
No pruning
1.313
1.114
3.80
Random
1.461
1.271
3.74
Proof length
1.694
1.167
5.46
Interestingness
2.332
1.754
4.56
Appendix
Table 2: Verified candidates before selection.
Promotion rule
Ranked first
Ranked in top two
Mean rank ↓
No pruning
13%
34%
2.89
Random
8%
29%
2.95
Proof length
19%
64%
2.36
Interestingness
60%
73%
1.80
Appendix
Table 3: Direct policy-blinded judgment of mathematical interestingness.
Promotion rule
Quality (1–5)
Diversity (1–5)
Families per ten
Redundant
No pruning
2.50±0.53
1.30±0.48
2.60±0.97
50.0%±26.7%
Random
2.40±0.52
1.20±0.42
2.90±0.99
53.0%±18.9%
Proof length
2.60±0.52
1.30±0.48
2.90±0.74
50.0%±18.3%
Interestingness
3.40±0.52
2.10±0.32
3.50±0.71
28.0%±7.9%
Appendix
Table 4: Policy-blinded cohort judgment. Entries are mean ± sample standard deviation across the ten round-level cohorts for each promotion rule.
Figure 8: Full cross-area interestingness matrix. Each cell is the median target-wise ratio for the row area under premises from the column area versus the same-area premise condition. All premise frontiers are synchronously expanded through three rounds before new predictions are obtained. We select ten targets per area (120 total); four row areas contribute nine ratios after each excludes one non-positive same-area score. Asterisks mark 95% confidence intervals that exclude one.
Figure 9: Algebra. For monic q and r , reducing pr modulo qr equals reducing p modulo q and then multiplying by r .
We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research. Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics. This consists of an automatic pipeline that extracts lemmas from arXiv and rewrites them into self-contained statements by making all assumptions and required definitions explicit. It results in a benchmark that can be updated regularly with new problems taken directly from human mathematical research, while previous instances can be used for training without compromising future evaluations. We benchmark current state-of-the-art LLMs, which obtain around 10-15% accuracy in theorem proving (pass@1) depending on the model, showing that there is currently a large margin of progression for LLMs to reach human-level proving capabilities in a research context.
Antoine Peyronnet, Fabian Gloeckle, Amaury Hayat
1Ecole Normale Superieure de Rennes · 2Ecole des Ponts Paris · 3Korean Institute for Advanced Study
Large language models (LLMs) are increasingly capable of mathematical problem solving and can even assist with research-level proofs, yet we still lack a scalable and reproducible way to measure step-level reasoning in long proofs across diverse sources. This evaluation gap limits trustworthy AI assistance in proof-certified scientific progress. Existing evaluations often emphasize final answers or rely on costly expert grading, while end-to-end proof generation remains open-ended and hard to verify automatically. We introduce Mask-Proof, a pipeline that turns real proofs into automatically checkable masked-step tasks. It masks key formula steps, provides the necessary surrounding context, and evaluates model reconstructions with an LLM-based equivalence judge using repeated votes for stability. The resulting Mask-ProofBench contains 292 curated problems across diverse research areas. Experiments with 17 models show that reasoning-enhanced models outperform standard models by 12% to 27%. Our evaluator achieves 96.8% agreement with expert annotators, enabling faithful, reproducible, and comparable measurement of step-level mathematical reasoning. Benchmark, annotations, and code are available at https://github.com/weating/Mask-Proof.
Jierui Zhang, Siyuan Tan, Xinhang Li +8
School of Computer Science Beijing University of Posts and Telecommunications Beijing, China · Graduate College for Engineers Beijing University of Posts and Telecommunications Beijing, China · School of Mathematical Sciences Fudan University Shanghai, China +6
Recent artificial intelligence (AI) systems have shown remarkable progress in mathematical reasoning. Many existing approaches, including large language models (LLMs), draw on human prior knowledge in the form of mathematical text, code, or theorem libraries. Although these approaches are highly effective in practice, it remains an open question whether an agent can autonomously discover useful theorems without such human priors. We study this question in a formal axiomatic system by developing an agent that starts from axioms and inference rules alone and gradually grows a library of useful theorems. Concretely, we propose a self-supervised theorem-discovery algorithm that alternates between proof search and useful-theorem extraction, building a theorem library whose entries are reused as lemmas for subsequent proof search. Experiments show that the agent discovers tens of thousands of theorems and finds proofs for human-written benchmark problems, suggesting that its discoveries include theorems meaningful from a human mathematical perspective. Furthermore, the discovered theorems improve LLM proof performance when provided as prompt lemmas, indicating that they can serve as external knowledge for LLM reasoning. Our results provide evidence that useful theorems can emerge from proof search without relying on human-provided theorem libraries. More broadly, they suggest a path toward self-evolving AI systems for mathematics whose discoveries remain formally verifiable.