HOList

该数据集名为HOList，包含29,465个定理及其证明，其中以“核心”和“复杂”数据集为重点，涵盖18,943个定理、637个定义以及603,950个证明步骤。该数据集涉及数学的多个领域，如集合论、算术、线性代数、拓扑学以及多变量复分析等。数据集使用S-表达式来表示陈述，并在定理上明确划分了训练/验证/测试数据。在“核心”和“复杂”数据集中，共包含18,943个定理。此外，该数据集的任务包括逻辑推理，涵盖了类型推断以及预测定理中缺失的假设。

The dataset named HOList contains 29,465 theorems and their corresponding proofs, with its "core" and "complex" subsets as the focal points, which encompass 18,943 theorems, 637 definitions, and 603,950 proof steps. This dataset spans multiple mathematical domains, including set theory, arithmetic, linear algebra, topology, multivariable complex analysis, and other related fields. Formal statements in the dataset are represented using S-expressions, and explicit train/validation/test splits are assigned to each theorem. A total of 18,943 theorems are included in the core and complex subsets. Additionally, the tasks supported by this dataset involve logical reasoning, including type inference and predicting missing assumptions within theorems.