发生了什么？
Tactician 提供 Coq 插件，从已有 tactic script 中学习，既能交互式推荐下一步 tactic，也能执行 tactic 层面的自动证明合成，并支持从已安装的 Coq 开发中持续学习。
为什么重要？
它是较早的、持续维护的 proof-assistant-native 学习平台之一，预示了后来把交互式证明状态暴露给持续改进学习 Agent 的 AI 定理证明基础设施路线。
重要性说明：Tactician 将学习式 tactic 预测发展为直接嵌入 Coq 的交互工作流：它可以从既有开发中学习、建议下一步 tactic 或自动合成证明，并在跨 package dependency 的实际使用中持续适应。
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 实质性支持
- 形式保障
- 有形式化工件
如何理解这些标签？ →
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 学习模型对 tactic 选择进行排序并驱动 tactic 层面的证明搜索，同时仍嵌入由人控制的 Coq 证明开发循环。
- 人类贡献
- 研究者设计学习与搜索机制、实现 Coq 插件及 dependency-aware instrumentation；人工编写的 Coq 开发则提供系统学习所需的 tactic 轨迹。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- tactician, coq
- 机构
- —
- 数学问题
- —
- 方法
- tactic-learning, proof-search, online-learning, proof-synthesis
