ErdosProblems · research solved · AMS 11

hardknown result, no worker yet

Erdős Problem 437

Theorem 437 · Erdős

Let 1≤a1<⋯<ak≤x1\leq a_1<\cdots<a_k\leq x. How many of the partial products a1,a1a2,…,a1⋯aka_1,a_1a_2,\ldots,a_1\cdots a_k can be squares? Is it true that, for any ϵ>0\epsilon>0, there can be more than x1−ϵx^{1-\epsilon} squares?

The answer is yes, which follows from work of Bui, Pratt, and Zaharescu [BPZ24], as noted by Tao [Ta24].

Formal statement · Lean 4.lean
theorem erdos_437 : answer(True) ↔
    ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℕ in atTop, (x : ℝ) ^ (1 - ε) < L x := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