Let the Library Speak: Self-Advertised Method Selection for Formal Proving

Key points

• A method has prerequisites, a target, an intended action, and obligations that its use leaves to prove.1
• 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.1
• 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.1
• 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.1

Sources (1)

• [1]Let the Library Speak: Self-Advertised Method Selection for Formal Proving
  arXiv (AI, ML, NLP, CV, robotics, multi-agent) · Oct 7, 04:03 AM

  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.

Extractive summary: sentences quoted from the sources.