Datasetpublic

mathlib-initiative/mathlib-const-dep

Mathlib Constant Dependencies This dataset contains direct constant dependency information for declarations in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout. Extracted from the Mathlib commit with the following hash. 0df444a360eaa60ab8c11dca51a86af692955474 The dataset follows this schema: fields: - type: datatype: string nullable: false name: name - type: datatype: string nullable: true name: module - type: item:… See the full description on the dataset page: https://huggingface.co/datasets/mathlib-initiative/mathlib-const-dep.

sourceHugging Faceapache-2.0updated 19d agoView on Hugging Face

0likes1.1kdownloads

Dataset Card

Mathlib Constant Dependencies

This dataset contains direct constant dependency information for declarations in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout.

Extracted from the Mathlib commit with the following hash.

0df444a360eaa60ab8c11dca51a86af692955474

The dataset follows this schema:

yaml

fields:
- type:
    datatype: string
  nullable: false
  name: name
- type:
    datatype: string
  nullable: true
  name: module
- type:
    item:
      datatype: string
    datatype: list
  nullable: false
  name: deps
- type:
    datatype: bool
  nullable: false
  name: allowCompletion

Attribution

This dataset is derived from Mathlib, an open-source mathematical library developed by the leanprover-community. If you use this dataset, please cite the Mathlib paper or the Mathlib repository.

A full list of Mathlib contributors is available at: https://github.com/leanprover-community/mathlib4/graphs/contributors