Source-linked AI summary
Let the Library Speak: Self-Advertised Method Selection for Formal Proving
Xiaopeng Yuan, Suijin Wang, Yanli Wang, Haibo Jin, Peng Kuang, Jerry Wang, Lijun Yu, Haohan Wang
TL;DR
The paper addresses the gap between finding related facts or proofs and deciding whether a method can be used on the current theorem. It introduces self-advertisement, which ranks methods after they propose a problem-specific use; it reports higher hit@5 than the strongest reranker on both Putnam and IMO ProofBench.
Problem
Related facts, proofs, or relevance scores do not establish how a method applies to the current goal or what conditions its use requires.
Source: §1 · pp. 1–2Method
Self-advertisement has each Method Contract propose a target, action, and required conditions for the current goal before proposals are ranked.
Source: §1 · p. 2Results
95.0% hit@5 on Putnam and 91.7% on IMO ProofBench, compared with 84.2% and 88.3% for the strongest reranker, respectively.
Source: §1 · p. 2Takeaways & Limitations
Across Putnam and IMO ProofBench, self-advertisement improves coverage of annotated methods in shortlists, including methods ranked low by lexical or embedding similarity.
Source: §6 · p. 9Shortlist coverage does not guarantee a completed proof, and the downstream comparison adds the contract as a whole rather than isolating selection from execution guidance.
Source: §6 · pp. 9–10
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
Surface similarity and relevance scores do not establish whether a mathematical method applies to a theorem. The paper proposes self-advertisement, in which candidate methods describe a problem-specific use before they are ranked.
1 INTRODUCTION
- A relevant retrieved fact or proof may not fit the goal, while a useful method may come from a problem that looks different on the surface.The selection question is what each method would do, what part of the goal it targets, and what conditions its use requires.Source: §1 · pp. 1–2
- The paper distinguishes shortlist suitability from whether a prover can complete the remaining Lean obligations.It also analyzes when similarity-only representations cannot distinguish goals that need different methods.Source: §1 · pp. 2–3
- Self-advertisement asks each of 82 Method Contracts to propose a target, action, and required conditions, demoting vague or unsupported proposals before ranking.Each contract also provides Mathlib anchors, a checked example or scaffold, and expected residual obligations.Source: §1 · pp. 2–3
- 95.0% hit@5 on Putnam and 91.7% on IMO ProofBench, compared with 84.2% and 88.3% for the strongest reranker, respectively.The reported gains concern shortlist coverage; rerankers remain more precise at rank 1 in most settings.Source: §1 · p. 2
- In the IMO ProofBench comparison, adding the selected contract as a whole does not isolate the contribution of selection, and most problems remain unsolved within the budget.Source: §1 · p. 3
2 RELATED WORK
Prior formal-proving systems retrieve facts, theorems, or worked proofs, while applicability-aware selection asks how a method could be used on the current goal. The paper represents methods with contracts and elicits problem-specific proposals for ranking.
2 RELATED WORK
- Premise selection, Mathlib search, proof retrieval, and lemma libraries provide formal facts or worked examples, whereas this paper represents a reusable mathematical method with its prerequisites and execution guidance.The contracts also record the method’s intended action and expected proof obligations.Source: §2 · p. 3
- LLM rerankers can assess retrieved candidates, but standard reranking gives a score or ordering rather than a structured account of use.Proof planning and adaptation-guided retrieval also model preconditions, effects, or adaptability; this work elicits applicability proposals from formalization methods.Source: §2 · p. 3
- Each Method Contract records prerequisites and Mathlib guidance, then proposes a target, action, and required conditions for the current goal in a batched call.Vague proposals are demoted, and the resulting shortlist presents inspectable reasons for selecting methods.Source: §2 · p. 3
3 APPLICABILITY-AWARE METHOD RETRIEVAL: A FORMAL FRAMEWORK
The framework treats method selection as a question of whether a contract can make a useful, justified step on a goal, not merely whether it looks similar. It formalizes contract applicability, scaffold guarantees, and the limits of shortlist selection.
3.1 PROBLEM AND CONTRACTS
- A contract specifies parameters, required conditions, a target and action, an execution scaffold, and residual obligations; applicability requires a correct proof to use that step downstream.Experiments use annotated reference contracts, which are applicable when the annotations are correct but may cover only some usable methods.Source: §3.1 · pp. 3–4
3.2 WHAT A CHECKED SCAFFOLD ESTABLISHES
- A checked parameterized scaffold yields a checked target proof once its required conditions and residual obligations are proved.A compiled example alone does not certify new bindings, and a proposal identifies rather than discharges the remaining work.Source: §3.2 · p. 4
3.3 SIMILARITY REPRESENTATIONS AND THE CANDIDATE-POOL CEILING
- Full goal and contract descriptions can support better expected hit@k than similarity features when distinct goals share a representation but need different shortlists.The information bound can be strict when those full descriptions distinguish the goals.Source: §3.3 · p. 4
- Any two-stage selector that reranks only a similarity-selected top-m pool has hit@k and recall@k bounded by that pool’s hit@m and recall@m for k ≤ m.A contract ranked low by the similarity filter cannot be recovered by reranking; self-advertisement judges every contract without using similarity as a filter or ranking signal.Source: §3.3 · pp. 4–5
3.4 ESTIMATING APPLICABILITY AND RANKING REGRET
- Sorting per-contract applicability scores is optimal for expected recall@k and also for expected hit@k when there is a single reference contract.With several applicable methods, near-duplicates can add little expected hit coverage, so per-contract sorting need not maximize hit@k.Source: §3.4 · pp. 5–6
- The top-k regret bound is conditional, and absolute proposal scores need not share a scale across contracts; a runoff compares leading proposals directly.The bound is not a prediction of measured gains, and only errors on contracts that are or appear to be in the top k affect the shortlist.Source: §3.4 · p. 5
- Expected hit coverage is monotone and submodular, and a greedy selector using true marginal gains achieves at least 1−1/e of optimal size-k coverage.This guarantee concerns the objective under true marginal gains.Source: §3.4 · p. 5
3.5 SELECTION AND DOWNSTREAM PROOF SUCCESS
- Better selection raises proof success when a selected contract helps the prover, while hit@k, recall@k, and rank-1 coverage reflect different ways a shortlist is used.Hit@k captures finding a usable contract within the prover’s budget; recall@k captures how much of a multi-method reference route the shortlist supplies.Source: §3.5 · p. 6
4 METHOD
The method selects contracts by asking how each could be used on the current goal, then ranks proposals by whether they commit to a checkable use. An optional runoff compares leading proposals, while the 82-contract library supplies separate selection and execution material.
4.1 SELF-ADVERTISEMENT
- Self-advertisement elicits a goal-specific target, action, required conditions, and supporting contract material for every contract before ranking.The selector reads the contracts’ selection sides; the chosen contract’s execution side is then passed to the prover.Source: §4.1 · p. 6, §4 · p. 6
- A main nomination that fails the commitment gate is demoted to a supporting role, while passing nominations rank ahead of other offers.The gate requires a concrete target and action plus supporting contract material; the tiered ranking then orders contracts by tier and score.Source: §4.1 · p. 6
4.2 RUNOFF
- The optional runoff compares leading proposals pairwise to address close or tied scores, swapping a lower contract upward when it judges that contract a better fit.It re-ranks the top q contracts in q−1 calls, using the same backbone; contracts outside the window keep their order.Source: §4.2 · pp. 6–7
4.3 CONTRACT LIBRARY
- The library contains 82 contracts from Putnam 2000–2014, each pairing selection-facing applicability descriptions with prover-facing execution guidance.Execution material includes a Lean scaffold, compiled worked instance, Mathlib declarations, required hypotheses, and residual obligations; all 82 Lean artifacts compile.Source: §4.3 · p. 7
5 EXPERIMENT
Self-advertisement leads shortlist coverage across the reported backbones and benchmarks, including cases where similarity misses annotated methods; adding a selected contract also improves proof success in the tested loop. The downstream comparison evaluates the contract as a whole, not selection alone.
5.1 SETUP
- Evaluation uses 120 Putnam 2015–2025 problems and 60 IMO ProofBench problems, labeled with methods appearing in official solutions and checked before selectors ran.The 82-contract library comes from Putnam 2000–2014, with no evaluation problem used as a contract source.Source: §5.1 · p. 7
5.2 MAIN RESULTS
- Self-advertisement leads recall@5 in all six backbone–benchmark settings and leads hit@3, hit@5, and MRR on Putnam under every backbone.On Putnam, hit@5 rises from .900 to .950 to .975 across the three backbones, while the best reranker scores .842, .842, and .858; on IMO ProofBench, runoff hit@5 is .933, .933, and .917.Source: §5.2 · pp. 7–8, Table 1 · p. 8
5.3 APPLICABILITY BEYOND SIMILARITY
- Across BM25 and three embedding retrievers, Figure 2 includes annotated methods ranked outside similarity’s top five but inside self-advertisement’s top five.Some such methods never enter rerankers’ candidate pools, so reranking cannot recover them; self-advertisement evaluates every contract and supplies a checkable target, action, and conditions.Source: §5.3 · pp. 8–9, Figure 2 · p. 9
5.4 DOWNSTREAM PROVING
- With GPT-5.6 Luna and ten Lean compilations per problem, adding the top-ranked contract raises Putnam success from 5.8% to 12.5% and IMO ProofBench success from 10.0% to 15.0%.The comparison adds the selected contract as a whole, so it does not isolate selection from contract content; most problems remain unsolved within the budget.Source: §5.4 · p. 9, Table 2 · p. 9
6 CONCLUSION
The paper concludes that selecting methods by their proposed use improves shortlist coverage and that adding the top-ranked contract increases proof success on both benchmarks. It cautions that shortlist coverage is not proof completion and that the downstream test does not isolate selection from execution guidance.
6. CONCLUSION
- Self-advertisement improves coverage of annotated methods, including methods ranked low by lexical or embedding similarity, and adding the top-ranked contract increases problems proved on both benchmarks.The downstream comparison adds the contract as a whole rather than isolating selection from its execution guidance.Source: §6 · pp. 9–10
AI USE STATEMENT
The authors used generative AI for contract construction, evaluation-label proposals, theoretical-result refinement, paper structuring, and editing.
AI USE STATEMENT
- GPT-5.6 Sol drafted contracts and proposed evaluation labels, with authors reviewing extracted methods and merges, Lean artifacts compiled, and a human checking every label.Generative AI also helped refine theoretical statements and proof sketches, suggest paper structure, and edit text for readability.Source: AI USE STATEMENT · p. 10
ETHICS STATEMENT
The work uses publicly available competition problems and official solutions, with no human subjects or personal data.
ETHICS STATEMENT
- The study uses public Putnam and IMO ProofBench problems and official solutions, with no human subjects or personal data.Source: ETHICS STATEMENT · p. 10
REPRODUCIBILITY STATEMENT
The paper documents its checked execution environment and defines the selection metrics used to evaluate shortlists.
REPRODUCIBILITY STATEMENT
- Every execution-side artifact was checked using Lean v4.27.0 and Mathlib commit a3a10db.Appendix C.2 lists the pinned environment, and Figure 3 shows an example contract.Source: REPRODUCIBILITY STATEMENT · p. 10
- The tiered ranking breaks ties by contract identifier, making it deterministic given the model outputs.Source: REPRODUCIBILITY STATEMENT · p. 10
A SELECTION METRICS
- hit@k measures whether a shortlist contains an annotated method, recall@k its coverage of annotated methods, and MRR how early the first appears.Source: A SELECTION METRICS · p. 13
A.1 MULTI-METHOD COVERAGE
Expected hit@k is a monotone submodular coverage objective with a greedy approximation guarantee, distinct from the additive expected-recall objective.
A.1 MULTI-METHOD COVERAGE
- Greedy selection using true marginal gains achieves at least 1−(1−1/k)^k, and therefore at least 1−1/e, of optimal expected hit@k coverage.Source: §A.1 · p. 13
- Expected hit@k is monotone and submodular because adding a contract has diminishing marginal benefit as the shortlist grows.Source: §A.1 · p. 14
- Expected recall@k is additive and optimized by sorting per-contract scores, while expected hit@k is submodular and can favor diversity.The implementation sorts per-contract scores; the paper does not run the diversity-aware greedy procedure for multi-method hit@k.Source: §A.1 · p. 14
B PROOFS
The proofs establish conditional scaffold soundness, an information bound for similarity representations, a candidate-pool ceiling, and a top-k ranking-regret bound.
B PROOFS
- The appendix supplies proofs for Propositions 1–3, Corollary 1, and Proposition 4.Source: B PROOFS · p. 14
B.1 CONDITIONAL SCAFFOLD SOUNDNESS
- A checked scaffold yields a checked proof of its target only after its precondition and residual obligations are proved.This guarantee concerns reuse, not whether the binding is useful or advances the proof.Source: §B.1 · p. 14
B.2 INFORMATION BOUND
- Full goal descriptions can support higher expected hit@k than similarity representations; the inequality is strict when distinct goals sharing a representation require different shortlists.The construction gives Vk(X) = 1 and Vk(T) = k/n for k < n.Source: §B.2 · p. 15
B.3 CANDIDATE-POOL CEILING
- For cutoffs k ≤ m, a two-stage selector’s hit@k and recall@k cannot exceed what its similarity-based top-m candidate pool contains.Source: §B.3 · p. 15
B.4 TOP-k RANKING REGRET
- The top-k regret bound depends on shortlist disagreement; estimates outside the leading contracts may be arbitrarily poor.The monotone rescaling need only be close to the true scores on at most 2k contracts.Source: §B.4 · p. 16
C.1 A METHOD CONTRACT
Figure 3 presents an abridged Method Contract, separating what the selector reads from what the prover executes. The associated artifacts and proving experiments use a pinned Lean and Mathlib environment.
C.2 LEAN ENVIRONMENT
- All contract checks and proving experiments use Lean v4.27.0 and a pinned Mathlib commit, with a startup check preventing revision drift.The table lists pinned dependencies; the text gives the full Mathlib commit.Source: §C.2 · p. 16, Table 3 · p. 16
D.1 DOWNSTREAM
- The downstream comparison uses a 10-compilation budget for all arms except pass@20, which draws 20 samples and receives twice the budget.The setup compares AxProverBase with a version whose initial prompt adds the top-ranked self-advertised contract.Source: §D.1 · p. 16
C.1 A METHOD CONTRACT
- Figure 3 separates the contract’s selection side, read by the selector, from its execution side, received by the prover; auxiliary fields are omitted.The displayed Lean code compiles in the pinned environment.Source: §C.1 · p. 16, Figure 3 · p. 17