FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl
收藏Hugging Face2026-05-18 更新2026-05-31 收录
下载链接：
https://hf-mirror.com/datasets/FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl
下载链接
链接失效反馈官方服务：
资源简介：
LeanSearch v2 — Mathlib v4.28.0-rc1语料库（JSONL格式）是一个数据集，其中每条记录对应Mathlib v4.28.0-rc1（一个数学库版本）中的一个声明。该数据集使用LLM（大语言模型）生成的非正式描述作为嵌入输入，这些描述是构建配套cuVS索引的原始来源。数据集旨在支持定理证明和检索任务，与Lean4和mathlib标签相关。
LeanSearch v2 — Mathlib v4.28.0-rc1 corpus (JSONL) is a dataset with one record per Mathlib v4.28.0-rc1 declaration, using LLM-generated informal descriptions as the embedding input — the raw source from which the companion cuVS index is built.
提供机构：
FrenzyMath
