mathlib-initiative/mathlib-const-dep

该数据集包含了Mathlib（Lean 4定理证明器的数学库）中声明的直接常量依赖信息，使用lean_scout工具从特定提交哈希（5e932f97dd25535344f80f9dd8da3aab83df0fe6）的Mathlib版本中提取。数据集遵循一个模式，包括以下字段：name（字符串类型，非空）、module（字符串类型，可为空）、deps（字符串列表类型，非空）和allowCompletion（布尔类型，非空）。数据集源自开源的Mathlib库，由leanprover-community开发，使用时建议引用Mathlib论文或仓库。

This dataset contains direct constant dependency information for declarations in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout from the Mathlib commit with hash 5e932f97dd25535344f80f9dd8da3aab83df0fe6. The dataset follows a schema with fields: name (string, non-nullable), module (string, nullable), deps (list of strings, non-nullable), and allowCompletion (boolean, non-nullable). It is derived from the open-source Mathlib library developed by the leanprover-community, and users are encouraged to cite the Mathlib paper or repository when using this dataset.