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 statement1 of 9

Is it true that $\sum_{n\leq x}t_2(n)\ll \frac{x^2}{(\log x)^c}$ for some $c>0$ ?

FormalConjectures/ErdosProblems/394.leanErdos394.erdos_394.parts.i1 lineExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.