Skip to content

Erdős problem 394

Start work

For the least tk(n)t_k(n) with n∣tk(n)(tk(n)+1)⋯(tk(n)+k−1)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/2048c = 1/2048 admissible in the t2t_2 bound.

Sources

The source's own material, retained exactly.

10 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

394.lean

Retained formal statement2 of 9

Is it true that, for k≥2k\geq 2, ∑n≤xtk+1(n)=o(∑n≤xtk(n))?\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
True ↔  ∀ k ≥ 2,    (fun x => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(Erdos394.t (k + 1) n)) =o[Filter.atTop] fun x =>      ∑ 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.