mathlib-initiative/mathlib-const-dep

---
license: apache-2.0
language:
- en
tags:
- lean4
- mathlib
- theorem-proving
- formal-mathematics
pretty_name: Mathlib Constant Dependencies
---

# Mathlib Constant Dependencies

This dataset contains direct constant dependency information for declarations in [Mathlib](https://github.com/leanprover-community/mathlib4/tree/5e932f97dd25535344f80f9dd8da3aab83df0fe6), the mathematical library for the Lean 4 theorem prover, extracted with [lean_scout](https://github.com/mathlib-initiative/lean_scout).

Extracted from the Mathlib commit with the following hash.
```
5e932f97dd25535344f80f9dd8da3aab83df0fe6
```

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](https://github.com/leanprover-community/mathlib4), an open-source mathematical library developed by the [leanprover-community](https://leanprover-community.github.io/). If you use this dataset, please cite the [Mathlib paper](https://doi.org/10.1145/3372885.3373824) or the [Mathlib repository](https://github.com/leanprover-community/mathlib4).

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