Summary (Overview)

• VAMPIRE-HAMMER is a new proof-producing hammer that integrates the VAMPIRE automated theorem prover (ATP) with the LEAN interactive theorem prover (ITP), providing full proof reconstruction checked by LEAN's kernel.
• The tool leverages the LEAN-AUTO translation framework to export goals into first-order (TPTP TF0) and higher-order (TPTP THF) logic, then reconstructs annotated TSTP proofs from VAMPIRE as LEAN proof terms.
• VAMPIRE-HAMMER extends VAMPIRE with annotated TSTP proof output, including unifier information, literal position tracking, and associativity/commutativity bridges for clause permutations.
• On a benchmark of 196,083 Mathlib theorems with a 10-second budget, VAMPIRE-HAMMER solves 96,289 problems, including 21,158 unique problems not solved by any other evaluated tool — a relative improvement of 20.4%.
• This is the first complete reasoning pipeline for native proof reconstruction in LEAN supporting both first- and higher-order logic proof extraction.

Introduction and Theoretical Foundation

The paper addresses a fundamental challenge in interactive theorem proving: integrating ATPs like VAMPIRE as proof hammers in dependent type theory-based ITPs such as LEAN. While VAMPIRE has long served as a proof hammer in Isabelle, its integration with LEAN faces distinct challenges:

1. Translation: Goals must be translated from dependent type theory into simply typed higher-order logic or typed first-order logic for VAMPIRE.
2. Reconstruction: The external proof must be reconstructed using the symbols and assumptions introduced during translation, and ultimately verified by LEAN's kernel.

The key insight is that these two tasks — translating a goal and reconstructing an external proof — are distinct challenges not fully addressed by prior techniques. Recent approaches translate fragments of dependent type theory into first- and higher-order logic, but fall short of complete proof reconstruction.

The theoretical foundation builds on prior work in proof checking [13,2], which produced VAMPIRE proofs checkable by Z3 or LEAN. However, direct proof output alone is insufficient: the pipeline requires:

• Translation of proof goals from dependent type theory to a form suitable for VAMPIRE
• Reconstruction of the proof using the original symbols and assumptions

The paper uses standard TPTP syntax [14] for problem exchange and TSTP format for proof output, enabling interoperability and potential extension to other ATPs.

Methodology

Pipeline Overview

The VAMPIRE-HAMMER pipeline consists of five main stages (Figure 2):

1. Goal Preparation and Direct Reasoning: Given a goal $G$ and premises $\Gamma$, the tactic attempts lightweight LEAN-native reasoning first. If that fails, it introduces $\neg G$ and attempts to derive $\bot$ from $\Gamma \cup \{\neg G\}$.

2. Monomorphization and Preprocessing: Delegated to LEAN-AUTO [12], this stage handles typeclass laws, definition unfolding, and tracks inhabitation obligations (TPTP sorts are nonempty, but LEAN allows empty types).

3. External Proof Search: Problems are exported to VAMPIRE in either first-order (TF0) or higher-order (THF) encodings. VAMPIRE runs in portfolio mode for first-order logic and default mode for higher-order logic.

4. Proof Decoding: The TSTP proof is parsed in LEAN and converted into an internal representation with decoded annotations.

5. Local Reconstruction: Each proof step is replayed as a local lemma with premises $P_1, \ldots, P_n$ and conclusion $C$, constructing a LEAN term of the form $P_1 \to \cdots \to P_n \to C$.

Key Technical Innovations

Annotated TSTP output: VAMPIRE is extended to emit reconstruction-critical information:

• uni annotations recording substitutions used in inferences
• rem_lit annotations recording positions of removed literals
• ac bridges recording associativity/commutativity permutations for clause literal reordering

Listing 1 shows this annotation format:

tff(f3, plain, ![X : group] : (mul(X, inv(X)) = e | mul(inv(X), X) = e),
    inf(fw_res, [uni([subs(f2, [b(Y, X)])]), rem_lit(lit(f1, 0))], [f1, f2]]).
tff(f4, plain, ![X : group] : (mul(inv(X), X) = e | mul(X, inv(X)) = e),
    inf(ac, [perm([1, 0))], [f3])).

Reconstruction theorems: Many proof steps are discharged by instantiating general theorems, such as the binary resolution theorem (Listing 2):

