hpsearch-embed-4b-v2

The embedder of hpsearch's GPU modes: hmzprover/hpsearch-embed-4b (Qwen3-Embedding-4B, 4B parameters) LoRA-fine-tuned in two rounds on six-style queries; the weights are the average of the two rounds' merged models. Queries use hpsearch's instructions (Instruct: ...\nQuery: ); documents are a declaration's Lean statement then its NL statement.

Fine-tuning data (public, generated locally):

• six-style search queries (a Lean fragment, LaTeX, a plain-English description, a slogan, a nickname, a concrete special case) written by Qwen3-30B-A3B-Instruct-2507 for 201k declarations of the LeanSearch v2 Mathlib corpus (FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl: every definition, structure, class, instance and abbrev, and 120k theorems), from each declaration's Lean statement and its public informalization; hard negatives mined with the previous embedder (positive-aware: a negative's cosine is below 0.95 x the positive's);
• replayed public pairs of hmzprover/hpsearch-embed-4b's training set (Lean Finder and LeanSearch v2 informalizations, Mathlib signatures, LeanStateSearch's train split).

Decontamination: no declaration that is a gold of any evaluation set used by hpsearch (MathlibQR / MathlibMPR, Lean Finder, LeanStateSearch, LeanDojo, MIRB, TheoremSearch, TBPS, hmzprover; every split) is used as a positive or prompted for, by name or by statement, and every query equal (normalised) to an evaluation query is dropped.