Lean-Github

We release Lean-Github and InternLM2-Step-Prover with 29K theorems compiled from 100+ Lean 4 repos and a 7B models fine-tuned on Lean-Github and Lean-Workbook with SOTA performance on MiniF2F-test (54.5%), ProofNet (18.1%), and Putnam (5 problems).
[🤗Dataset](https://huggingface.co/datasets/internlm/Lean-Github) [🤗Model](https://huggingface.co/internlm/internlm2-step-prover) [📑 Paper](https://arxiv.org/abs/2407.17227) [📖 README](https://github.com/InternLM/InternLM-Math/blob/main/lean-github/README.md)

# Citation and Tech Report
```
@misc{wu2024leangithubcompilinggithublean,
title={LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover},
author={Zijian Wu and Jiayu Wang and Dahua Lin and Kai Chen},
year={2024},
eprint={2407.17227},
archivePrefix={arXiv},
primaryClass={cs.AI},
url={https://arxiv.org/abs/2407.17227},
}
```

本研究发布了Lean-Github与InternLM2-Step-Prover两项成果：前者为从100余个Lean 4代码仓库中编译得到的包含29000条定理的数据集，后者则是基于Lean-Github与Lean-Workbook数据集微调得到的70亿参数（7B）模型，在MiniF2F测试集（准确率54.5%）、ProofNet基准（准确率18.1%）以及Putnam竞赛（5道题目）上取得了当前最优（State-of-the-Art，SOTA）性能。
[🤗数据集](https://huggingface.co/datasets/internlm/Lean-Github) [🤗模型](https://huggingface.co/internlm/internlm2-step-prover) [📑 论文](https://arxiv.org/abs/2407.17227) [📖 说明文档](https://github.com/InternLM/InternLM-Math/blob/main/lean-github/README.md)

# 引用与技术报告

@misc{wu2024leangithubcompilinggithublean,
title={LEAN-GitHub: 编译GitHub上的Lean仓库以构建通用Lean定理证明器},
author={Zijian Wu and Jiayu Wang and Dahua Lin and Kai Chen},
year={2024},
eprint={2407.17227},
archivePrefix={arXiv},
primaryClass={cs.AI},
url={https://arxiv.org/abs/2407.17227},
}