eaeasee/Lean-Workbook2
收藏官方服务：
资源简介：
该数据集是关于用Lean 4形式化的竞赛级数学问题集合。它包含两个拆分部分：Lean Workbook有57231个问题，Lean Workbook Plus有82893个问题。每个问题提供自然语言陈述、答案、形式化陈述和形式化证明（如果可用）。这些数据可用于支持自动形式化模型训练和证明搜索。数据集基于Lean v4.8.0-rc1和Mathlib4相同版本的环境。
This dataset is about contest-level math problems formalized in Lean 4. It contains 57231 problems in the split of Lean Workbook and 82893 problems in the split of Lean Workbook Plus. We provide the natural language statement, answer, formal statement, and formal proof (if available) for each problem. These data can support autoformalization model training and searching for proofs. The test environment is based on Lean v4.8.0-rc1 with Mathlib4 of the same version.
提供机构：
eaeasee
