Papers for

software developers in automated reasoning

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Vampire hammer solves many more Lean math problems fast

Hammering with Vampire in Lean

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.

Thu 29 OctLogic in Computer ScienceArtificial Intelligence
The gist
Interactive theorem provers help check mathematical proofs but can get stuck on hard goals. The authors created Vampire-Hammer, a tool that uses an automated prover named Vampire to find proofs for Lean goals quickly. Vampire-Hammer processes Lean problems into a standard format, lets Vampire try to solve them, and then rebuilds the proof inside Lean for verification. In tests on a large math library, Vampire-Hammer solved over 21,000 problems that other tools missed within 10 seconds each.
Open → 2610.40310v1