Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.40310

Hammering with Vampire in Lean

Jonas Bodingbauer·Laura Kovács
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.LOcs.AI

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jonas Bodingbauer, Laura Kovács. 2026-10-29. Hammering with Vampire in Lean. https://arxiv.org/abs/2610.40310

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Negative Translations for Affine and Lukasiewicz Logic

We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in \emph{affine logic} the translation schemes due to Kolmogorov and Gödel both satisfy Troelstra's criteria for a negative translation. On the other hand, the schemes of Glivenko and Gentzen both fail for affine logic, but for different reasons: one can extend affine logic to make Glivenko work and Gentzen fail and {\it vice versa}. By contrast, in the setting of \emph{Łukasiewicz logic}, we can prove a general result asserting that a wide class of formula translations including those of Kolmogorov, Gödel, Gentzen and Glivenko not only satisfy Troelstra's criteria with respect to a natural intuitionistic fragment of Łukasiewicz logic but are all equivalent.

cs.LO↗
arXiv2026

A Complete Mental Temporal Logic for Intelligent Agents

In this paper, we present a mental temporal logic BPICTL together with a sound and complete axiomatization, which generalizes CTL by introducing mental modalities. A sound and complete inference system of BPICTL is given. We also prove the finite model property and decidability of BPICTL. Furthermore, we present a model checking algorithm for BPICTL.

cs.LO↗
arXiv2026

Hereditary History-Preserving Bisimilarity: Characterizations via Backward Ready Multisets

We devise two complementary characterizations of hereditary history-preserving bisimilarity (HHPB): a denotational one, over stable configuration structures, and an operational one, in a reversible process calculus. Our characterizations rely on forward-reverse bisimilarity (FRB) augmented with backward ready multiset equality, which is able to distinguish between autoconcurrency and autocausation. With respect to previous work, we thus shift the emphasis from uniquely identifying events, as done in other characterizations, to counting occurrences of identically labeled events associated with incoming transitions. This yields a more lightweight behavioral equivalence than HHPB: our bisimulations are still binary relations instead of ternary ones and do not need to incrementally build any labeling- and causality-preserving bijection for occurred events. We show that our characterizations are valid in the absence of non-local autoconflicts. We then study the logical foundations of these characterizations by relating event identifier logic, which captures HHPB, and backward ready multiset logic, developed for our extension of FRB.

cs.LO↗