CoolFace
Datasetpublic

internlm/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 🤗Model 📑 Paper 📖 README Citation and Tech Report @misc{wu2024leangithubcompilinggithublean, title={LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover}, author={Zijian Wu and Jiayu… See the full description on the dataset page: https://huggingface.co/datasets/internlm/Lean-Github.

sourceHugging Faceapache-2.0updated 2y agoView on Hugging Face
41likes348downloads
Dataset Card

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 🤗Model 📑 Paper 📖 README

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