HolStep 从 HOL Light 证明中抽取中间陈述与 conjecture，对文本表示进行规范化，并把实际使用的证明步骤与负样本配对。该发布定义 conditioned 与 unconditioned proof-step classification 等任务，并提供基线代码，使研究者能够在统一的形式数学语料上比较学习式表示与相关性模型。
Cezary Kaliszyk、François Chollet 与 Christian Szegedy 发布 HolStep：一个基于 11,400 条 HOL Light 证明构建、采用 BSD 许可的数据集，包含超过两百万个带标签的训练与测试证明步骤样本，并配套定义证明步骤有用性等 benchmark 任务以及逻辑回归、卷积网络和循环神经网络基线。
该项目推动定理证明机器学习从小规模、定制化实验走向可复用数据集与可复现评测。HolStep 随后成为多种神经架构的 benchmark，并成为后来“交互环境 + benchmark”形式数学系统的重要历史前序。
重要性说明：HolStep 将大规模 HOL Light 证明轨迹整理为公开机器学习数据集与 benchmark，包含数百万个带标签的证明步骤样本。它把真实高阶逻辑数学中的前提有用性与证明步骤相关性转化为可统一评测的问题，为早期神经定理证明研究提供了公共基础，并直接支撑 FormulaNet 等后续工作，也预示了 HOList 这类更完整的 HOL Light 学习环境。
arXiv 与 ICLR 研究记录确认了 HolStep 数据集、benchmark 任务以及论文报告的基线实验。
公开 Deepmath 仓库仍保留 HolStep 基线代码，原始研究记录也明确给出公开数据集入口。E3 表示 artifact 可直接检查，并不代表论文报告的全部基线结果已获得独立复现。
当前没有记录的更正。
