Erdős problem 938

Let $A=\{n_1 < n_2 < \cdots\}$ be the sequence of powerful numbers (if $p\mid n$ then $p^2\mid n$ ). Are there only finitely many three-term progressions of consecutive terms $n_k,n_{k+1},n_{k+2}$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

938.lean

Retained formal statement1 of 1

Let $A=\{n_1 < n_2 < \cdots\}$ be the sequence of powerful numbers (if $p\mid n$ then $p^2\mid n$ ). Are there only finitely many three-term progressions of consecutive terms $n_k,n_{k+1},n_{k+2}$ ?

FormalConjectures/ErdosProblems/938.leanErdos938.erdos_9384 linesExact file

1True ↔2  {P |3      (↑P).IsAPOfLength 3 ∧4        ∃ k, P = {Nat.nth Nat.Powerful k, Nat.nth Nat.Powerful (k + 1), Nat.nth Nat.Powerful (k + 2)}}.Finite

OpenStatement only, no proof