hpsearch-embed-8b-nl

The embedder hpsearch's GPU modes use for English sentences and questions ("Is there a lemma in Mathlib that ...", "How can I prove ... in Lean?"): Qwen3-Embedding-8B (8B parameters) LoRA-fine-tuned (r=32, one epoch, contrastive with in-batch and one hard negative) on 398k query/declaration pairs. Queries use hpsearch's instructions (Instruct: ...\nQuery: ); documents are a declaration's Lean statement then its NL statement (half the user-question pairs show the Lean statement only).

Fine-tuning data (public, generated locally):

• user-question queries written by Qwen3-30B-A3B-Instruct-2507 for about 450k declarations of the LeanSearch v2 Mathlib corpus (FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl), four styles (asking whether Mathlib has a result, a proof task, a broad Zulip-like discussion, a user stuck in a proof), from each declaration's Lean statement and its public informalization; hard negatives mined with hpsearch-embed-4b-v2 (positive-aware);
• replayed six-style queries and public pairs of hmzprover/hpsearch-embed-4b-v2's training set.

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