Erdős problem 394

For the least $t_k(n)$ with $n \mid t_k(n)(t_k(n)+1)\cdots(t_k(n)+k-1)$ , do the conjectured logarithmic-saving and adjacent-length estimates hold on average? Both answered affirmatively, with $c = 1/2048$ admissible in the $t_2$ bound.

Sources

The source's own material, retained exactly.

10 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

394.lean

Retained formal statement7 of 9

Since $t_2(p)=p-1$ for prime $p$ it is trivial that $\sum_{n\leq x}t_2(n)\gg \frac{x^2}{\log x}$ .

FormalConjectures/ErdosProblems/394.leanErdos394.erdos_394.variants.lower_bound1 lineExact file

1(fun x => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(Erdos394.t 2 n)) =O[Filter.atTop] fun x => ↑x ^ 2 / Real.log ↑x

SolvedStatement only, no proof