lean_workbook_plus_222

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Numbers of the form $4k+2$ as well as $1,4$ can't be generated. Hence they must be on the board. We will prove that, with these numbers, we can generate all of the other ones till $1000$ . Notice that, $3=2^2-1, 5= 3^2-2^2, 7=4^2-3^2 \cdots$ Hence using these identities

we can inductively generate all of the remaining numbers. Hence the minimum number of positive integers on the board has to be $252$ .

Why this node was retired

The posted statement is

theorem lean_workbook_plus_222 :
  IsLeast {n : ℕ | ∀ k : ℕ, 1 ≤ k ∧ k ≤ 1000 → ∃ a b : ℕ, a^2 - b^2 = k ∨ a^2 + b^2 = k ∨ 2 * a^2 = k ∨ 2 * b^2 = k} 252   :=  by sorry

The posted predicate is independent of n and does not model generation from a starting board. The full operation rules must come from the original problem.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Define the legal board-generation operation and minimize the cardinality of the initial board among boards whose closure contains1,…,1000; make the minimized n the actual cardinality.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.