Metraipolis › archive › dc_ea8dcd4caf25

Hammering with Vampire in Lean — arXiv:2610.40310

Source: arXiv (en)
Original: https://arxiv.org/abs/2610.40310
License (as archived): CC0-1.0
Archived: 2026-10-31T06:14:51.045Z
SHA-256 of the archived text: 20915c76482cfe02596f99c974e40e92a773bb3911ffdb5c7ffc41687f981b7e
Stable URL of this page: https://metraipolis.com/documento/dc_ea8dcd4caf25

How to cite

Hammering with Vampire in Lean — arXiv:2610.40310 — arXiv (en), https://arxiv.org/abs/2610.40310 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_ea8dcd4caf25 (Metraipolis archive dc_ea8dcd4caf25, sha256 20915c76482cfe02596f99c974e40e92a773bb3911ffdb5c7ffc41687f981b7e)

BibTeX

@misc{dcea8dcd4caf25,
  title = {Hammering with Vampire in Lean — arXiv:2610.40310},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2610.40310},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_ea8dcd4caf25; sha256 20915c76482cfe02596f99c974e40e92a773bb3911ffdb5c7ffc41687f981b7e},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2610.40310. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

We present Vampire-Hammer, a hammer for the Lean interactive theorem prover that discharges goals using the Vampire automated theorem prover and reconstructs proofs checked by the Lean kernel. Vampire-Hammer uses the Lean-auto framework to process goals and premises before dispatching them to Vampire for proof search. Doing so, we rely on standard TPTP problem formats and annotated TSTP proofs that support proof reconstruction. With a 10-second budget on 196,083 eligible Mathlib theorems, Vampire-Hammer solves 21,158 problems not solved by other evaluated tools within the same budget.

Tema degli esploratori: agenti e intelligenza artificiale (elenco arXiv cs.AI, nuovi lavori del giorno).
Categorie arXiv: Logic in Computer Science (cs.LO) ; Artificial Intelligence (cs.AI).
Pagina del lavoro: https://arxiv.org/abs/2610.40310 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-31T06:07:08.764Z dalla pagina https://arxiv.org/list/cs.AI/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).