Summary (Overview)

• Novel problem formulation: The paper introduces "applicability-aware method selection" for formal theorem proving, distinguishing it from similarity-based retrieval. A method may look relevant to a theorem but not be applicable due to unmet prerequisites or mismatched targets.
• Self-advertisement mechanism: Before ranking, a model generates a problem-specific proposal for each candidate method, stating what part of the goal it targets, what action it would take, and what conditions that action requires. Vague or unsupported proposals are demoted.
• Method Contracts library: The authors construct 82 reusable methods from Putnam 2000–2014 as structured contracts pairing applicability descriptions with Mathlib anchors, checked Lean scaffolds, and expected proof obligations.
• Strong empirical results: Self-advertisement achieves 95.0% hit@5 on Putnam 2015–2025 (vs. 84.2% for the strongest reranker) and 91.7% on IMO ProofBench (vs. 88.3%), with coverage gains coming largely from methods that do not look similar to the problem.
• Downstream proof improvement: Adding the top-ranked contract to an Ax-Prover-style proof loop raises the proportion of proved problems from 5.8% to 12.5% on Putnam and from 10.0% to 15.0% on IMO ProofBench.

Introduction and Theoretical Foundation

Background and Motivation

Large language models can propose high-level approaches to mathematical problems, and recent theorem-proving systems use them to generate Lean code, check it, and revise it in response to feedback. However, before a prover can use a mathematical method, it must decide whether that method offers a useful step for the current goal. A suggestion such as "use induction" leaves open what to induct on, which part of the goal the method would address, and what remains to be proved.

Existing systems support formal proof construction at several levels:

• Premise selection and Mathlib search provide relevant definitions and theorems
• Proof retrieval offers examples of how related problems were solved
• Verifier-guided loops use Lean's errors to revise failed attempts

The central problem: surface similarity does not establish applicability. A retrieved inequality may require nonnegativity that has not been established, while a useful method may come from a problem that looks quite different on the surface.

Theoretical Framework

The paper formalizes the problem using the following structure. Let $g$ be a Lean goal with local context $\Gamma$, and let $\mathcal{C}$ be a finite library of method contracts. A contract $c$ has:

• Parameters $x_c$
• Required conditions $\mathrm{Pre}_c(x_c)$
• A target statement $G_c(x_c)$ with an intended action
• An execution scaffold $S_c$
• Residual obligations $\mathrm{Obl}_c(x_c)$

A selector receives $g$, $\Gamma$, and the contract descriptions, and returns an ordered list $\pi(g) = (c_1, \ldots, c_{|\mathcal{C}|})$.

Key definitions:

• Semantic applicability: A contract $c$ is applicable to $g$ if some correct proof of $g$ contains a step that instantiates $c$ at a binding $\theta$
• Annotated set $A(g) \subseteq \mathcal{C}$: reference contracts used in official solutions; when correct, $A(g) \subseteq \mathrm{App}(g)$

Methodology

Self-Advertisement

Self-advertisement replaces the question of how closely a contract resembles the goal with the question of how the contract would be used. In a single model call, the model reads the goal, its local context, and the selection-facing description of every contract, and returns a proposal for each contract. The proposal of contract $c$ commits to:

• A target $t_c$, which instantiates $G_c(\hat{\theta})$ in terms of the goal's own objects
• An action $a_c$
• Required facts $\mathrm{Pre}_c$, which instantiate $\mathrm{Pre}_c(\hat{\theta})$
• Verified material $\sigma_c$ from the contract that supports this commitment
• Whether the contract offers itself ($o_c$), its role $\rho_c \in \{\text{main}, \text{support}\}$, and an applicability score $\hat{s}_c$

Commitment Gate

A main nomination must pass the commitment gate:

$$\text{Gate}(c) = o_c \wedge \text{Spec}(t_c) \wedge \text{Spec}(a_c) \wedge (\sigma_c eq \varnothing)$$

where Spec holds when a target or action names a concrete object of the goal rather than a generic phrase. A main nomination that fails the gate is demoted to a supporting role.

Runoff

The runoff re-ranks the top $q$ contracts by comparing their proposals directly. In one pass of $q-1$ calls from the top of the window down, the model sees each contract, the contract above it, and the proposal that contract wrote earlier; it writes a proposal for the lower contract and judges whether it fits the proof better, swapping if so.

Contract Library Construction

