跳到正文
研踪PaperTrail
← 研踪 PaperTrail

arXiv:2610.40310 · v1

Hammering with Vampire in Lean

Jonas BodingbauerLaura Kovács
cs.LOcs.AI
首次提交 2026-10-29 23:49
版本更新 2026-10-29 23:49
雷达观测 2026-10-30 13:28
arXiv ↗PDF ↗

摘要

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.

作者备注：10 pages, 3 figures, 1 table. Tool demonstration paper

查看 arXiv 原文 ↗阅读 PDF ↗

AI 论文解读

基于摘要 · 非全文审阅

作者提出 Vampire-Hammer，将 Lean 目标交给 Vampire 自动定理证明器求解，并重建可由 Lean 内核检查的证明。

正在读取账号与研究记录…

版本差异

目前只观测到一个版本，无法比较变化。之后收录新版本时，会在这里对照标题、作者、分类和摘要。

观测到的版本

相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。

v1 · 2026-10-29 23:49 · 最新观测版本

Hammering with Vampire in 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.

查看此版本解读 →查看此版本原文 ↗