Search Results

Abstract

Cite as

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)

@InProceedings{bodingbauer_et_al:LIPIcs.ITP.2026.36,
  author =	{Bodingbauer, Jonas and Hajdu, M\'{a}rton and Kov\'{a}cs, Laura and Polaczek, Axel and Rawson, Michael},
  title =	{{Lean on Vampire Proofs}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{36:1--36:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.36},
  URN =		{urn:nbn:de:0030-drops-270102},
  doi =		{10.4230/LIPIcs.ITP.2026.36},
  annote =	{Keywords: Automated Reasoning, Interactive Theorem Provers, Automated Theorem Provers, Lean, Vampire, Proof Reconstruction}
}