A retrieval-tuned embedding model for mathematical text. Fine-tuned from on mathlib4 concepts via multi-view contrastive learning. On MELD — a benchmark of mathematical statements paired across radically different presentations (e.g., set-theoretic vs. category-theoretic phrasings of the same theorem) — MathLeap-Qwen-8B achieves MMR 0.43, beating its base Qwen3-Embedding-8B (0.32, +0.11) and the retrieval-specialized Octen-Embedding-8B (0.42). Each concept has up to four parallel representations: - nlinformal: informal natural-language description (all concepts) - nlinformal2: LLM-generated NL rephrasing (~85% of concepts) - leantype: Lean 4 type signature - leansignature: full Lean 4…