Erdős problem 920

Is it true that, for $k\geq 4$ , $f_k(n) \gg \frac{n^{1-\frac{1}{k-1}}}{(\log n)^{c_k}}$ for some constant $c_k>0$ ?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

920.lean

Retained formal statement2 of 5

It is known that $f_3(n)\asymp (n/\log n)^{1/2}$ (see [erdosproblems.com/1104]).

FormalConjectures/ErdosProblems/920.leanErdos920.erdos_920.variants.k_eq_31 lineExact file

1(fun n => ↑(Erdos920.f 3 n)) =Θ[Filter.atTop] fun n => (↑n / Real.log ↑n) ^ (1 / 2)

SolvedStatement only, no proof