Hammering with Vampire in Lean.

arXiv:2610.40310v1 Announce Type: cross 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 us