Erdős problem 394 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

10 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

394.lean

Retained formal statement2 of 9

Is it true that, for $k\geq 2$ , $\sum_{n\leq x}t_{k+1}(n) =o\left(\sum_{n\leq x}t_k(n)\right)?$

FormalConjectures/ErdosProblems/394.leanErdos394.erdos_394.parts.ii4 linesExact file

1True ↔2  ∀ k ≥ 2,3    (fun x => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(Erdos394.t (k + 1) n)) =o[Filter.atTop] fun x =>4      ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(Erdos394.t k n)

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.

Sources

Search problems.science