Lean-Workbook
收藏arXiv2025-09-30 收录
下载链接：
https://huggingface.co/datasets/internlm/Lean-Workbook
下载链接
链接失效反馈官方服务：
资源简介：
该数据集名为“Lean-Workbook”，包含了一系列用于自动定理证明的数学问题。该数据集中不仅包含了已被证明和反驳的陈述，还附有相应的策略和状态，这有助于展示问题难度的分布以及定理证明方法的有效性。在处理过程中，该数据集耗用了超过20,000个CPU日。其任务是自动定理证明。
The dataset named "Lean-Workbook" contains a series of mathematical problems designed for automated theorem proving. It not only includes both proven and refuted statements, but also provides corresponding proof tactics and states, which helps demonstrate the distribution of problem difficulty and the effectiveness of automated theorem proving methods. During its processing, this dataset consumed over 20,000 CPU-days. The core task of this dataset is automated theorem proving.
提供机构：
InternLM
