LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover
<|reference_start|>LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover: 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<|reference_end|>
@article{wu2024lean-github:,
    title={LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN
  prover},
    author={Zijian Wu, Jiayu Wang, Dahua Lin, Kai Chen},
    journal={arXiv preprint arXiv:2407.17227},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.17227},
    primaryClass={cs.AI cs.CL}
}