# Hammering with Vampire in Lean

**Authors:** Jonas Bodingbauer, Laura Kovács  
**Lab:** TU Wien · **Published:** 29 Oct 2026  
**Links:** [arXiv](https://arxiv.org/abs/2610.40310) · [PDF](https://arxiv.org/pdf/2610.40310) · [This page](https://omen-bit.github.io/ai-paper-daily/paper/2610.40310.html)

## Key numbers

- **21,158**: Vampire-Hammer solves 21,158 problems not solved by other evaluated tools within the same budget

## 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.

---

Notes written by AI from the paper, numbers copied from the abstract. Check the paper before you rely on them. From AI Papers Daily.