l3lab/ntp-mathlib

---
tags:
- theorem-proving
- math
- lean
---

## [miniCTX: Neural Theorem Proving with (Long-)Contexts]()

Lean 4 tactic prediction examples extracted from Mathlib.

These examples have **not** been formatted for instruction tuning (including data splits).

Please see `l3lab/ntp-mathlib-instruct-*` for datasets with instruction tuning examples.

### Version
Generated using `ntptoolkit`'s `ntp-training-data`.

It used the following config for `ntp-training-data`:

```json
{
"repo": "https://github.com/leanprover-community/mathlib4",
"commit": "cf8e23a62939ed7cc530fbb68e83539730f32f86",
"lean": "leanprover/lean4:v4.4.0",
"name": "mathlib",
"import_file": "Mathlib.lean",
"imports": ["Mathlib"]
}
```

### Example usage:

```bash
ds = datasets.load_dataset('l3lab/ntp-mathlib')

print(len(ds['train']))
# ==> 307049
```

### Format:
```json
{
'state': 'proof state',
'srcUpToTactic': 'source up to tactic invocation',
'nextTactic': 'tactic',
'declUpToTactic': 'declariation up to tactic invocation',
'declId': 'unique ID for declaration',
'decl': 'declaration',
'file_tag': 'file ID'
}
```

#### Citation

Please cite:
```
@misc{hu2024minictx,
title={miniCTX: Neural Theorem Proving with (Long-)Contexts},
author={Jiewen Hu and Thomas Zhu and Sean Welleck},
year={2024},
eprint={2408.03350},
archivePrefix={arXiv},
primaryClass={cs.AI},
url={https://arxiv.org/abs/2408.03350},
}
```