Lean on Vampire Proofs (Short Paper)
Jonas Bodingbauer, M\'arton Hajdu, Laura Kov\'acs, Axel Polaczek, Michael Rawson
TL;DR
This paper discusses efforts to reconstruct Vampire theorem prover proofs as trusted proofs in Lean to enhance proof checking and user trust.
Contribution
It introduces ongoing work to translate Vampire proofs into Lean, aiming to improve proof verification and trustworthiness.
Findings
Initial proof reconstruction approach developed
Enhanced proof checking in Lean demonstrated
Potential for increased user trust in Vampire proofs
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
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.