59.1LOMar 27
Lean on Vampire Proofs (Short Paper)Jonas Bodingbauer, Márton Hajdu, Laura Kovács et al.
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