FrenzyMath/lsv2-mathlib-v4.28.0-rc1-cuvs
收藏Hugging Face2026-05-18 更新2026-06-14 收录
下载链接：
https://hf-mirror.com/datasets/FrenzyMath/lsv2-mathlib-v4.28.0-rc1-cuvs
下载链接
链接失效反馈官方服务：
资源简介：
LeanSearch v2 — Mathlib v4.28.0-rc1 cuVS索引是一个预构建的cuVS CAGRA索引，覆盖了Mathlib v4.28.0-rc1中的每个声明，并使用Qwen3-Embedding-8B模型进行编码。该数据集可以直接集成到LeanSearch v2服务管道中，包括cuvs_index.bin、metadata.pkl和texts.pkl文件，用于检索和定理证明任务。
LeanSearch v2 — Mathlib v4.28.0-rc1 cuVS Index is a pre-built cuVS CAGRA index that covers every declaration in Mathlib v4.28.0-rc1, and is encoded using the Qwen3-Embedding-8B model. This dataset can be directly integrated into the LeanSearch v2 service pipeline, and contains cuvs_index.bin, metadata.pkl, and texts.pkl files intended for retrieval and theorem proving tasks.
提供机构：
FrenzyMath
