cs.LOOct 29, 2026

Hammering with Vampire in Lean

Authors: Jonas Bodingbauer, Laura Kovács

Organizations: TU Wien, Vienna, Austria

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Figures & tables

Figure 2: The Vampire-Hammer pipeline via Lean-auto and proof reconstruction. Additional goals from goal splitting and domain inhabitation return to goal preparation.
Figure 3: Cactus plots and solve counts over two runs with a 10 s10\,\mathrm{s} proof budget. Unique counts denote problems solved by the respective tool, not solved by any other tool in the suite. VH: Vampire-Hammer ; LD: Lean-auto + Duper ; DU: Duper ; AE: Aesop ; SA: simp_all ; GR: grind ; TB: theoretical best, combining all tools using the fastest successful proof per problem.
Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Tool or componentVersionCommit
Vampire-Hammer0.1.04c50a21de3e4
Vampire5.1.06ee1f120df1b
Duper4.34.19e09cd05fd54
Lean-auto4.34.16b2774cde4d1
Aesop4.34.0355695d523e4
simp_all (Lean)4.34.15045d0056413
Appendix
Table 1: Tool versions and dependency pins from the saved benchmark setup, with abbreviated commit identifiers. A dash indicates that no release version was established.
More in this topic

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 162 papers

Explore similar work

CardsList

  1. MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

    May 26, 2026Jinzheng Li, Zeru Zhu, Yuanjie RenLarge Language Model-Guided Theorem ProvingAutomated Theorem Proving

    1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology

  2. Lean Graph Search for Formal Theorem Proving

    Oct 15, 2026Yihan Xu, Jia-Chen Gu, Junyi Zhang +7Graph-Based RetrievalLean Theorem Proving

    University of California, Los Angeles

  3. Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

    Oct 18, 2026Haotian Deng, Chris Farber, Sonal Narasimha +2Automated Theorem ProvingLarge Language Model-Guided Theorem Proving

    Purdue University