{"id":"arxiv:2603.26342","kind":"preprint","title":"Lean on Vampire Proofs (Short Paper)","authors":["Jonas Bodingbauer","Márton Hajdu","Laura Kovács","Axel Polaczek","Michael Rawson"],"author_count":5,"year":2026,"published":"2026-03-27","venue":null,"cited_by":null,"doi":null,"arxiv_id":"2603.26342","nct_id":null,"source_url":"https://arxiv.org/abs/2603.26342","archive_url":"https://space-kitty.com/papers/arxiv:2603.26342","updated":"2026-03-27","pmid":null,"pmcid":null,"openalex_id":null,"pdf_url":"https://arxiv.org/pdf/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","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.LO"],"details":null,"provenance":"arxiv","attribution":"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.","topics":[],"cited_in_dossiers":[]}