license: apache-2.0
base_model: Qwen/Qwen3-Embedding-0.6B
library_name: sentence-transformers
pipeline_tag: sentence-similarity
tags:
- lean4
- mathlib
- retrieval
- premise-selection
hpsearch-embed-fast
The query side of hpsearch's mode fast for proof states and Lean
expressions: the first 8 layers of Qwen3-Embedding-0.6B and a linear map to 2,560 dimensions, trained so that a
query lands next to the hmzprover/hpsearch-embed-4b-v2
vectors of what it asks for (documents keep their hpsearch-embed-4b-v2 vectors; pairs_with names it). About
3 ms per query on an A100 with CUDA-graph replay.
Queries: a proof state (prompt Instruct: Given a Lean 4 proof state, retrieve Mathlib lemmas that help prove its goal\nQuery: , goal first), its goal alone, or a Lean expression (a statement's conclusion or Pi type; prompt
Instruct: Given Lean 4 code, retrieve the Mathlib declaration it states or names\nQuery: ). Full softmax over the
frozen document vectors, plus distillation (KL over the documents) from hpsearch-embed-4b-v2's own query side on
expressions. Lean expressions come from the training corpora's own statements (no evaluation gold among them).
Training data
Public training splits only:
- LeanDojo Benchmark 4 (v10)
random/train: each traced tactic's state paired with the premises it uses; - LeanStateSearch (
ruc-ai4math/mathlib_handler_benchmark_410)random/train, the same way. For part of the states, a one-to-three-sentence English description of the next step (written by an LLM from the state and the tactic) follows the state, as in Lean Finder's "augmented" proof states.
Decontamination (strict): a state is dropped when its theorem is in a held-out split or is the theorem of any evaluation query, when its text equals any evaluation query, or when its goal equals the goal of any proof-state evaluation query; a premise is dropped when its name or statement is a gold of any evaluation (MathlibQR/MPR, Lean Finder, LeanStateSearch, TBPS, TheoremSearch, MIRB, LeanDojo, hpsearch's own); such premises are also left out of the contrastive softmax. Kept: 147,412 states (89,719 LeanDojo, 57,693 LeanStateSearch), 89,298 premises.