主要证据
- Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem ProversS1 · 主要研究来源 · 论文 · 2010-07-14
Sledgehammer 将外部自动证明器实用化地接入 Isabelle
Sledgehammer 自动选择 Isabelle 相关事实，将证明义务翻译给外部 ATP，并利用返回结果帮助构造由证明助手检查的证明。
发生了什么？
Lawrence Paulson 与 Jasmin Blanchette 在 2010 年 7 月 14 日 PAAR-2010 报告三年 Sledgehammer 使用经验，将其定位为 Isabelle 与自动定理证明器之间的实用桥梁。
为什么重要？
该系统让强自动化进入日常交互式证明流程，并成为后来“外部搜索 + 可信证明检查”AI 助手的重要前史。
重要性说明：Sledgehammer 建立了交互式证明助手与强大外部 ATP 的实用结合架构，自动选择相关事实，并把外部搜索转化为证明助手内部可用的证明进展。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 实质性支持
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 自动前提选择与外部证明器承担大量证明搜索，Isabelle 保留可信形式证明环境。
- 人类贡献
- 研究者设计翻译、相关性筛选、证明器编排与证明重建机制；用户提供形式目标并整合所得证明步骤。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 机器检查
- 最后审阅
- 2026-09-15
技术细节
- 系统
- sledgehammer, isabelle
- 机构
- university-of-cambridge
- 数学问题
- interactive-theorem-proving
- 方法
- premise-selection, automated-theorem-proving, proof-reconstruction
全部来源与工件
- Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem ProversS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
验证历史
- 2010-07-14 · 论文已发布 · E2 · 研究记录
PAAR-2010 议程与 proceedings 记录了 Sledgehammer 的 Isabelle/ATP 工作流；machine_checked 指重建形式证明由证明助手验证，并不表示 Chronicle 独立复现使用结果。
更正
当前没有记录的更正。