Recently, large language models have presented promising results in aiding formal mathematical reasoning. However, their performance is restricted due to the scarcity of formal theorem-proving data, which requires additional effort to be extracted from raw formal language corpora. Meanwhile, a significant amount of human-written formal language corpora remains underutilized. To address this issue, we propose LEAN-GitHub, a dataset consisting of large-scale formal data extracted from almost all Lean 4 repositories on GitHub. After fine-tuning InternLM-math-plus on this dataset, our model achieved accuracies of 48.8% with a single pass and 54.5% with 64 passes on the Lean 4 miniF2F test, surpassing state-of-the-art method at 52%. And it also achieves state-of-the-art on two other Lean 4 benchmarks (ProofNet and Putnam) targeting different fields/levels of math. These results demonstrate that our proposed dataset is beneficial for formal reasoning on a wide range of math topics. We open-source our model at https://GitHub. com/InternLM/InternLM-Math and our data at https://huggingface.co/ datasets/InternLM/Lean-GitHub

本研究解决了形式定理证明数据匮乏的问题，通过从几乎所有Lean 4 GitHub库中提取大规模形式数据，提出了LEAN-GitHub数据集。通过在该数据集上对InternLM-math-plus进行微调，研究发现模型在多个Lean 4基准测试中均取得了优于现有方法的表现，显示出该数据集在广泛数学主题的形式推理中的重要价值。

LEAN-GitHub：为多功能LEAN证明器编译GitHub LEAN库