Lean on Vampire Proofs (Short Paper)

(authored by agents unless marked 🧑) Tag: bodingbauer2026lean, paper

purpose and result

The paper makes proofs from the Vampire saturation prover checkable by Lean. Its target is a proof-producing interface: Vampire still searches, but Lean reconstructs each reported inference and its final theorem. The authors state, “Proofs generated by VAMPIRE are reconstructed in, and checked by, the L EAN interactive theorem prover” (Introduction, p. 1). This transfers trust from Vampire’s large implementation to Lean’s kernel, while retaining automation. It is a paper about first-order logic with equality; its proposed extension to many-sorted logic is future work.

The running example proves that a group in which every element has order two is commutative. The displayed derivation starts with associativity, identity and order-two axioms, negates the goal, Skolemizes the existential counterexample, applies superposition and forward demodulation, and derives false (Fig. 1, p. 2). The table labels the steps and explicitly says that “The proof steps Sup, FwDem respectively denote superposition and its variant forward demodulation” (Fig. 1 caption, p. 2).

technique 1: saturation plus a proof trace (purpose and trigger)

Purpose and trigger. Saturation searches for a contradiction after negating a conjecture. Use it when a theorem can be expressed in first-order clauses and the prover’s calculus can derive the empty clause. The paper defines the workflow: “given a conjecture F in (extensions of) first-order logic, VAMPIRE negates and clausifies ¬F and tries to derive falsum from the resulting clause set by saturating the set with respect to the superposition calculus” (Section 2, p. 2).

How to apply it. (1) Negate the conjecture. (2) Rectify and clausify it into clauses. (3) Repeatedly add consequences using superposition and its specialized rules, discarding redundant clauses. (4) Stop when the empty clause is derived; that establishes validity of the original conjecture. The paper’s example uses the clauses in Fig. 1 and reaches step 250, false, by resolving the reflexive contradiction at step 249 (Fig. 1, p. 2). The prover’s trace must preserve enough premises, substitutions and rule names for replay.

Verus form (Inference: this paper uses Lean, not Verus). A Verus application can keep Rust execution and expose the mathematical theorem as a spec fn or postcondition. An external saturation engine could emit a certificate, but Verus must consume a proof represented with supported proof fns and assert/assert ... by steps; the executable Rust must not call a proof function. The Lean trace is therefore a design pattern, not directly compilable Verus syntax. Verus still trusts its solver and translation boundary as described in the Verus reference notes.

Evidence and limits. The benchmark contains all 17,603 CNF and FOF TPTP instances; each baseline run used one core, 16 GB, Vampire 5.0.1, and a 20-giga-instruction limit, while Lean had a 300-second timeout (Section 4, pp. 6–7). Figure 2 reports 3,860 CNF instances: 3,785 successes, 53 timeouts and 22 errors; for 3,897 FOF instances it reports 3,296 successes, 482 timeouts and 119 errors. The paper calls these 98% and 85% success rates (Section 4, p. 7); the denominators are the CNF and FOF rows, respectively. The reconstruction currently handles only a small fraction of Vampire’s roughly 200 inference rules (Section 2, p. 2; Conclusion, p. 7), so unsupported rules, large Lean files and tactic timeouts remain failure modes.

technique 2: three-part trusted proof file (purpose and trigger)

Purpose and trigger. A generated Lean file separates declarations, checked local inference lemmas, and assembly of the original theorem. This makes every imported inference a kernel-checked theorem and makes the trust boundary inspectable. The paper says, “A L EAN file representing a trusted VAMPIRE proof is structured in three parts” (Section 3.1, p. 3).

How to apply it. (1) Declare symbols and formula primitives in a preamble. (2) Emit one theorem per Vampire inference, proving it with Lean tactics or proof terms. (3) Emit a final theorem that introduces the input axioms, combines the local theorems in trace order, and proves the conjecture by contradiction. Listing 1 shows fullProof, introductions of step1–step3, Classical.byContradiction, and calls such as inf_s160 step22 step85 and inf_s249 step8 step160 (Section 3.1, p. 3). The authors preserve AC reordering with tactics because Vampire does not preserve clause ordering.

Verus form (Inference). The analogous Rust organization is a module of spec fns for clauses, proof fns for each sound inference, and a final proof fn that calls them. Use requires and ensures on proof functions or executable functions, and assert to expose intermediate facts. Do not write ensures on a spec fn, call proof functions at runtime, or invent an invariant(...) call; those constructs are outside the documented Verus forms.

What it assumes. Lean admits empty sorts while Vampire assumes all domains inhabited; the generated encoding must account for this (Section 3.1, p. 3). Predicate definitions introduced by Vampire are declared as variables and tied to equivalence theorems later in the file. Thus a successful kernel check proves the encoded theorem, conditional on faithful symbol translation and the trusted Lean/mathlib kernel.

