arXiv cs.AI· Jonas Bodingbauer, Laura Kov\'acs·· 14 小时前AI 评分22
Vampire-Hammer：为 Lean 定理证明器接入 Vampire 自动证明器
Hammering with Vampire in Lean
AI 导读
Vampire-Hammer 是一款面向 Lean 交互式定理证明器的 hammer 工具，借助 Vampire 自动定理证明器完成目标证明，并由 Lean 内核校验重构后的证明。
正文 · 原文
Abstract:We present Vampire-Hammer, a hammer for the Lean interactive theorem prover that discharges goals using the Vampire automated theorem prover and reconstructs proofs checked by the Lean kernel. Vampire-Hammer uses the Lean-auto framework to process goals and premises before dispatching them to Vampire for proof search. Doing so, we rely on standard TPTP problem formats and annotated TSTP proofs that support proof reconstruction. With a 10-second budget on 196,083 eligible Mathlib theorems, Vampire-Hammer solves 21,158 problems not solved by other evaluated tools within the same budget.
| Comments: | 10 pages, 3 figures, 1 table. Tool demonstration paper |
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.40310 [cs.LO] |
| (or arXiv:2610.40310v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2610.40310 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Jonas Bodingbauer [view email]
[v1]
Thu, 29 Oct 2026 15:49:40 UTC (282 KB)
来源：arXiv cs.AI · arxiv.org