新论文 · v1arXiv:2610.40310
在 Lean 中用 Vampire 进行自动定理证明
Hammering with Vampire in Lean
Jonas Bodingbauer, Laura Kovács
AI 速览：作者提出 Vampire-Hammer，将 Lean 目标交给 Vampire 自动定理证明器求解，并重建可由 Lean 内核检查的证明。
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.
cs.LO · cs.AI