# Lean on Vampire Proofs (Short Paper)

Preprint · Jonas Bodingbauer, Márton Hajdu, Laura Kovács, Axel Polaczek, Michael Rawson

- Archive id: arxiv:2603.26342
- Published: 2026-03-27
- arXiv: https://arxiv.org/abs/2603.26342
- Source URL: https://arxiv.org/abs/2603.26342
- PDF: https://arxiv.org/pdf/2603.26342
- Provenance: arxiv

## 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 reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.