Document Open Access Logo

Lean on Vampire Proofs (Short Paper)

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.36.pdf
  • Filesize: 1.12 MB
  • 9 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • Theory of computation → Higher order logic
  • Computing methodologies → Theorem proving algorithms
Keywords
  • Automated Reasoning
  • Interactive Theorem Provers
  • Automated Theorem Provers
  • Lean
  • Vampire
  • Proof Reconstruction

Metrics

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 Vampire’s output. We describe ongoing efforts in reconstructing Vampire proofs as trusted proofs in Lean. Our experiments showcase feasibility of generating trusted Vampire proofs that are validated in Lean.

Cite As Get BibTex

Jonas Bodingbauer, Márton Hajdu, Laura Kovács, Axel Polaczek, and Michael Rawson. Lean on Vampire Proofs (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 36:1-36:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.36

Author Details

Jonas Bodingbauer
  • TU Wien, Austria
Márton Hajdu
  • TU Wien, Austria
Laura Kovács
  • TU Wien, Austria
Axel Polaczek
  • TU Wien, Austria
Michael Rawson
  • University of Southampton, UK

Funding

This research was funded in whole or in part by the ERC Consolidator Grant ARTIST 101002685, the ERC Proof of Concept Grant LEARN 101213411, and by the SBA Research COMET Center SBA-K1 NGC managed by the FFG.

Acknowledgements

We thank Henrik Böving for providing helpful insights on Lean.

Supplementary Materials

References

  1. Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, and Peter H. Schmitt. The KeY Approach: Integrating Object Oriented Design and Formal Verification. In JELIA, 2000. URL: https://doi.org/10.1007/3-540-40006-0_3.
  2. Michael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In CPP, 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_12.
  3. Leo Bachmair and Harald Ganzinger. Resolution Theorem Proving. In Handbook of Automated Reasoning. North-Holland, 2001. URL: https://doi.org/10.1016/B978-044450813-3/50004-7.
  4. Seulkee Baek. A Formally Verified Checker for First-Order Proofs. In ITP, Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:13, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.6.
  5. Clark W. Barrett, Thomas A. Henzinger, and Sanjit A. Seshia. Certificates in AI: Learn but Verify. Communications of ACM, 2026. URL: https://doi.org/10.1145/3737447.
  6. Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, and Andrei Voronkov. The Vampire Diary. In CAV, 2025. URL: https://doi.org/10.1007/978-3-031-98682-6_4.
  7. Raven Beutner and Bernd Finkbeiner. Checking Satisfiability of Hyperproperties Using First-Order Logic. In ATVA, 2024. URL: https://doi.org/10.1007/978-3-031-78750-8_10.
  8. Dirk Beyer. Reliable and Reproducible Competition Results with BenchExec and Witnesses Report on SV-COMP 2016. In TACAS, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_55.
  9. Sascha Böhme. Proof reconstruction for Z3 in Isabelle/HOL. In SMT Workshop, 2009. Google Scholar
  10. Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andrés Goens, Aaron Hill, Harald Husum, Hernán Ibarra Mejia, Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, Jérémy Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, and Fan Zheng. The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale, 2025. URL: https://doi.org/10.48550/arXiv.2512.07087.
  11. Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex Keizer, Léon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark Barrett, and Tobias Grosser. Interactive Bitvector Reasoning using Verified Bit-Blasting. Proceedings of the ACM on Programming Languages (OOPSLA), 2025. URL: https://doi.org/10.1145/3763167.
  12. Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In ITP, 2024. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.10.
  13. Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In CADE, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  14. Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In ITP, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.8.
  15. Remi Desmartin, Omri Isac, Grant O. Passmore, Ekaterina Komendantskaya, Kathrin Stark, and Guy Katz. A Certified Proof Checker for Deep Neural Network Verification in Imandra. In ITP, 2025. URL: https://doi.org/10.4230/LIPIcs.ITP.2025.1.
  16. Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovács, and Giles Reger. The Rapid Software Verification Framework. In FMCAD, 2022. URL: https://doi.org/10.34727/2022/ISBN.978-3-85448-053-2_32.
  17. Simon Jeanteur, Laura Kovács, Matteo Maffei, and Michael Rawson. CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. In IEEE SP, 2024. URL: https://doi.org/10.1109/SP54263.2024.00246.
  18. Anja Petkovic Komel, Michael Rawson, and Martin Suda. Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo. CoRR, 2025. URL: https://doi.org/10.48550/arXiv.2503.15541.
  19. Laura Kovács and Andrei Voronkov. First-Order Theorem Proving and Vampire. In CAV, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_1.
  20. Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, and Cesare Tinelli. IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. In TACAS, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_17.
  21. Evan Laufer, Alex Ozdemir, and Dan Boneh. zkPi: Proving Lean Theorems in Zero-Knowledge. In CCS, 2024. URL: https://doi.org/10.1145/3658644.3670322.
  22. The mathlib Community. The lean mathematical library. In CPP, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  23. William McCune. Solution of the Robbins Problem. Journal of Automated Reasoning, 1997. URL: https://doi.org/10.1023/A:1005843212881.
  24. Jia Meng and Lawrence C. Paulson. Translating Higher-Order Clauses to First-Order Clauses. Journal of Automated Reasoning, 2008. URL: https://doi.org/10.1007/s10817-007-9085-y.
  25. Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark W. Barrett. lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. In CAV, 2025. URL: https://doi.org/10.1007/978-3-031-98682-6_11.
  26. Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, and Andrei Voronkov. On the Evaluation of Indexing Techniques for Theorem Proving. In IJCAR, 2001. URL: https://doi.org/10.1007/3-540-45744-5_19.
  27. Robert Nieuwenhuis and Albert Rubio. Paramodulation-Based Theorem Proving. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 371-443. Elsevier and MIT Press, 2001. URL: https://doi.org/10.1016/B978-044450813-3/50009-6.
  28. Yicheng Qian, Joshua Clune, Clark W. Barrett, and Jeremy Avigad. Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers. In CAV, 2025. URL: https://doi.org/10.1007/978-3-031-98682-6_10.
  29. Michael Rawson, Andrei Voronkov, Johannes Schoisswohl, and Anja Petkovic Komel. Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories. In CADE, 2025. URL: https://doi.org/10.1007/978-3-031-99984-0_8.
  30. Giles Reger, Martin Suda, and Andrei Voronkov. New Techniques in Clausal Form Generation. In GCAI, 2016. URL: https://doi.org/10.29007/dzfz.
  31. Neha Rungta. A Billion SMT Queries a Day (Invited Paper). In CAV, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_1.
  32. Stephan Schulz. Empirical properties of term orderings for superposition. In Boris Konev, Claudia Schon, and Alexander Steen, editors, PAAR, CEUR Workshop Proceedings. CEUR-WS.org, 2022. URL: https://ceur-ws.org/Vol-3201/paper4.pdf.
  33. Geoff Sutcliffe. Stepping Stones in the TPTP World. In IJCAR, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_3.
  34. Josef Urban and Geoff Sutcliffe. Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. In AISC, 2010. URL: https://doi.org/10.1007/978-3-642-14128-7_12.
  35. Andrei Voronkov. AVATAR: The Architecture for First-Order Theorem Provers. In CAV, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_46.
  36. Lawrence Wos, George A. Robinson, Daniel F. Carson, and Leon Shalla. The Concept of Demodulation in Theorem Proving. J. ACM, 14(4):698-709, October 1967. URL: https://doi.org/10.1145/321420.321429.
  37. Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, and Sean Welleck. Premise Selection for a Lean Hammer, 2025. URL: https://doi.org/10.48550/arXiv.2506.07477.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact