Erdős problem 1028
Let where ranges over all functions . Estimate .
Sources
FormalConjectures/ErdosProblems/
1028.lean
Retained formal statement
Erdős [Er63d] proved
∀ᶠ (n : ℕ) in Filter.atTop, ↑n / 4 ≤ ↑(Erdos1028.H n)SolvedStatement only, no proof