Goedel-LM/RL_dataset_V2

--- pretty_name: Goedel-Prover-V2 RL Dataset language: en license: apache-2.0 tags: - theorem-proving - lean4 - code size_categories: 100K<n<1M configs: - config_name: default data_files: - split: train path: data/train-* dataset_info: features: - name: subset dtype: string - name: messages list: - name: content dtype: string - name: role dtype: string splits: - name: train num_bytes: 1059173933.03536 num_examples: 98632 download_size: 336508509 dataset_size: 1059173933.03536 --- # Goedel-Prover-V2 RL Dataset This dataset contains RL data with two task subsets. - `lean4_completion`: Whole Proof Generation - `lean4_revision`: self-revision See [Goedel-Prover-V2 paper](https://arxiv.org/abs/2508.03613). ## Citation ``` @article{lin2025goedel, title={Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction}, author={Lin, Yong and Tang, Shange and Lyu, Bohan and Yang, Ziran and Chung, Jui-Hui and Zhao, Haoyu and Jiang, Lai and Geng, Yihan and Ge, Jiawei and Sun, Jingruo and others}, journal={arXiv preprint arXiv:2508.03613}, year={2025} } ```