Lean on Vampire Proofs (Short Paper)
Logic in Computer Science
2026-03-30 v1
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
Keywords
Cite
@article{arxiv.2603.26342,
title = {Lean on Vampire Proofs (Short Paper)},
author = {Jonas Bodingbauer and Márton Hajdu and Laura Kovács and Axel Polaczek and Michael Rawson},
journal= {arXiv preprint arXiv:2603.26342},
year = {2026}
}
Comments
9 pages, 3 figures