LLM-based formal provers can retrieve relevant lemmas and prior proofs, but relevance alone does not say whether a mathematical method can be used on the current theorem. A method has prerequisites, a target, an intended action, and obligations that its use leaves to prove. Methods that look equally related to a theorem may therefore differ substantially in whether they offer a plausible next step. We formulate this as an applicability-aware method-selection problem and introduce self-advertisement: before candidates are ranked, a model generates a problem-specific proposal for each one, stating what part of the goal it targets, what action it would take, and what conditions that action requires. We organize 82 reusable methods from Putnam 2000-2014 as Method Contracts, which pair applicability descriptions with Mathlib anchors, a checked example or scaffold, and expected proof obligations. A single batched call elicits proposals across the library; vague or unsupported proposals are demoted, yielding a ranked shortlist accompanied by inspectable claims about each candidate's use. We analyze when similarity-based representations cannot distinguish methods with different applicability, how errors in applicability estimates affect shortlist quality, and what a checked scaffold guarantees under its stated assumptions. Against lexical, embedding, and embedding-plus-LLM reranking baselines, self-advertisement achieves 95.0% hit@5 on Putnam 2015-2025, compared with 84.2% for the strongest reranker. On IMO ProofBench, it achieves 91.7% compared with 88.3%. These results indicate improved coverage of annotated methods in the retrieved shortlists, particularly on Putnam.
Figures & tables
Figure 1: Self-advertised method selection. Given a theorem, a single model call asks every contract in the library how it would be used. A gate demotes proposals that are vague (Pigeonhole) or unsupported (AM-GM, since ai≥0 is not given), and the top-ranked contract (Cauchy–Schwarz) goes to the prover. Inset: similarity retrieval would pick AM-GM instead.
Putnam 2015–2025 ( n=120 )
IMO ProofBench ( n=60 )
Selector
hit@1
hit@3
hit@5
R@3
R@5
MRR
hit@1
hit@3
hit@5
R@3
R@5
MRR
No LLM
Random
.058
.158
.225
.038
.053
.141
.083
.167
.267
.041
.076
.158
BM25
.208
.400
.508
.104
.140
.337
.183
.333
.400
.103
.147
.295
TF-IDF cosine
.267
.442
.525
.118
.144
.382
.233
.367
.433
.135
.165
.318
OpenAI emb-3-small
.325
.533
.683
.157
.229
.463
.267
.517
.617
.213
.263
.411
Table 1: Shortlist quality against annotated reference contracts. hit@ k : fraction of problems whose top- k list contains at least one annotated contract. R@ k : fraction of annotated contracts that appear in the top k . Bold: best within each LLM block; ties are all bolded.
Figure 2: Each dot is one problem; y is the rank of its highest-ranked annotated method under self-advertisement (GPT-5.6 Luna, shared across panels), and x is that method’s rank by problem–method similarity under the panel’s retriever. Dashed lines mark the top five; the shaded region holds methods that similarity ranks outside its top five but self-advertisement places inside.
Putnam 2015–2025
IMO ProofBench
Method
ALG
ANA
DISC
All
Basic
Adv.
All
Base
0.0
0.0
0.0
0.0
3.3
0.0
1.7
pass@20
2.3
0.0
0.0
0.8
3.3
0.0
1.7
APOLLO
4.5
0.0
2.2
2.5
13.3
0.0
6.7
AxProverBase
9.1
3.3
4.3
5.8
20.0
0.0
10.0
+ Self-adv. contract (ours)
9.1
10.0
17.4
12.5
26.7
3.3
15.0
Table 2: Downstream proving success rate (%) with GPT-5.6 Luna under a budget of 10 Lean compilations per problem.
Appendix figures & tables1 asset
Supplementary material from the paper’s appendix.
Appendix
Figure 3: An example Method Contract. The selector reads the selection side; the prover receives the execution side. All Lean code compiles in the pinned environment (Appendix C.2 ).
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.
Niket Patel, Ahmad Rammal, Amaury Hayat +2
New York University · CERMICS, ENPC, Institut Polytechnique de Paris
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
LLMs have recently achieved strong results on formal proving benchmarks. However, existing evaluations remain heavily concentrated on competition-style problems and often fail to capture how models behave on longer, more dependency-rich mathematical developments. We introduce TheoremBench, a Lean4 benchmark designed to evaluate theorem provers beyond contest settings. The benchmark is built from nearly one hundred classical theorems and is released in two complementary forms: a plain main version containing one target theorem per instance, and a premised version that expands each theorem into a structured family of related proving tasks consisting of the main theorem together with automatically extracted supporting subtheorems. This design enables evaluation of not only whether the final theorem was proved from scratch, but also of partial progress through the internal proof structure of a theorem. Our experiments show that explicit premises substantially improve performance for Lean4-capable prover models. To provide a comprehensive evaluation, we introduce theorem-level coverage and token-efficiency metrics that expose qualitative differences in proof behavior. The results show that current provers remain strongly biased toward easy subtheorems and often solve theorems through long and inefficient tactic traces rather than compact proof plans. TheoremBench therefore provides a more fine-grained view of formal reasoning ability and highlights the importance of structural benchmark design for evaluating Lean4 theorem provers.
QuocViet Pham, Elvir Karimov, Andrey Galichin +1
Skolkovo Institute of Science and Technology · HSE University · Sberbank +1