Erdős Problem 937

Reference: erdosproblems.com/937

References:

• [BBC24] Bajpai, P., Bennett, M. A. and Chan, T. H., Arithmetic progressions in squarefull / powerful numbers, Int. J. Number Theory 20 (2024), 19-45.

def Erdos937.IsCoprimePowerfulAP4 (a d : ℕ) : Prop

The four numbers $a, a+d, a+2d, a+3d$ form a four-term arithmetic progression ($d > 0$) of pairwise coprime powerful numbers.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos937.erdos_937 : True ↔ {p : ℕ × ℕ | IsCoprimePowerfulAP4 p.1 p.2}.Infinite

Are there infinitely many four-term arithmetic progressions of coprime powerful numbers? (A number $n$ is powerful if $p \mid n \to p^2 \mid n$; Nat.Powerful.)

Erdős [Er76d] asked this; the answer is yes: Bajpai, Bennett and Chan [BBC24] proved that there are infinitely many four-term arithmetic progressions of pairwise coprime powerful numbers. (Without coprimality this is easy, and by a theorem of Fermat there are no four squares in arithmetic progression.)

theorem Erdos937.not_isCoprimePowerfulAP4_zero_one : ¬IsCoprimePowerfulAP4 0 1

Sanity check for IsCoprimePowerfulAP4: the progression $0, 1, 2, 3$ is not a valid example, since $2$ is not powerful.