lean_workbook_plus_79829

⚠️ 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.

Let assume an AP with the first term $a$ - a non-negative integer and the common difference is $d$. So, the $n^{th}$ term of the AP will be $T_{n}=a+(n-1)d$. As the AP is increasing $\exists min(n)$ for which $T_{n}{\geq} d^{2}$ and also $T_{n+1}$ is a perfect square. Let's say $T_{n+1}=p^{2}$ so we can conclude... $d^{2}{\leq}p^{2}$ hence $d{\leq}p$. We also have .. $T_{n+2}=p^{2}+d < p^{2}+2p+1=(p+1)^{2}$. so the bound for $T_{n+2}$ is ..... $p^{2}<T_{n+2}<(p+1)^{2}$. There are no perfect squares between two consecutive perfect squares. This contradicts our assumption that every term is a perfect square. And also it is an integer. So no such AP exists...

Why this node was retired

The posted statement is

theorem lean_workbook_plus_79829 : ¬ (∃ a d : ℕ, ∀ n : ℕ, ∃ p : ℕ, a + (n-1)*d = p^2)   :=  by sorry

The source increasing AP assumption d>0 was omitted, allowing a constant square progression.

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

Proposed corrected statement

For a∈ℕ and d>0 prove that not every term a+nd(n≥0) is a square; equivalently an all-square arithmetic progression must have d=0 and square a.

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.