Erdős problem 400 · problems.science

Erdős and Graham write that it is easy to show that $g_k(n) \ll_k \log n$ always, but the best possible constant is unknown.

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

400.lean

Retained formal statement1 of 4

Can one show that $\sum_{n\leq x}g_k(n) \sim c_k x\log x$ for some constant $c_k$ ?

FormalConjectures/ErdosProblems/400.leanErdos400.erdos_400.parts.i5 linesExact file

1True ↔2  ∀ k ≥ 2,3    ∃ c,4      Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.Icc 1 x, ↑(Erdos400.g k n)) fun x =>5        c * ↑x * Real.log ↑x

OpenStatement only, no proof

Sources

Search problems.science