l3lab/ntp-mathlib-instruct-context-fullproof

---
tags:
- theorem-proving
- math
- lean
configs:
- config_name: default
data_files:
- split: train
path: "ctx_full_proof_mathlib_only/ctx_full_proof_train*"
- split: dev
path: "ctx_full_proof_mathlib_only/ctx_full_proof_dev*"
- split: test
path: "ctx_full_proof_mathlib_only/ctx_full_proof_test*"
---
## [miniCTX: Neural Theorem Proving with (Long-)Contexts]()

Lean 4 full proof generation examples extracted from Mathlib.

Examples contain:
- prompt:
- instruction, preceding file content
- completion: proof

The file content has been truncated to 1024 tokens.

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

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"]
}
```

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