/ Paper arXiv 2610.40310
In short
In shortReport a mistake
Key numbers
From the paperCopied from the abstract, not written by AI.
Abstract
From the paperThe authors' own words.
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.
From the full paper
From the paperCopied from the paper itself by our code.
Reading the paper on arXiv…
Ask this paper
/ Ask a questionAnswers come from the full paper and name the section
/ Your notes
Select text in the abstract to highlight it or add a note. They stay in this browser.