theorem resolution (lit : Prop) (c1 c1' c2 c2' : List Prop) : 
  H (c1 ++ lit :: c1') → H (c2 ++ (¬ lit) :: c2') → H ((c1 ++ c1') ++ (c2 ++ c2'))

Fallback: When rule-specific reconstruction fails, grind [8] is used as a fallback. Symbols introduced externally (Skolem constants, AVATAR split predicates, named definitions) are justified via local let statements.

Search Strategy

Three complementary strategies are employed:

1. Split higher/first-order routes: Higher-order export preserves function types and expressive subsets of dependent type theory; first-order search is more optimized in VAMPIRE but may produce larger problems.

2. Domain inhabitation search: A time-limited search for type inhabitants is performed. If no inhabitant is found, VAMPIRE is invoked assuming inhabitation, with the justification as an open obligation. If the proof doesn't use this assumption, it is reconstructed immediately; otherwise, the complementary empty-type case is attempted.

3. Time scheduling: Higher-order search runs during the first 20% of the budget (tends to terminate quickly), then first-order portfolio mode, then a final higher-order attempt with additional hints. Goals of the form $A \land B$ are split with reserved time for subgoals.

Empirical Validation / Results

Benchmark Setup

• Benchmark: User-declared theorems of Mathlib, using LEAN version v4.34.1
• Premises: Direct theorem dependencies from original proofs plus local hypotheses
• Eligible cases: 196,083 theorems (intersection across all tools)
• Budget: 10-second wall-clock per invocation, including premise extraction, tactic execution, and kernel checking
• Hardware: AMD EPYC 9335 CPUs at 3 GHz, 1.5 TB memory, 64 parallel LEAN instances per node
• Validation: Two full runs, arithmetic mean reported; proofs must be accepted by LEAN's kernel; sorryAx and self-referential proofs are rejected

Comparative Results

Key findings from Figure 3 (cactus plots):

• The union of all tools solves 124,854 theorems; VAMPIRE-HAMMER solves 96,289 (77.1% of the theoretical best).
• 21,158 problems are solved exclusively by VAMPIRE-HAMMER — a relative improvement of 20.4% over the union of all other tools.
• Notable kinks in the VAMPIRE-HAMMER curve reflect transitions between proof search modes.
• Of all problems exported to VAMPIRE: 62% solved via higher-order reasoning, 36% via first-order, and 1% via both (influenced by the higher-order-first schedule).

Theoretical and Practical Implications

Theoretical Significance

• First complete pipeline for native proof reconstruction in LEAN supporting both first- and higher-order logic proof extraction from VAMPIRE.
• Demonstrates that ATP proof search efficiency can be fully maintained in a hammer while reconstruction is shared efficiently between the ATP and ITP.
• Establishes that dependent type theory goals can be effectively translated to classical first- and higher-order logic while retaining proof reconstructability.

Practical Implications

• Extensibility: Because proofs are exchanged through standard TSTP format, the reconstruction approach may extend to other ATPs whose inference rules and proof output can be annotated similarly.
• Complementarity: VAMPIRE-HAMMER significantly extends the reach of existing LEAN proof automation — its 21,158 unique solutions represent theorems that no other tool can currently prove within budget.
• Theorem prover integration: Provides a practical template for integrating efficient external provers with kernel-verified proof checking in dependent type theory systems.

Conclusion

The paper presents VAMPIRE-HAMMER, a proof-producing hammer that brings VAMPIRE's automated reasoning capabilities to LEAN with full kernel verification. The tool successfully:

• Exports goals via LEAN-AUTO into first-order or higher-order TPTP
• Searches for refutations with VAMPIRE
• Reconstructs annotated TSTP proofs inside LEAN as compositions of local lemmas
• Produces proof terms checked by LEAN's kernel

The evaluation demonstrates substantial practical impact: 21,158 problems solved uniquely by VAMPIRE-HAMMER among 196,083 eligible Mathlib theorems within a 10-second budget.

Future directions identified by the authors:

1. Integration of full-library premise selection (e.g., via lean-hammer [16])
2. Improving exported problem quality
3. Advancing higher-order reasoning capabilities in VAMPIRE

Availability: Implementation at https://github.com/vprover/vampire-hammer; benchmark data at https://doi.org/10.5281/zenodo.23405497.