---
title: Lean-Github
canonical_url: "https://www.modelscope.cn/datasets/Shanghai_AI_Laboratory/Lean-Github"
md_url: "https://www.modelscope.cn/datasets/Shanghai_AI_Laboratory/Lean-Github.md"
repository: Shanghai_AI_Laboratory/Lean-Github
last_updated: 2025-05-29
license: "Apache License 2.0"
storage_size: "41 MB"
downloads: 678
stars: 0
---

# Lean-Github

> Lean-Github - Shanghai_AI_Laboratory 在 ModelScope 开源的数据集。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…

Shanghai_AI_Laboratory/Lean-Github 是 ModelScope 魔搭社区上的数据集，存储大小 41 MB，采用 Apache License 2.0 许可。

- **Repository**: Shanghai_AI_Laboratory/Lean-Github
- **License**: Apache License 2.0
- **Storage size**: 41 MB
- **Downloads**: 678
- **Stars**: 0
- **Last updated**: 2025-05-29

Source: https://www.modelscope.cn/datasets/Shanghai_AI_Laboratory/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}, 
}
```