The 82 contracts are built in three steps using GPT-5.6 Sol:

1. Extraction: Extract methods from Putnam 2000–2014 reference solutions; authors review every extraction and merge
2. Drafting: Draft both selection-facing and execution-facing sides of each contract
3. Compilation: Every Lean artifact compiled with Lean v4.27.0 and Mathlib; all 82 contracts pass

Empirical Validation / Results

Main Results

Table 1 shows shortlist quality across all settings (excerpt):

Key findings:

• Self-advertisement attains the highest recall@5 in all six backbone–benchmark settings
• On Putnam, it leads at hit@3, hit@5, and MRR under every backbone
• Rerankers remain more precise at rank 1 in most settings; the runoff narrows this gap (Putnam hit@1 rises from 62.5% to 72.5% with GPT-5.6 Terra, above the strongest reranker at 67.5%)

Applicability Beyond Similarity

Figure 2 demonstrates that many annotated methods that self-advertisement places in its top five are ranked outside the top five by similarity retrievers—often so dissimilar that they never enter rerankers' candidate pools, making them unrecoverable by any reranking backbone.

Downstream Proving

Table 2 reports proof success with GPT-5.6 Luna under a budget of 10 Lean compilations per problem:

Adding the top-ranked contract more than doubles success on Putnam and raises it by 50% on IMO ProofBench.

Theoretical Results

Proposition 1 (Conditional scaffold soundness): A Lean-checked scaffold of type

$$S_c: \forall x_c, \operatorname{Pre}_c(x_c) \to \operatorname{Obl}_{c,1}(x_c) \to \dots \to \operatorname{Obl}_{c,r}(x_c) \to G_c(x_c)$$

yields a checked proof of $G_c(\theta)$ for any binding $\theta$ whose required conditions and obligations have checked proofs.

Proposition 2 (Information bound): If $T = \phi(X)$, then $V_k(X) \geq V_k(T)$. The inequality can be strict when distinct goals share the same similarity representation but require different shortlists.

Corollary 1 (Candidate-pool ceiling): A two-stage selector's hit@k and recall@k are bounded by the first-stage selector's hit@m and recall@m, regardless of the second-stage model.

Proposition 3 (Top-k ranking regret): If scores $\hat{s}_c$ are within $\epsilon$ of true weights $w_c(x)$ under an increasing transformation, then expected recall regret is bounded: $R_x(S_k^*) - R_x(\hat{S}_k) \leq 2k\epsilon$.

Proposition 4 (Multi-method coverage): Expected hit@k is monotone and submodular; a greedy selector attains at least $1 - 1/e$ times the optimum.

Theoretical and Practical Implications

Theoretical Implications

1. Similarity is insufficient for method selection: Proposition 2 formally shows that similarity-only selectors can assign identical representations to goals requiring different methods, creating an information-theoretic ceiling.

2. Two-stage reranking has inherent limits: Corollary 1 proves that rerankers operating on similarity-filtered candidate pools cannot recover methods the similarity stage missed—a structural bound, not a model limitation.

3. Different metrics need different rules: Expected recall@k is additive (sorting by $w_c$ is optimal), while expected hit@k is submodular (diversity-aware selection matters when multiple methods apply).

Practical Implications

1. Inspectable selection: Unlike rerankers that output only scores, self-advertisement produces concrete, checkable claims about each candidate's use (target, action, conditions), enabling human inspection and verification.

2. Library design matters: The Method Contract structure separates selection-facing descriptions from execution guidance, allowing the same library to serve both selection and proving stages.

3. Downstream proof improvement: The doubling of proof success on Putnam demonstrates that better method selection translates into more completed proofs within fixed compute budgets.

Conclusion

The paper presents self-advertisement, a method-selection approach that asks each Method Contract to propose a target, action, and required conditions for the current theorem. Key takeaways:

1. Coverage gains: Self-advertisement improves coverage of annotated methods in shortlists, including methods ranked low by lexical or embedding similarity, across Putnam and IMO ProofBench.

2. Downstream impact: Adding the top-ranked contract to a fixed-budget proof loop increases the number of problems proved on both benchmarks.

3. Two clear limits: Shortlist coverage does not guarantee a completed proof, and the downstream comparison adds the contract as a whole rather than isolating selection from execution guidance.

Future directions: Separate the contributions of selection vs. execution guidance, and help provers carry promising method proposals through to verified proofs.