HOList complex corpus
收藏arXiv2025-09-30 收录
下载链接：
https://arxiv.org/abs/1905.10501
下载链接
链接失效反馈官方服务：
资源简介：
该数据集包含了从HOL Light数学库中衍生出的定理，涵盖了数学的多个领域，如拓扑学、多变量微积分、实分析和复分析、几何代数以及测度论。此外，该数据集还分为训练集、验证集和测试集，用于评估自动定理证明方法的性能。具体规模包括10,214个训练定理、3,225个验证定理、2,320个核心定理以及637个定义。任务内容是使用定理和定义作为前提来证明定理。
This dataset comprises theorems derived from the HOL Light mathematical library, spanning multiple mathematical domains including topology, multivariable calculus, real and complex analysis, geometric algebra, and measure theory. Furthermore, the dataset is partitioned into training, validation, and test sets for evaluating the performance of automated theorem proving methods. Its specific scale consists of 10,214 training theorems, 3,225 validation theorems, 2,320 core theorems, and 637 definitions. The task is to prove target theorems using the provided theorems and definitions as premises.
提供机构：
HOList benchmark
