Vacuous Theorems in Lean 4: How Contradictory Hypotheses Pass the Kernel
How a flipped inequality or off-by-one bound in a Lean 4 theorem hypothesis makes the statement vacuously true, why the kernel accepts it without warning, and how vacuity probes catch it.
1. How vacuous truth happens in real specifications
In classical and constructive logic alike, False → P holds for every proposition P. When a theorem’s hypotheses cannot be satisfied simultaneously—because a refactor flipped an inequality, a natural-number subtraction truncated at zero, or two range bounds fail to overlap—Lean’s tactics (omega, linarith, simp_all, contradiction) close the goal immediately from the contradictory premises without ever touching the conclusion.
Consider the bug in SeamCert’s demo file (VacuousCircuitSpec.lean): a 32-bit range check over two 16-bit limbs (lo and hi) where a typo constrained l.lo twice instead of constraining l.hi:
theorem range_check_sound (l : Limbs) (x : Nat)
(hx : x = l.value) (hlo : l.lo < 2 ^ 16) (hlo' : 2 ^ 16 ≤ l.lo) :
x < 2 ^ 32 := by
omega2. Why the Lean kernel and #print axioms stay silent
From the kernel’s point of view, range_check_sound is a completely valid theorem: for every l : Limbs that satisfies both l.lo < 65536 and 65536 ≤ l.lo, x < 2 ^ 32 does hold, because no such l exists. There is no sorryAx, no ofReduceBool, and no compiler warning.
Because omega discharges linear arithmetic contradictions automatically, the proof script looks ordinary and short. Even worse, if you change the conclusion from x < 2 ^ 32 to x < 2 ^ 31 or x = 0, the exact same by omega proof still compiles.
3. Automated detection: Vacuity probes (Mutants.lean)
SeamCert tests every theorem with hypotheses using two complementary checks:
1. **Static pairwise comparison analysis:** Parses top-level conjuncts (∧) in all proposition binders and arrow premises, normalises <, ≤, >, ≥, =, and ≠, and flags impossible natural-number bounds (n < 0), false literal inequalities (3 < 2), and contradictory pairs (a < b and b ≤ a).
2. **Planted vacuity probe (M_vacuity) and constant perturbation (M_const):** Generates an example with the exact same binders and hypotheses as your theorem, replaces the conclusion with False, and tries standard automation:
example (l : Limbs) (x : Nat) (hx : x = l.value) : l.lo < 2 ^ 16 → 2 ^ 16 ≤ l.lo → False := by
intros
first
| contradiction
| omega
| (simp_all; done)
| decide4. The definitive fix: Prove a consistency witness
A vacuity probe that fails to compile shows that simple automation could not derive False from the hypotheses, but subtle contradictions across custom structures can still hide beyond omega and simp_all.
In a Deep Audit (and as best practice in any formal specification), we pair every main theorem with an explicit **witness example** proving ∃ inputs, H₁ inputs ∧ H₂ inputs ∧ ... on a non-trivial concrete instance. Once a witness compiles, the hypotheses are provably consistent in Lean’s logic.
Questions & Answers
Does Lean 4 have a built-in linter for vacuous hypotheses?
Lean 4’s unused-variables linter warns when a named hypothesis binder is not referenced in the proof term. However, in a vacuous proof, the contradictory hypotheses ARE used to close the goal—it is the conclusion or the remaining non-contradictory hypotheses that go unused.
Why does constant perturbation also catch vacuity?
If a proof closes the goal purely from contradictory hypotheses, the proof term never depends on the numbers in the conclusion. Changing x < 2 ^ 32 to x < 2 ^ 31 while keeping the original proof still compiles, immediately exposing that the bound was not used.
Sources & References
Run the static scanner or commission a Deep Audit
Paste your statement file on the front page for an immediate static reading and a generated Mutants.lean file, or commission a £349 Deep Audit for an independent dual-kernel replay, consistency witness, and Mathlib definition reading.