LOMar 27
Lean on Vampire Proofs (Short Paper)
arXiv:2603.2634259.1h-index: 4
AI Analysis
This work tackles the problem of proof verification for users of automated theorem provers, but it appears incremental as it builds on existing methods without introducing new paradigms.
The paper addresses the challenge of verifying Vampire's automated theorem proofs to enhance user trust by reconstructing them as trusted proofs in Lean, with ongoing efforts described but no concrete results or numbers provided.
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