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
In [ErGr80] they mention a conjecture of Erdős that the sum is . This was proved by Erdős and Hall [ErHa78], who proved that in fact
(fun x => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(Erdos394.t 2 n)) =O[Filter.atTop] fun x => ↑x ^ 2 * (Real.log (Real.log (Real.log ↑x)) / Real.log (Real.log ↑x))SolvedStatement only, no proof