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

arXiv:2610.09401v1 Announce Type: new Abstract: 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