AI-MO/NuminaMath-LEAN
收藏Hugging Face2025-07-31 更新2025-08-09 收录
下载链接：
https://hf-mirror.com/datasets/AI-MO/NuminaMath-LEAN
下载链接
链接失效反馈官方服务：
资源简介：
NuminaMath-LEAN是一个大规模的数学竞赛问题数据集，包含10万个使用Lean 4语言形式化的数学竞赛问题。该数据集源自NuminaMath 1.5数据集的挑战性子集，专注于IMO和USAMO等著名竞赛的问题。它是迄今为止为训练和评估自动定理证明器而设计的人类注释形式化声明和证明的最大集合。此数据集也是我们Kimina-Prover 72B背后的数据集。
NuminaMath-LEAN is a large-scale dataset of 100K mathematical competition problems formalized in Lean 4. It is derived from a challenging subset of the NuminaMath 1.5 dataset, focusing on problems from prestigious competitions like the IMO and USAMO. It represents the largest collection of human-annotated formal statements and proofs designed for training and evaluating automated theorem provers. This is also the dataset behind our Kimina-Prover 72B.
提供机构：
AI-MO
