l3lab/ntp-mathlib-instruct-context

---
tags:
- theorem-proving
- math
- lean
configs:
- config_name: default
data_files:
- split: train
path: "with_context_mathlib_only/with_context_train*"
- split: dev
path: "with_context_mathlib_only/with_context_dev*"
- split: test
path: "with_context_mathlib_only/with_context_test*"
---
## [miniCTX: Neural Theorem Proving with (Long-)Contexts]()

Lean 4 tactic prediction examples extracted from Mathlib.

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

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

---
标签：
- 定理证明（theorem-proving）
- 数学（math）
- Lean（Lean）
数据集配置：
- 配置名称：default
数据文件：
- 训练集（train）：路径为`with_context_mathlib_only/with_context_train*`
- 验证集（dev）：路径为`with_context_mathlib_only/with_context_dev*`
- 测试集（test）：路径为`with_context_mathlib_only/with_context_test*`
---

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

从Mathlib库中提取的Lean 4 策略预测示例。

示例包含以下内容：
- 提示词（prompt）：
- 指令、前置文件内容、证明状态
- 指令、证明状态
- 补全项（completion）：策略

文件内容已被截断至1024个Token（Token）。

### 版本信息
本数据集由`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"]
}

#### 引用格式
请引用如下文献：
bibtex
@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},
}