On what does not follow
Lean on Vampire
Models
Vampire finds the world where a claim fails. Lean's kernel checks it.
Michael Jagdeo 1Jeff Dumps
1 Exponent Labs LLC
01 / Background & motivation
Does it follow?
Show a world where it doesn't.
Step 1
Find
Vampire · untrusted
Searches for a finite world where the axioms hold and the claim fails.
Step 2
Translate
cm.py · trusted, tested
Turns the model and the TPTP problem into Lean, against an independent evaluator.
Step 3
Check
Checker.lean · proved
A verified evaluator, proved equal to ordinary first-order satisfaction.
Step 4
Certify
Lean kernel · the trusted base
Checks every proof. A wrong model yields no certificate.
Can a counter-model from an untrusted prover become a certificate Lean's kernel accepts, at the scale of real problems?
02 / Worked example
Break the model.
Watch Lean refuse it.
The model
Click a cell of r. Change what a and b denote.
| r | e1 | e2 |
|---|---|---|
| e1 | ||
| e2 |
- ✓
~ r(X,Y) | ~ r(Y,Z) | r(X,Z)
r is transitive · axiom
- ✓
r(a,b)
a is related to b · axiom
- ✓
~ r(b,a)
b is not related to a · negated conjecture
What Lean's kernel says
certifiedEvery formula holds, so every decide succeeds: symmetry does not follow.
-- generated by cm.py (excerpt) inductive T | e1 | e2 abbrev «a» : T := T.e1 abbrev «b» : T := T.e2 abbrev «r» (x0 x1 : T) : Prop := (4 >>> (1 * x0.idx + 2 * x1.idx)) % 2 = 1 theorem c0' : (∀ X' Y' : T, (¬(«r» X' Y') ∨ (∀ Z' : T, (¬(«r» Y' Z') ∨ («r» X' Z'))))) := by decide theorem c1' : («r» «a» «b») := by decide theorem c2' : ¬(«r» «b» «a») := by decide -- the three statements above, conjoined: theorem countermodel : Nonempty T ∧ (φ₀ ∧ (φ₁ ∧ φ₂)) := ⟨⟨T.e1⟩, ⟨c0', ⟨c1', c2'⟩⟩⟩
This is the paper's mutation test, by hand: corrupt one table entry, and Lean must accept exactly the models a separate brute-force evaluator of the original TPTP accepts. Vampire is never trusted.
03 / Evaluation
Three samples.
One frozen commit.
100 problems, one square each.
- Certified, kernel only 59
- Certified with native code 3
- Lean ran out of budget 4
- Translator crashed 2
- Model finder failed to run 0
- Vampire found no model 29
- Unsupported input, refused 3
Three questions, three denominators.
Selected before its first execution. A harness-only change after an aborted attempt recorded translator exceptions as failures; after the round-4 repair all three samples were rerun at one commit, so these results are descriptive.
04 / Scale
A million facts.
A median of 5.2 minutes.
Generate, compile every module, check axioms. Model search excluded (cached). Bars: median of 3 alternating runs; grey line: range.
Reflection is
2.7×
lower on wall time (ratio of medians).
Same Lean 4.35, 4 workers for both, one 8 GB M2 laptop, commit 62d43d6. The model has one element, so this measures certificate throughput, not quantifier depth, where reflection is slower and the tool dispatches to the shallow path.
05 / Theoretical guarantee
Why a certificate
means what it says.
theorem Fm.check_iff (M : Model) (φ : Fm) :
∀ env, φ.check M env = true ↔ φ.Sem M envA Boolean evaluator, proved equal to the semantics.
Fm.check computes, by brute force over the domain, whether a formula holds; Fm.Sem says it in logic. Proved once, the equivalence lets every certificate run one kernel evaluation instead of elaborating one proposition per formula.
Why validity and well-formedness are part of every certificate.
A certificate needs check, wf and valid all true, so none of these can produce one. Each value shown is a kernel-checked line of tests/Boundary.lean.
| Case | Model | Formula | check | wf | valid | Certificate |
|---|---|---|---|---|---|---|
| Constant out of range | n := 1, c ↦ 1 | ∀ x, x ≠ c | true | false | · | none |
| Empty domain | n := 0 | ∀ x, ⊥ | true | · | false | none |
| Function leaves the domain | n := 2, f ↦ 2 | — | · | · | false | none |
| Unbound variable | n := 1, c ↦ 1 | x₃ = x₃ | · | false | · | none |
| Function at an unchecked arity | n := 1, f/1 listed | ∀ x, f(x, x) = x | · | false | · | none |
06 / Trust & review
What is trusted,
and what review changed.
| Stage | Code | Trusted? | How it is checked |
|---|---|---|---|
| Find | Vampire | untrusted | A wrong model makes a decide or the evaluator fail; mutation tests confirm Lean rejects broken models. |
| Input preprocessing | bench.expand | trusted, tested | Benchmark only. Tested include expansion; every input checked by SHA-256 against the official TPTP release. |
| Model parse | model() | untrusted | Validity, well-formedness and nonemptiness are kernel-checked parts of every certificate. |
| Record reading | statements | trusted, tested | Every character of the file is accounted for or the file is rejected; tested against the oracle's separately written reader and hand-counted fixtures. |
| Rewrite | problem, miniscope | trusted, tested | Each rewritten formula is compared with its original on the model and every one-entry mutation of it. |
| Translate | lean(), tokens() | trusted, tested | Lean must accept exactly the mutants a separate brute-force evaluator of the original source accepts. |
| Evaluate | Checker.lean | proved | check_iff and sem_iff_sat are kernel-checked theorems. |
| Certify | Lean kernel | trusted base | Axioms: propext (shallow); propext and Quot.sound (reflected). |
Four rounds of peer review.
The reviewer asked
Auditing the delivered code, the reviewer showed that a legal TPTP record could be skipped without error, and that the test oracle copied the same record reader, so both accepted a model of a weakened problem.
What changed
Records are now read by a total, fail-closed reader and the oracle has its own. The defect had dropped records from 9 benchmark inputs, 8 reported as certified; all three samples were rerun.
07 / Looking ahead
Proofs in. Models in.
Lean on Vampire Proofs brings Vampire's refutations into Lean. This brings its models. The remaining step is on the user's side: a command inside Lean that takes a goal and returns a certified counter-model.