HOList 对 HOL Light 进行工程化封装，使学习系统能够通过机器学习环境与证明状态和 tactics 交互。其 benchmark 将 core、complex 与 Flyspeck 语料中的定理陈述整理为训练、验证和测试划分；DeepHOL 则提供神经证明器与强化学习循环，用于持续生成新的成功证明轨迹。
Google Research 与合作研究者发布 HOList：一个基于 HOL Light 的开源强化学习环境与 benchmark，并配套发布 DeepHOL 深度学习 tactic 证明器；该系统利用人工与合成证明训练，并在包含 Flyspeck 相关内容的定理语料上进行评测。
该工作展示了如何把成熟证明助手与大型数学库转化为可交互的学习环境，而不仅是静态语料。此后“环境 + benchmark”的模式成为神经定理证明基础设施的重要范式，并使证明助手原生的强化学习成为可重复研究路线。
重要性说明：HOList 将开放的 HOL Light 交互环境、源自大型形式数学库的 benchmark 与 DeepHOL 神经证明器整合为统一研究栈，成为强化学习与神经证明引导进入交互式定理证明的重要早期参照，并为后来更端到端地学习搜索与 tactic 选择的系统提供前史。
arXiv 与 ICML 研究记录确认了 HOList、其 benchmark 以及论文报告的 DeepHOL 实验。machine_checked 仅指证明轨迹通过 HOL Light 检查，并不表示论文报告的 benchmark 性能已得到独立复现。
公开的 Deepmath 代码库与 HOList benchmark 网站提供证明器代码、benchmark 定义、模型资源与证明检查流程。E3 表示存在可直接检查的 artifacts，而非对全部实验结论的独立确认。
当前没有记录的更正。