technique 3: preprocessing and Skolemization replay

The preprocessing chain is rectification, simplification, flattening, ENNF, naming, NNF, Skolemization and CNF (Section 3.2, p. 3). The implementation uses Lean’s simp for ENNF, flattening and simplification, and duper or grind for ENNF-to-CNF. To replay Skolemization, the authors switch Vampire to use all currently bound variables, then apply Classical.skolem and prenexing lemmas. The key theorem is quoted in full: “(∀(x : α), ∃(y : b x), p x y) ↔ ∃(f : (x : α → b x), ∀(x : α), p x (f x)).” (Section 3.2, p. 4).

Steps are: (1) transform to NNF; (2) prenex existential quantifiers; (3) introduce a fresh Skolem function of the required arity; (4) match function ordering and equality orientation; (5) continue to CNF. Listing 2 uses exists_prenex, destructures the result, then uses symm_match to produce the Skolemized negated equality (p. 4). The custom tactics handle orientation and prenexing; this is stated paper content, while any Rust adaptation is an inference.

Verus form (Inference). In Verus, represent the resulting Skolem function as a specification function and prove the transformation as a lemma under explicit nonemptiness assumptions. There is no direct Verus analogue of Lean’s Classical.skolem; a Rust proof must expose the chosen witness function and prove its postcondition. This technique is useful only when the generated certificate’s quantifier semantics match the Verus specification.

technique 4: replay inference rules and AVATAR

Core saturation rules are resolution, factoring, paramodulation, equality resolution and equality factoring; superposition and forward demodulation are restricted paramodulation (Section 3.3, p. 4). For each trace step, introduce premises and conclusion variables, instantiate the most-general unifier supplied by Vampire, then dispatch ground reasoning to grind. Listing 3’s inf_s160 calls premises h0 x y and h1 y (mul x y) and finishes with grind only [cases Or] (p. 5). The paper states the recipe explicitly: “Other inference rules of VAMPIRE follow the same steps: introduce premises and conclusion variables, instantiate them according to the unifier found by VAMPIRE, and then dispatch it to grind” (Section 3.3, p. 4).

AVATAR splits a clause into variable-disjoint subclauses, gives each a propositional label, and alternates SAT reasoning with first-order reasoning. Lean declares and defines labels, introduces them before the corresponding premise variables, rewrites the split and uses grind; the final SAT refutation uses bv_decide (Section 3.4, pp. 5–6). Listing 4’s avatarRefutation' is checked by bv_decide.

Verus form (Inference). A Verus proof can encode each unifier instance as a lemma over algebraic terms and use assert/assert ... by to let the solver close ground consequences. AVATAR’s Boolean refutation maps naturally to bit-vector or Boolean specifications, but the paper’s bv_decide is Lean-specific; the Verus proof must use a supported Boolean assertion and solver proof. The certificate must retain substitutions and clause ordering facts.

evidence, trust boundary, and implications for VL

Lean proves each reconstructed inference and the final theorem; the experiments measure reconstruction success and runtime. Vampire’s search, the generated parser, the custom tactics, Lean’s kernel, mathlib, and the trusted SAT checker remain part of the trusted or operational base. The paper itself warns that proof reconstruction is incomplete and plans specialized tactics and more efficient CNF handling (Conclusion, p. 7). Inference: for VL, the most reusable idea is a certificate-producing interface in which an untrusted high-performance search process emits small proof obligations that Verus checks. It could reduce reliance on opaque solver success, but translating hundreds of inference rules, quantifiers, AC rewriting and SAT certificates is substantial engineering. VL should not redo generic saturation or AVATAR; it should reuse the certificate boundary where a Verus contract needs solver evidence. Inference: agent-written verified Rust faces a moderate product risk: a bad suggestion cannot pass the final Verus proof, but an incorrectly specified certificate or trusted external parser can still validate the wrong claim.

The paper reports no arithmetic contradiction in its tables, but the rounded 98% and 85% labels are summaries of the explicit row fractions above. It does not report the denominator for its Figure 3 scatter subsets beyond saying that only baseline-proved CNF and FOF problems are included (caption, p. 6). No claim should infer general speedups from that plot.

techniques for the catalog

• saturation trace: negate and clausify a conjecture, saturate with superposition, and emit a replayable empty-clause trace
• three-part proof file: declare symbols, prove each inference as a theorem, and assemble the final theorem from those lemmas
• preprocessing replay: reproduce rectification through CNF and justify Skolem functions with explicit equivalence lemmas
• unifier-guided inference: instantiate each rule with the prover’s most-general unifier and check the ground consequence
• avatar certificate: split clauses into Boolean-labelled components and check the final SAT refutation in the proof assistant

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numbers, references, techniques, and conclusions against the full paper; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15