Source-linked AI summary
Hammering with Vampire in Lean
Jonas Bodingbauer, Laura Kovács
TL;DR
Lean proof automation faces the challenge of translating dependent-type goals for ATP search while reconstructing proofs in a form the kernel can check. VAMPIRE-HAMMER combines LEAN-AUTO, Vampire, and annotated TSTP proof reconstruction inside Lean. On 196,083 eligible Mathlib theorems, it uniquely solves 21,158 problems within a 10-second budget that no other evaluated tool solves within that budget.
Problem
Integrating automated theorem provers with full proof reconstruction in dependent-type provers such as Lean remains challenging because translation and reconstruction are distinct problems.
Source: §1 · p. 1Method
VAMPIRE-HAMMER translates Lean goals through LEAN-AUTO, searches with Vampire, and reconstructs annotated TSTP proofs in Lean as kernel-checkable terms.
Source: §1 · p. 2, §2 · pp. 3–4Results
Takeaways & Limitations
VAMPIRE-HAMMER extends the reach of existing Lean proof automation on the evaluated benchmark.
Source: §4 · p. 6The evaluation excludes targets whose statements or original proofs reference constants introduced by the same command.
Source: §4 · p. 5
Abstract
from arXiv · showhide
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.
1 Introduction
VAMPIRE-HAMMER brings Vampire proof search to Lean with proof reconstruction checked by Lean’s kernel. It addresses the challenge of combining dependent-type translation with reconstruction, and extends proof automation on Mathlib benchmarks.
1 Introduction
- Integrating ATPs with full proof reconstruction in dependent-type provers such as Lean remains challenging because translation and reconstruction are distinct problems.Earlier approaches translated fragments of dependent type theory, but had not fully addressed both challenges.Source: §1 · p. 1
- Figure 1 illustrates a group-theory goal that VAMPIRE-HAMMER discharges with one tactic call, replacing an explicit proof that factors the commutator into three squares.The goal states that central squares imply central commutators.Source: Figure 1 · p. 2
- VAMPIRE-HAMMER combines LEAN-AUTO translation with annotated TSTP proof output and reconstruction in Lean.It exports problems in TPTP syntax and produces proof terms checked by Lean’s kernel.Source: §1 · pp. 1–2
- 21,158 Mathlib problems were solved only by VAMPIRE-HAMMER among evaluated tools within the 10-second budget.The evaluation covered 196,083 theorems.Source: §1 · p. 2
2 The VAMPIRE-HAMMER Pipeline
VAMPIRE-HAMMER prepares Lean goals, exports them for Vampire search, and reconstructs the returned refutation as Lean proof terms checked by the kernel.
2 The VAMPIRE-HAMMER Pipeline
- The tactic first tries lightweight Lean-native reasoning; if that fails, it translates the problem for Vampire and reconstructs the resulting refutation as a Lean proof.Successful invocations ultimately produce proof terms checked by Lean’s kernel.Source: §2 · pp. 2–3
- Goal preparation negates the goal and collects explicit premises, local facts, typeclass laws, and defining equations, normalizing expressions as needed.The task becomes deriving ⊥ from the premises together with the negated goal.Source: §2 · p. 3
- LEAN-AUTO handles monomorphization and translation, while preprocessing tracks inhabitation obligations because TPTP sorts are nonempty and Lean types may be empty.Depending on configuration, the output is a monomorphic higher-order or first-order encoding.Source: §2 · p. 3
- The exporter maps fresh names for source types, symbols, and formulas to their reified counterparts before passing first- or higher-order TPTP problems to Vampire.Vampire’s proof output includes annotations such as unifiers and modified literal positions; added associativity and commutativity bridges record clause permutations.Source: §2 · p. 3
- Lean parses annotated TSTP steps and reconstructs each as a local lemma, using rule-specific procedures and grind as a fallback when those procedures do not apply.Local justifications for introduced symbols are assembled into a proof of the empty clause, then Lean-Auto assembles the term checked against the original goal.Source: §2 · pp. 3–4
3 Search Strategy
VAMPIRE-HAMMER supports both higher- and first-order search, schedules them in complementary time slices, and handles goals involving potentially empty types through additional inhabitation reasoning.
3 Search Strategy
- Higher-order export preserves function types, while first-order search is more mature and optimized but can produce larger problems and discard information.The paper therefore treats both routes as viable.Source: §3 · p. 4
- When no inhabitant is found, Vampire first searches assuming the type is inhabited; if that assumption is used, the tactic also tries the empty-type case and combines both proofs when successful.An unused inhabitation assumption leaves a proof that can be reconstructed immediately.Source: §3 · p. 4
- Search begins with higher-order mode for 20% of the budget, then uses first-order portfolio search, with a later higher-order attempt using additional hints if needed.The time allocation was determined empirically; easily split conjunction goals receive reserved time for their subgoals.Source: §3 · p. 5
4 Experimental Evaluation
On a 10-second budget, VAMPIRE-HAMMER solves many Mathlib problems not solved by the other evaluated tools, within a benchmark using proof-derived premises.
4 Experimental Evaluation
- The benchmark covers 196,083 eligible Mathlib theorems and supplies each tactic with the target’s direct proof dependencies and local hypotheses.The setup primarily evaluates automated reasoning given proof-derived premises rather than end-to-end premise selection.Source: §4 · p. 5
- Targets are excluded when their statements or original proofs reference constants introduced by the same command.The harness reconstructs the environment immediately before the target’s original declaration.Source: §4 · p. 5
- Each tactic invocation receives a 10-second wall-clock budget that includes premise extraction, tactic execution, and kernel checking.A success requires a complete proof accepted by Lean’s kernel.Source: §4 · p. 5
- VAMPIRE-HAMMER proved 96,289 of the 196,083 benchmark theorems within 10 seconds; across all compared tools, 124,854 were solved, including 21,158 solved only by VAMPIRE-HAMMER.Source: §4 · pp. 5–6
- 21,158 problems were solved uniquely by VAMPIRE-HAMMER among the evaluated tools within the 10-second budget.The union of all tools solved 124,854 theorems, and the paper reports a 20.4% relative improvement.Source: Figure 3 · p. 6, §4 · p. 6
5 Conclusion
VAMPIRE-HAMMER brings Vampire to Lean through proof-producing translation and reconstruction, and solves problems left unsolved by other evaluated tools on the Mathlib benchmark.
5 Conclusion
- 21,158 problems were solved by VAMPIRE-HAMMER that no other evaluated tool solved within the same budget.The evaluation covered 196,083 eligible Mathlib theorems.Source: §5 · p. 6
- VAMPIRE-HAMMER translates Lean goals and premises into first-order or higher-order TPTP, then reconstructs annotated TSTP proofs as local lemmas checked by Lean’s kernel.The translation uses Lean-Auto, and the reconstructed proof yields a Lean-checked proof term.Source: §5 · p. 6
- TSTP-based reconstruction may extend to other ATPs when their inference rules and proof output can be supported; future work includes premise selection, better exported problems, and Vampire higher-order reasoning..Source: §5 · p. 6
A Benchmark Setup
The benchmark evaluates theorems in their declaration-time Lean environments, using explicit premises drawn from their original proofs while retaining other available library support.
A Benchmark Setup
- Each theorem is evaluated in an environment reconstructed from immediately before its declaration, excluding the target theorem and later declarations.Source: A Benchmark Setup · p. 9
- Tools receive the same proof-derived premise names, but may also use global simplification rules, registered grind rules, and available typeclass instances.Such background knowledge can make some goals simpler, including when an earlier theorem provides an equivalent result.Source: A Benchmark Setup · p. 9
- The evaluation measures reconstruction of existing Mathlib theorems with premises from their original proofs, not interactive usability or full-library premise discovery.Source: A Benchmark Setup · p. 9
B Benchmarked Tool Versions
The benchmark materials document the saved setup’s tool versions and provide per-tool proof-attempt results and benchmarking scripts.
B Benchmarked Tool Versions
- Table 1 documents tool versions and dependency pins from the saved benchmark setup, including abbreviated commit identifiers.A dash indicates that no release version was established.Source: Table 1 · p. 9
- Two CSV files report each tool’s proof-attempt results for the 196,083 eligible theorems.Source: B Benchmarked Tool Versions · p. 9
- The benchmarking scripts are available in the vampire-hammer-benchmarks repository.Source: B Benchmarked Tool Versions · p. 9
C Usage
VAMPIRE-HAMMER is installed as a Lake dependency and invoked as a Lean tactic, with options for premise selection and search behavior.
C Usage
- VAMPIRE-HAMMER is installed as a Lake dependency that automatically builds Vampire and the bundled TPTP parser.The dependency is added through the Lean project’s lakefile.Source: C Usage · p. 9
- After importing VampireHammer, users invoke the vampire tactic on selected hypotheses or lemmas, or use vampire [*] to select all local hypotheses.The section gives a simple example using two hypotheses to prove a goal.Source: C Usage · p. 10
- Search defaults to concurrent first-order and native higher-order attempts with a 10-second allowance, while options control timeout, sequencing, definitions, caching, and output retention.Completed proofs are cached within the Lean session; vampire.outputPath retains input and prover output.Source: C Usage · p. 10