Lean for All

Day 26: Proving something else🔗

Compare a statement with the claim word by word, and catch statements that are weaker or different.

The most common problem in AI-written Lean is not cheating. It is statement drift: the proof is correct, but the statement is a little different from the claim, usually weaker. Typical drifts:

  • ∃ (“some”) instead of ∀ (“every”)

  • ≤ instead of <, or → instead of ↔

  • one specific number instead of every number

  • a finite range (n < 100) instead of every n

  • Nat instead of Int or the real numbers

  • the answer written into the statement

Each one turns a hard claim into an easy theorem.

Two small examples. Claim: “every n above 1 has n · n > n”. Proved:

theorem squares_grow : ∃ n : Nat, n * n > n := ⟨2, ⊢ 2 * 2 > 2 All goals completed! 🐙⟩

That only says some n works (n = 2). One example, not every case.

Claim: “n < n · n for every n above 1”. Proved:

theorem squares_grow' (n : Nat) : n ≤ n * n := Nat.le_mul_self n

≤ instead of <, and the condition “above 1” dropped. True, but it is not the claim: it allows n · n = n.

A finite range is testing in disguise. Euler noticed that n · n + n + 41 is prime for n = 0, 1, 2, … . Is it prime for every n?

def isPrime (n : Nat) : Bool := n ≥ 2 && (List.range (n - 2)).all (fun k => n % (k + 2) != 0) theorem euler_prime : ∀ n, n < 40 → isPrime (n * n + n + 41) = true := ⊢ ∀ (n : Nat), n < 40 → isPrime (n * n + n + 41) = true All goals completed! 🐙 false#eval isPrime (40 * 40 + 40 + 41) 
false

(decide +kernel is decide with the computation done by Lean’s core checker; it is fully checked.) The theorem is correct, for n below 40. At n = 40 the value is 1681 = 41 · 41, not prime. A statement “for n < 40” proves nothing about all n.

Changing the kind of number changes the claim. Claim: “every integer x with x · x = 4 equals 2”. That is false: x = −2. But on Nat there is no −2:

theorem square_four (x : Nat) (h : x * x = 4) : x = 2 := x:Nath:x * x = 4⊢ x = 2 x:Nath:x * x = 4hx:x < 3⊢ x = 2 x:Nath:x * x = 4hx:x < 3this:x = 0 ∨ x = 1 ∨ x = 2⊢ x = 2 h:0 * 0 = 4hx:0 < 3⊢ 0 = 2h:1 * 1 = 4hx:1 < 3⊢ 1 = 2h:2 * 2 = 4hx:2 < 3⊢ 2 = 2 h:0 * 0 = 4hx:0 < 3⊢ 0 = 2h:1 * 1 = 4hx:1 < 3⊢ 1 = 2h:2 * 2 = 4hx:2 < 3⊢ 2 = 2 All goals completed! 🐙

A false claim, “proved”, by quietly choosing a smaller world. Always check the type: Nat, Int, or (in Mathlib) ℝ.

Last, a file can change what symbols mean:

instance weirdLT : LT Nat := ⟨fun _ _ => True⟩ theorem five_lt_two : (5 : Nat) < 2 := trivial

The instance redefines < on Nat as “always true”. A notation line can do the same for a new symbol. The Lab’s Audit warns “Defines its own notation” or notes “Defines an instance”. For notation, its English reading also shows the real meaning (a reversed symbol 10 ≺ 3 reads as 3 ≤ 10). For an instance it cannot: 5 < 2 still reads 5 < 2, so find the instance and read it. Then compare the statement with the claim, word by word.

Check yourself🔗