mathlib-initiative/mathlib-types
收藏Hugging Face2026-04-28 更新2025-12-20 收录
下载链接：
https://hf-mirror.com/datasets/mathlib-initiative/mathlib-types
下载链接
链接失效反馈官方服务：
资源简介：
该数据集包含关于Mathlib（Lean 4定理证明器的数学库）中定义的类型信息，使用lean_scout工具从特定提交（8f62007a980111b87be592665493301acbb05ea4）中提取。数据集遵循特定的schema结构，包含类型名称、模块和类型定义等字段。
This dataset contains information about types defined in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted using lean_scout. Extracted from the Mathlib commit with the following hash: 8f62007a980111b87be592665493301acbb05ea4. The dataset follows a specific schema including fields for type name, module, and type definition.
提供机构：
mathlib-initiative
