hpsearch-embed-4b-agent

The keyword-query embedder of hpsearch's best mode: hmzprover/hpsearch-embed-4b (Qwen3-Embedding-4B) LoRA fine-tuned on agents' search queries and merged. Queries use hpsearch's instructions (Instruct: ...\nQuery: ); documents are a declaration's Lean statement then its NL statement.

Fine-tuning data:

• agent search queries from hmzprover/query-chains (keyword bags and guessed Lean names an agent typed into a theorem search tool), each paired with the declaration its chain finally found (in hmzprover/proofs); hard negatives are the lexical search hits that are not that declaration;
• replayed public pairs of the base model's own training set.

Decontamination: every chain of the hmzprover search benchmark (positive and negative chains) is excluded, and every pair whose normalised query text, or whose target's name or statement, occurs in any evaluation set used by hpsearch (MathlibQR / MathlibMPR, Lean Finder, LeanStateSearch, TheoremSearch, TBPS, hmzprover) is dropped.