arXiv cs.AI· Jonas Bodingbauer, Laura Kov\'acs·· 13 小时前AI 评分22
Vampire-Hammer：为 Lean 定理证明器接入 Vampire 自动证明器
Hammering with Vampire in Lean
AI 导读
Vampire-Hammer 是一款面向 Lean 交互式定理证明器的 hammer 工具，借助 Vampire 自动定理证明器完成目标证明，并由 Lean 内核校验重构后的证明。
正文 · AI 翻译
摘要：我们提出 Vampire-Hammer，这是一个用于 Lean 交互式定理证明器的锤子工具，它使用 Vampire 自动定理证明器来消解目标，并重建由 Lean 内核检查的证明。Vampire-Hammer 使用 Lean-auto 框架处理目标和前提，然后将它们分派给 Vampire 进行证明搜索。在此过程中，我们依赖标准的 TPTP 问题格式和带注释的 TSTP 证明，以支持证明重建。在 196,083 个符合条件的 Mathlib 定理上，以 10 秒为预算，Vampire-Hammer 解决了 21,158 个其他已评估工具在相同预算内未能解决的问题。
| 评论： | 10 页，3 幅图，1 张表。工具演示论文 |
| 主题： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI） |
| 引用为： | arXiv:2610.40310 [cs.LO] |
| （或 arXiv:2610.40310v1 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.40310 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Jonas Bodingbauer [查看电子邮件]
[v1]
2026 年 10 月 29 日星期四 15:49:40 UTC（282 KB）
来源：arXiv cs.AI · arxiv.org