Erdős problem 394
For the least with , do the conjectured logarithmic-saving and adjacent-length estimates hold on average? Both answered affirmatively, with admissible in the bound.
Sources
FormalConjectures/ErdosProblems/
394.lean
Retained formal statement
Erdős and Hall conjecture that the sum is for any .
∀ c < Real.log 2, (fun x => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(Erdos394.t 2 n)) =o[Filter.atTop] fun x => x ^ 2 / Real.log x ^ cOpenStatement only, no proof