Vampire-Hammer：用 Vampire 自动定理证明器为 Lean 重建证明
Hammering with Vampire in Lean
AI 导读
研究者提出 Vampire-Hammer，一种面向 Lean 交互式定理证明器的工具，调用 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