Lean on Vampire Proofs (Short Paper)
arXiv:2603.26342
Abstract
Vampire proves theorems completely automatically in first- and higher-order logic extended with theories. Proof checking is increasingly demanded to consolidate user trust in Vampires output. We describe ongoing efforts in reconstructing Vampire proofs as trusted proofs in Lean
arXiv comment9 pages, 3 figures