Vampire hammer solves many more Lean math problems fast
Hammering with Vampire in Lean
Logic in Computer ScienceArtificial Intelligence
Summary
Interactive theorem provers help check mathematical proofs but can get stuck on hard goals. The authors created Vampire-Hammer, a tool that uses an automated prover named Vampire to find proofs for Lean goals quickly. Vampire-Hammer processes Lean problems into a standard format, lets Vampire try to solve them, and then rebuilds the proof inside Lean for verification. In tests on a large math library, Vampire-Hammer solved over 21,000 problems that other tools missed within 10 seconds each.
What this means in practice
- •For formal verification engineers: Quickly discharge proof goals in Lean formalizations by integrating Vampire to automate otherwise difficult subgoals.
- •For software developers in automated reasoning: Improve the automation layer for interactive theorem provers by building on Vampire-Hammer’s integration approach and proof reconstruction techniques.
Authors
Jonas Bodingbauer, Laura Kovács
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.