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

原始信息汇总

数据集概述

数据集名称

miniCTX: Neural Theorem Proving with (Long-)Contexts

数据集内容

• 类型: 定理证明
• 语言: Lean 4
• 来源: 从Mathlib提取的tactic预测示例

数据集结构

• 训练集: state_tactic_mathlib_only/state_tactic_train*
• 开发集: state_tactic_mathlib_only/state_tactic_dev*
• 测试集: state_tactic_mathlib_only/state_tactic_test*

数据集特征

• 示例内容:
  • prompt: 指令、证明状态
  • completion: tactic

版本信息

• 生成工具: ntptoolkit中的ntp-training-data和instruction_tuning.py
• 配置详情:
  • 仓库: https://github.com/leanprover-community/mathlib4
  • 提交: cf8e23a62939ed7cc530fbb68e83539730f32f86
  • Lean版本: leanprover/lean4:v4.4.0
  • 名称: mathlib
  • 导入文件: Mathlib.lean
  • 导入: Mathlib

引用信息

• 作者: Jiewen Hu, Thomas Zhu, Sean Welleck
• 标题: miniCTX: Neural Theorem Proving with (Long-)Contexts
• 年份: 2024
• 预印本: arXiv