hmzprover/hpsearch-embed-4b

Text embedder for hpsearch's best mode: Qwen/Qwen3-Embedding-4B fine-tuned (LoRA, merged) to retrieve Lean 4 / Mathlib declarations from natural-language queries, Lean code and proof states.

Training data (public only): Lean Finder's and LeanSearch v2's informalizations of Mathlib, Mathlib source signatures, LeanStateSearch's random train split (proof state -> premises), and queries generated from these with Qwen3-8B. Every pair whose query or target declaration occurs in an evaluation set hpsearch reports on was removed.