Erdős Problem 363

References:

• erdosproblems.com/363
• [BaBe07] Bauer, Mark and Bennett, Michael A., On a question of Erd\H{o}s and Graham. Enseign. Math. (2) (2007), 259--264.
• [BeVL12] Bennett, Michael A. and Van Luijk, Ronald, Squares from blocks of consecutive integers: a problem of Erd\H{o}s and Graham. Indag. Math. (N.S.) (2012), 123--127.
• [Ul05] Ulas, Maciej, On products of disjoint blocks of consecutive integers. Enseign. Math. (2) (2005), 331--334.

def Erdos363.IsInterval (I : Finset ℕ) : Prop

A finite set of naturals is an interval of naturals.

Equations

• Erdos363.IsInterval I = ∃ (a : ℕ) (b : ℕ), I = Finset.Icc a b

def Erdos363.IsValidCollection (S : List (Finset ℕ)) : Prop

A collection of intervals as in Erdős Problem 363.

Equations

• Erdos363.IsValidCollection S = ((∀ I ∈ S, Erdos363.IsInterval I) ∧ (∀ I ∈ S, 4 ≤ I.card) ∧ List.Pairwise Disjoint S ∧ IsSquare (List.map (fun (I : Finset ℕ) => ∏ m ∈ I, m) S).prod)

theorem Erdos363.erdos_363 : False ↔ {S : List (Finset ℕ) | IsValidCollection S}.Finite

Is it true that there are only finitely many collections of disjoint intervals $I_1,\ldots,I_n$ of size $\lvert I_i\rvert \geq 4$ for $1\leq i\leq n$ such that[\prod_{1\leq i\leq n}\prod_{m\in I_i}m]is a square?

This is false: Ulas [Ul05] constructed infinitely many such collections.