ErdosProblems · research solved · AMS 11
hardknown result, no worker yet
Erdős Problem 437
Theorem 437 · Erdős
Let . How many of the partial products can be squares? Is it true that, for any , there can be more than 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
sorryProof. sorry
Nobody has tried yet.