CoolFace
Datasetpublic

FrenzyMath/lsv2-mathlib-v4.28.0-rc1-cuvs

LeanSearch v2 — Mathlib v4.28.0-rc1 cuVS index Pre-built cuVS CAGRA index over every Mathlib v4.28.0-rc1 declaration, encoded with Qwen3-Embedding-8B; drops directly into the LeanSearch v2 serving pipeline (cuvs_index.bin + metadata.pkl + texts.pkl). Code: https://github.com/frenzymath/LeanSearch-v2 Paper: https://arxiv.org/abs/2605.13137

sourceHugging Faceapache-2.0updated 4mo agoView on Hugging Face
0likes78downloads
Dataset Card

LeanSearch v2 — Mathlib v4.28.0-rc1 cuVS index

Pre-built cuVS CAGRA index over every Mathlib v4.28.0-rc1 declaration, encoded with Qwen3-Embedding-8B; drops directly into the LeanSearch v2 serving pipeline (cuvs_index.bin + metadata.pkl + texts.pkl).

  • —Code: <https://github.com/frenzymath/LeanSearch-v2>
  • —Paper: <https://arxiv.org/abs/2605.13137>