CoqGym 从开源 Coq 项目中抽取证明状态、环境、目标、tactics 与证明树，并通过可编程交互层暴露这些信息。ASTactic 从该语料学习生成证明步骤，并基于运行时语法组合 tactics，而不是仅依赖预先固定的完整 tactic 列表。
Kaiyu Yang 与 Jia Deng 发布 CoqGym：一个由 123 个 Coq 项目、约 71,000 条人工证明构成的数据集与交互环境，并提出 ASTactic 深度学习模型，以抽象语法树形式生成 tactics；论文报告其能够证明部分比较基线中的内置自动 tactic 无法证明的留出定理。
CoqGym 使成熟交互式证明助手上的学习式定理证明获得更丰富、可复现的数据与交互基础。其“环境 + 大型证明语料”设计预示了 LeanDojo 等后来项目把证明助手数学库封装为可复用机器学习基础设施的路线。
重要性说明：CoqGym 将大量真实 Coq 工程转化为包含数万条人工证明的交互式机器学习环境；ASTactic 则生成结构化 tactic，而不是只从固定 tactic 集合中选择。该环境成为后来证明助手学习基础设施的重要早期范式之一。
arXiv 与 ICML 研究记录确认了 CoqGym、ASTactic、数据规模及论文报告的留出定理证明实验。machine_checked 仅指生成证明通过 Coq 检查，并不表示论文报告的成功率已得到独立复现。
公开 CoqGym 仓库提供交互环境、数据抽取管线、证明语料工具与 ASTactic 实现。E3 表示存在可直接检查的 artifacts，而非对全部实验结论的独立验证。
当前没有记录的更正。
