Preprint: not peer reviewed. Results may change in later versions.
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
Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.
Record
- Archive ID
- arxiv:2603.26342
- Published
- Mar 27, 2026
- arXiv
- 2603.26342
- Categories
- cs.LO
- Provenance
- arxiv