Field guide

Five ways a Lean proof can pass and still be wrong

Every snippet below type-checks. Every one has appeared in a published benchmark or an AI-generated proof. If you review formalized mathematics, this is the checklist. (There are six — mathematicians miscount too.)

"It compiles" feels like the end of the argument. It's the beginning. Lean's kernel guarantees that a proof establishes its stated theorem — nothing about whether the theorem is the one you meant, whether its hypotheses say anything, or whether its definitions are honest. Here are the six ways that guarantee gets hollowed out, each of which passes a clean build.

1. The vacuous hypothesis

An assumption that is always true, or never satisfiable, turns a theorem into a tautology. The kernel does not object to an assumption that says nothing.

theorem looks_deep (n : ℕ) (h : True) : P n := by ...
-- or worse, a hypothesis that is secretly contradictory:
theorem also_fine (n : ℕ) (h : n < n) : P n := by ...
--   `h : n < n` is unsatisfiable ⇒ anything follows, vacuously.

Benchmark reality: a "gold" formalization in Dummit–Foote (7.2.2) was found to be vacuously true, collapsing an intended biconditional into nothing. The fix is always the same — each hypothesis has to be hardened until it bites.

2. The unfaithful statement

The proof is airtight; it just proves a different, usually weaker, theorem. A dropped hypothesis, a changed domain, quantifiers in the wrong order.

-- intended: for all n. actually stated: there exists n.
theorem off_by_a_quantifier :
    ∃ n : ℕ, 0 < n → Q n := by
  exact ⟨0, by simp⟩   -- trivial; the real claim was ∀ n

The classic case: a ProofNet formalization of an Axler exercise silently omitted an essential finite-dimensionality hypothesis. The statement compiled; it was simply no longer the theorem. In one audit, discrepancies like this affected over half of the miniF2F benchmark.

3. The hidden sorry (and the stray axiom)

An unfinished proof doesn't fail — it elaborates to the sorryAx axiom and still shows a checkmark in your editor. A single custom axiom can make everything provable.

theorem important : RiemannHypothesis := by
  sorry   -- green checkmark. build succeeds. proves nothing.

-- the only defense is to read the axiom trace:
#print axioms important
-- want ONLY: propext, Classical.choice, Quot.sound
-- see `sorryAx`? or an unfamiliar axiom? stop.

This is why serious projects re-run everything through lean4checker and pin the allowed axiom set. A CI badge does not read the axiom trace for you.

4. The junk-value trap

Lean functions are total: they return something even on inputs where the mathematics is undefined. Division by zero is 0. The sum of a non-summable series is 0. Bounds can then hold for reasons that have nothing to do with your theorem.

-- ∑' is 0 when `a` isn't summable, so this "bound"
-- holds vacuously for every divergent series:
theorem bound (a : ℕ → ℝ) (S : ℝ) (h : ∀ n, a n ≤ S) :
    (∑' n, a n) ≤ S := by ...
-- missing: (hs : Summable a). Without it, meaningless.

This exact pattern was documented in a marathon formalization effort: a bound that "held" only because the sum defaulted to zero, until a Summable hypothesis was added and the statement finally meant something.

5. The dishonest definition

The subtlest of all, because the proof is genuinely correct — of a theorem about a definition that isn't the one it claims to be. If IsPrime is defined wrong, every flawless theorem about primes is flawless nonsense.

def Converges (a : ℕ → ℝ) : Prop := True   -- stubbed
-- now every theorem with a `Converges a` hypothesis
-- is trivially dischargeable and totally hollow.

A misformalized intermediate lemma can make an entire downstream development "formally correct but mathematically irrelevant." You cannot catch this by reading proofs; you have to audit the definitions against what they're supposed to mean.

6. The exploit tactic

Some tactics trust code outside the kernel. native_decide compiles and runs native code and trusts the result — a door through which a wrong answer (or an adversarial one from an AI tool) can walk straight past the kernel.

theorem suspicious : BigComputationalClaim := by
  native_decide   -- trusts the compiler + your machine, not the kernel

Tao's Equational Theories Project banned native_decide explicitly "as a precaution against exploit-based proofs (such as those that might be contributed by an AI tool)." If a result leans on it, that isn't a proof you can stake a claim on.

The common thread

None of these are bugs in Lean. Lean is doing exactly its job: proving proofs against statements. Every failure above lives one level up — in the statement, the hypotheses, the definitions, the axioms, the trusted base — where the kernel makes no promises and, as of 2026, no tool reliably checks. That level is a human's job. It is the job Qed does.