l3lab/ntp-mathlib-instruct-st

---
tags:
- theorem-proving
- math
- lean
configs:
- config_name: default
data_files:
- split: train
path: "state_tactic_mathlib_only/state_tactic_train*"
- split: dev
path: "state_tactic_mathlib_only/state_tactic_dev*"
- split: test
path: "state_tactic_mathlib_only/state_tactic_test*"
---

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

Lean 4 tactic prediction examples extracted from Mathlib.

Examples contain:
- prompt:
- instruction, proof state
- completion: tactic

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

tags:
- theorem-proving
- math
- lean
configs:
- config_name: default
data_files:
- split: train
path: "state_tactic_mathlib_only/state_tactic_train*"
- split: dev
path: "state_tactic_mathlib_only/state_tactic_dev*"
- split: test
path: "state_tactic_mathlib_only/state_tactic_test*"
---

## [miniCTX：基于（长）上下文的神经定理证明（Neural Theorem Proving）]()

从Mathlib中提取的Lean4策略预测（tactic prediction）示例。

示例包含：
- prompt:
- 指令（instruction）
- 证明状态（proof state）
- completion: 策略（tactic）

### 版本
使用`ntptoolkit`的`ntp-training-data`和`instruction_tuning.py`生成。

它使用了以下`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"]
}

#### 引用

请引用：

@misc{hu2024minictx,
title={miniCTX：基于（长）上下文的神经定理证明（Neural Theorem Proving）},
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},
}