aiqbench analysis
This is an automated reasoning paper: a tool that hands Lean proof goals to the Vampire prover and reconstructs the resulting proofs so the Lean kernel can check them. It involves no machine learning, but automated theorem proving is a classic AI subfield, and the paper is cross-listed in cs.AI. The headline result is a benchmark on 196,083 Mathlib theorems at a 10-second budget, where it solves 21,158 problems that the other evaluated tools miss. Readers should weigh that as a tool-demo comparison at a fixed time limit, not a general claim about automated proving.
Hammering with Vampire in Lean
arXiv:2610.40310v1 Announce Type: cross Abstract: 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.
Abstract: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.
10 pages, 3 figures, 1 table. Tool demonstration paper
Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI)
arXiv:2610.40310 [cs.LO]
(or arXiv:2610.40310v1 [cs.LO] for this version)
https://doi.org/10.48550/arXiv.2610.40310 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 194 words