erbacher/LeanRank-data
收藏Hugging Face2025-09-29 更新2025-10-25 收录
下载链接：
https://hf-mirror.com/datasets/erbacher/LeanRank-data
下载链接
链接失效反馈官方服务：
资源简介：
LeanRank数据集包含了从mathlib4仓库中提取的定理证明数据。数据通过LeanDojo工具包生成，来源于mathlib4库的特定版本，对应于Git提交哈希c211948581bde9846a99e32d97a03f0d5307c31e。该数据集旨在用于检索和排名任务，尤其是前提选择。每个条目代表一个形式证明中的状态，包含上下文、一个积极前提和几个消极前提。
The LeanRank dataset contains theorem-proving data extracted from the mathlib4 repository. The data was generated using the LeanDojo toolkit from a specific version of the mathlib4 library, corresponding to the Git commit hash c211948581bde9846a99e32d97a03f0d5307c31e. The dataset is designed for retrieval and ranking tasks, particularly premise selection. Each entry represents a state in a formal proof, including the context, a positive premise, and several negative premises from the same mathlib file.
提供机构：
erbacher
