adamtopaz/mathlib_const_deps

---
pretty_name: Mathlib Const Deps
license: apache-2.0
tags:
- lean4
- theorem-proving
- lean-scout
- mathlib
---

# Mathlib Const Deps

This dataset was generated with [lean_scout](https://github.com/mathlib-initiative/lean_scout)
from the GitHub repository `adamtopaz/mathlib_const_deps` at commit `ded17d387875019ca8ee4eca1307a07e814fe565`.

## Source

- Source repository: `adamtopaz/mathlib_const_deps`
- Source commit: `ded17d387875019ca8ee4eca1307a07e814fe565`
- Hugging Face dataset repo: `adamtopaz/mathlib_const_deps`
- Dataset URL: `https://huggingface.co/datasets/adamtopaz/mathlib_const_deps`
- Generated at (UTC): `2026-03-27T20:57:40.590929Z`
- Mathlib commit used for extraction: `698d2b68b870f1712040ab0c233d34372d4b56df` (requested as `v4.29.0-rc8`)

If you use this dataset, please reference the corresponding `mathlib` / `mathlib4` revision used for extraction.

## Extraction details

- Extractor command: `const_dep`
- Target kind: `imports`
- Parquet shards: `128`
- Dry run: `False`

### Target values

- `Mathlib`

### Extractor config

```json
{}
```

### Scout command

```bash
lake run scout --command const_dep --parquet --dataDir /tmp/scout-action-cteyqymu --cmdRoot /home/runner/work/mathlib_const_deps/mathlib_const_deps --parallel 1 --numShards 128 --batchRows 1024 --config '{}' --imports Mathlib
```

## 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
```

## 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 [this link](https://github.com/leanprover-community/mathlib4/graphs/contributors).