Papers With

← All papers
First page of Hammering with Vampire in Lean

Hammering with Vampire in Lean

Jonas Bodingbauer, Laura Kovács

cs.LO Oct 29, 2026 · v1 cs.AI
tactic-automation tooling mathlib logic
Read PDF arXiv abstract Code
TL;DR
Builds a Lean hammer tactic that sends goals to the Vampire prover via Lean-auto, rebuilds the proofs for Lean kernel checking, and evaluates it on Mathlib.
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.
Problem

Using automated theorem provers as hammers in dependent-type-theory ITPs such as Lean is hard. Goals must be translated into first- or higher-order logic, and the external proofs must be reconstructed so the kernel can check them.

Approach

Vampire-Hammer is a Lean tactic. It first tries lightweight Lean-native reasoning. If that fails, it uses Lean-auto to monomorphize goals and premises and export them to higher-order (THF) or first-order (TF0) TPTP. Vampire is extended to output annotated TSTP proofs, which are reconstructed in Lean as compositions of local lemmas and checked by the kernel.

Results

With a 10-second budget on 196,083 eligible Mathlib theorems, given proof-derived premises, Vampire-Hammer solves 21,158 problems that no other evaluated tool solves. The comparison tools are Duper, Lean-auto, Aesop, simp_all and grind.