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 statement4 of 5

A positive answer to this question for all $k\geq 5$ follows from the lower bound in [erdosproblems.com/986] given by Bradač [Br26].

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

1∀ k ≥ 3, ∃ c > 0, (fun n => ↑n ^ (1 - 2 / (↑k + 1)) / Real.log ↑n ^ c) =O[Filter.atTop] fun n => ↑(Erdos920.f k n)

SolvedStatement only, no proof