Lean for All

Day 29: Case study: the statement does not match the claim🔗

Compare formal statements of a competition problem with the problem, and find exactly how each one falls short.

Competition problems are a favorite benchmark for AI provers. A known risk: if the formal statement does not match the problem, a “solved” result means nothing. Collections of formalized problems have contained such mismatches, and claims of “hundreds of problems solved” have counted some of them.

Our problem:

Find all integers x such that x · x = x + 6.

The answer is x = 3 and x = −2 (check: 9 = 3 + 6, and 4 = −2 + 6). “Find all” has two halves: these numbers are solutions, and there are no others.

An AI submits this file, saying “solved, three theorems, no sorry”. All accepted, and the Audit finds no red flags.

/-! Problem: find all integers x such that x * x = x + 6. (The answer: x = 3 and x = -2.) -/ /-- Solved: the equation has a solution. -/ theorem quadratic_solved : ∃ x : Int, x * x = x + 6 := ⟨3, ⊢ 3 * 3 = 3 + 6 All goals completed! 🐙⟩ /-- Solved: 3 is the only solution. -/ theorem only_solution (x : Nat) (h : x * x = x + 6) : x = 3 := x:Nath:x * x = x + 6⊢ x = 3 x:Nath:x * x = x + 6hx:x < 4⊢ x = 3 x:Nath:x * x = x + 6hx:x < 4this:x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3⊢ x = 3 h:0 * 0 = 0 + 6hx:0 < 4⊢ 0 = 3h:1 * 1 = 1 + 6hx:1 < 4⊢ 1 = 3h:2 * 2 = 2 + 6hx:2 < 4⊢ 2 = 3h:3 * 3 = 3 + 6hx:3 < 4⊢ 3 = 3 h:0 * 0 = 0 + 6hx:0 < 4⊢ 0 = 3h:1 * 1 = 1 + 6hx:1 < 4⊢ 1 = 3h:2 * 2 = 2 + 6hx:2 < 4⊢ 2 = 3h:3 * 3 = 3 + 6hx:3 < 4⊢ 3 = 3 All goals completed! 🐙 /-- Solved: the answers are 3 and -2. -/ theorem answers_work (x : Int) (h : x = 3 ∨ x = -2) : x * x = x + 6 := x:Inth:x = 3 ∨ x = -2⊢ x * x = x + 6 ⊢ 3 * 3 = 3 + 6⊢ -2 * -2 = -2 + 6 ⊢ 3 * 3 = 3 + 6⊢ -2 * -2 = -2 + 6 All goals completed! 🐙

Each theorem is correct. Now step 2: read each statement out loud, and compare it with “find all integers x with x · x = x + 6”.

What each one really says:

  1. quadratic_solved: “there is some integer with x · x = x + 6”. One example (3). It does not find all, and it does not even mention −2.

  2. only_solution: “every natural number x with x · x = x + 6 is 3”. True, but on Nat the solution −2 does not exist. Over the integers, the statement would be false.

  3. answers_work: “if x is 3 or −2, then x is a solution”. This checks the answer, but only one direction: it does not show there are no other solutions.

None of them is wrong. All of them are weaker than the problem.

A statement that matches the problem says both halves at once, over the integers, with ↔:

theorem quadratic_all_solutions (x : Int) : x * x = x + 6 ↔ x = 3 ∨ x = -2 := x:Int⊢ x * x = x + 6 ↔ x = 3 ∨ x = -2 x:Int⊢ x * x = x + 6 → x = 3 ∨ x = -2x:Int⊢ x = 3 ∨ x = -2 → x * x = x + 6 x:Int⊢ x * x = x + 6 → x = 3 ∨ x = -2 x:Inth:x * x = x + 6⊢ x = 3 ∨ x = -2 x:Inth:x * x = x + 6h1:(x - 3) * (x + 2) = 0⊢ x = 3 ∨ x = -2 x:Inth:x * x = x + 6h1:(x - 3) * (x + 2) = 0h2:x - 3 = 0⊢ x = 3 ∨ x = -2x:Inth:x * x = x + 6h1:(x - 3) * (x + 2) = 0h2:x + 2 = 0⊢ x = 3 ∨ x = -2 x:Inth:x * x = x + 6h1:(x - 3) * (x + 2) = 0h2:x - 3 = 0⊢ x = 3 ∨ x = -2 x:Inth:x * x = x + 6h1:(x - 3) * (x + 2) = 0h2:x - 3 = 0⊢ x = 3; All goals completed! 🐙 x:Inth:x * x = x + 6h1:(x - 3) * (x + 2) = 0h2:x + 2 = 0⊢ x = 3 ∨ x = -2 x:Inth:x * x = x + 6h1:(x - 3) * (x + 2) = 0h2:x + 2 = 0⊢ x = -2; All goals completed! 🐙 x:Int⊢ x = 3 ∨ x = -2 → x * x = x + 6 ⊢ 3 * 3 = 3 + 6⊢ -2 * -2 = -2 + 6 ⊢ 3 * 3 = 3 + 6⊢ -2 * -2 = -2 + 6 All goals completed! 🐙

for every x : Int, x · x = x + 6 if and only if x = 3 or x = −2.

“If” is answers_work. “Only if” is the hard half: the proof rewrites the equation as (x − 3)(x + 2) = 0, and a product is zero only when a factor is.

When you audit a solution to a “find all” problem, look for exactly this shape: ∀ x : (the right type), (condition) ↔ (x is one of the answers).

Check yourself🔗